∀ {F : Type u_3} {R : Type u_4} [inst : Semiring R] [inst_1 : EquivLike F R Rᵐᵒᵖ],
  (∀ (f : F) (a b : R), f (a * b) = f a * f b) →
    (∀ (f : F) (a b : R), f (a + b) = f a + f b) →
      (∀ (f : F) (x : R), MulOpposite.unop (f (MulOpposite.unop (f x))) = x) → RingInvoClass F R