∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_3} [inst_4 : TopologicalSpace M]
  [inst_5 : AddCommMonoid M] {M₂ : Type u_4} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R M] [inst_9 : Module S M₂] (toLinearEquiv : M ≃ₛₗ[σ] M₂)
  (continuous_toFun : autoParam (Continuous (↑toLinearEquiv).toFun) ContinuousLinearEquiv.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toLinearEquiv.invFun) ContinuousLinearEquiv.continuous_invFun._autoParam)
  (toLinearEquiv_1 : M ≃ₛₗ[σ] M₂)
  (continuous_toFun_1 :
    autoParam (Continuous (↑toLinearEquiv_1).toFun) ContinuousLinearEquiv.continuous_toFun._autoParam)
  (continuous_invFun_1 :
    autoParam (Continuous toLinearEquiv_1.invFun) ContinuousLinearEquiv.continuous_invFun._autoParam),
  ({ toLinearEquiv := toLinearEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toLinearEquiv := toLinearEquiv_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 }) =
    (toLinearEquiv = toLinearEquiv_1)