∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ}
  {M : outParam (Type u_4)} {inst_4 : TopologicalSpace M} {inst_5 : AddCommMonoid M} {M₂ : outParam (Type u_5)}
  {inst_6 : TopologicalSpace M₂} {inst_7 : AddCommMonoid M₂} {inst_8 : Module R M} {inst_9 : Module S M₂}
  {inst_10 : EquivLike F M M₂} [self : ContinuousSemilinearEquivClass F σ M M₂] (f : F), Continuous (EquivLike.inv f)