-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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₃
g' : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun : Continuous[inst_11, inst_13] (↑g' : M₁ →ₛₗ[σ₁₂] M₂).toFun
continuous_invFun : Continuous[inst_13, inst_11] g'.invFun
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_1 :
  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_1 :
  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_1,
                continuous_invFun := continuous_invFun_1 : M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂) :
        M₁ →ₛₗ[σ₁₂] M₂).toFun =
    (↑(↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                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_1, continuous_invFun := continuous_invFun_1 :
            M₁ ≃SL[σ₁₂] M₂ } :
        M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
    (↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            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_1, continuous_invFun := continuous_invFun_1 :
      M₁ ≃SL[σ₁₂] M₂ } =
    { toLinearEquiv := g', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun }
have rcases : ∀ (invFun_1 : M₂ → M₁) (toFun_1 : M₁ → M₂) (map_add'_1 : ∀ (x y : M₁), toFun_1 (x + y) = toFun_1 x + toFun_1 y)
  (map_smul'_1 :
    ∀ (m : R₁) (x : M₁),
      { toFun := toFun_1, map_add' := map_add'_1 : M₁ →ₙ+ M₂ }.toFun (m • x) =
        HSMul.hSMul.{u_2, u_5, u_5} (α := R₂) ((σ₁₂ : (a : R₁) → R₂) m : R₂)
          ({ toFun := toFun_1, map_add' := map_add'_1 : M₁ →ₙ+ M₂ }.toFun x))
  (left_inv_1 :
    Function.LeftInverse invFun_1
      { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : M₁ →ₛₗ[σ₁₂] M₂ }.toFun)
  (right_inv_1 :
    Function.RightInverse invFun_1
      { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : M₁ →ₛₗ[σ₁₂] M₂ }.toFun)
  (continuous_toFun :
    Continuous[inst_11, inst_13]
      (↑{ toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, invFun := invFun_1,
              left_inv := left_inv_1, right_inv := right_inv_1 : M₁ ≃ₛₗ[σ₁₂] M₂ } :
          M₁ →ₛₗ[σ₁₂] M₂).toFun)
  (continuous_invFun :
    Continuous[inst_13, inst_11]
      (LinearEquiv.invFun
        { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, invFun := invFun_1,
          left_inv := left_inv_1, right_inv := right_inv_1 : 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_1,
                  continuous_invFun := continuous_invFun_1 : M₁ ≃SL[σ₁₂] M₂ } :
              M₁ ≃ₛₗ[σ₁₂] M₂) :
          M₁ →ₛₗ[σ₁₂] M₂).toFun =
      (↑(↑{ toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, invFun := invFun_1,
                  left_inv := left_inv_1, right_inv := right_inv_1, continuous_toFun := continuous_toFun,
                  continuous_invFun := continuous_invFun : 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_1, continuous_invFun := continuous_invFun_1 :
              M₁ ≃SL[σ₁₂] M₂ } :
          M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
      (↑{ toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, invFun := invFun_1,
              left_inv := left_inv_1, right_inv := right_inv_1, continuous_toFun := continuous_toFun,
              continuous_invFun := continuous_invFun : 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_1, continuous_invFun := continuous_invFun_1 :
      M₁ ≃SL[σ₁₂] M₂ } =
    { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, invFun := invFun_1, left_inv := left_inv_1,
      right_inv := right_inv_1, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun }
Tactic: rcases g' with ⟨⟨⟨_, _⟩, _⟩, _⟩
Cleared hypotheses: g', continuous_toFun, continuous_invFun, h₁, h₂