-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_5 : RingHomInvPair σ₂₃ σ₃₂
inst_6 : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_7 : RingHomInvPair σ₁₃ σ₃₁
inst_8 : RingHomInvPair σ₃₁ σ₁₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_11 : TopologicalSpace M₁
inst_12 : AddCommMonoid M₁
M₂ : Type u_5
inst_13 : TopologicalSpace M₂
inst_14 : AddCommMonoid M₂
M₃ : Type u_6
inst_15 : TopologicalSpace M₃
inst_16 : AddCommMonoid M₃
M₄ : Type u_7
inst_17 : TopologicalSpace M₄
inst_18 : AddCommMonoid M₄
inst_19 : Module R₁ M₁
inst_20 : Module R₂ M₂
inst_21 : Module R₃ M₃
f' : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun : Continuous[inst_11, inst_13] (↑f' : M₁ →ₛₗ[σ₁₂] M₂).toFun
continuous_invFun : Continuous[inst_13, inst_11] f'.invFun
g' : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun_1 : Continuous[inst_11, inst_13] (↑g' : M₁ →ₛₗ[σ₁₂] M₂).toFun
continuous_invFun_1 : Continuous[inst_13, inst_11] g'.invFun
h₁ :
  (↑(↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂) :
        M₁ →ₛₗ[σ₁₂] M₂).toFun =
    (↑(↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂) :
        M₁ →ₛₗ[σ₁₂] M₂).toFun
h₂ :
  (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            M₁ ≃SL[σ₁₂] M₂ } :
        M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
    (↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
            M₁ ≃SL[σ₁₂] M₂ } :
        M₁ ≃ₛₗ[σ₁₂] M₂).invFun
rcases :
  ∀ (invFun : M₂ → M₁) (toFun : M₁ → M₂) (map_add' : ∀ (x y : M₁), toFun (x + y) = toFun x + toFun y)
    (map_smul' :
      ∀ (m : R₁) (x : M₁),
        { toFun := toFun, map_add' := map_add' : M₁ →ₙ+ M₂ }.toFun (m • x) =
          HSMul.hSMul.{u_2, u_5, u_5} (α := R₂) ((σ₁₂ : (a : R₁) → R₂) m : R₂)
            ({ toFun := toFun, map_add' := map_add' : M₁ →ₙ+ M₂ }.toFun x))
    (left_inv :
      Function.LeftInverse invFun
        { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : M₁ →ₛₗ[σ₁₂] M₂ }.toFun)
    (right_inv :
      Function.RightInverse invFun
        { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : M₁ →ₛₗ[σ₁₂] M₂ }.toFun)
    (continuous_toFun :
      Continuous[inst_11, inst_13]
        (↑{ toFun := toFun, map_add' := map_add', map_smul' := map_smul', invFun := invFun, left_inv := left_inv,
                right_inv := right_inv : M₁ ≃ₛₗ[σ₁₂] M₂ } :
            M₁ →ₛₗ[σ₁₂] M₂).toFun)
    (continuous_invFun :
      Continuous[inst_13, inst_11]
        (LinearEquiv.invFun
          { toFun := toFun, map_add' := map_add', map_smul' := map_smul', invFun := invFun, left_inv := left_inv,
            right_inv := right_inv : M₁ ≃ₛₗ[σ₁₂] M₂ }))
    (h₁ :
      (↑(↑{ toFun := toFun, map_add' := map_add', map_smul' := map_smul', invFun := invFun, left_inv := left_inv,
                    right_inv := right_inv, continuous_toFun := continuous_toFun,
                    continuous_invFun := continuous_invFun : M₁ ≃SL[σ₁₂] M₂ } :
                M₁ ≃ₛₗ[σ₁₂] M₂) :
            M₁ →ₛₗ[σ₁₂] M₂).toFun =
        (↑(↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
                    M₁ ≃SL[σ₁₂] M₂ } :
                M₁ ≃ₛₗ[σ₁₂] M₂) :
            M₁ →ₛₗ[σ₁₂] M₂).toFun)
    (h₂ :
      (↑{ toFun := toFun, map_add' := map_add', map_smul' := map_smul', invFun := invFun, left_inv := left_inv,
                right_inv := right_inv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
        (↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂).invFun),
    { toFun := toFun, map_add' := map_add', map_smul' := map_smul', invFun := invFun, left_inv := left_inv,
        right_inv := right_inv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M₁ ≃SL[σ₁₂] M₂ } =
      { toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }
⊢ { toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
      M₁ ≃SL[σ₁₂] M₂ } =
    { toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }

Tactic:
rcases f' with ⟨⟨⟨_, _⟩, _⟩, _⟩