-- 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₃
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₂ })
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_1 :
  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_1 :
  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, continuous_invFun := continuous_invFun :
                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_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 =
    (↑{ 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_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₂ } =
    { 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_1, continuous_invFun := continuous_invFun_1 }

Tactic:
congr