∀ {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₂],
  (∀ (f : F) (a b : M), f (a + b) = f a + f b) →
    (∀ (f : F) (r : R) (x : M), f (r • x) = σ r • f x) →
      autoParam (∀ (f : F), Continuous ⇑f) ContinuousSemilinearEquivClass.map_continuous._autoParam →
        autoParam (∀ (f : F), Continuous (EquivLike.inv f)) ContinuousSemilinearEquivClass.inv_continuous._autoParam →
          ContinuousSemilinearEquivClass F σ M M₂