Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
g : M₁ ≃SL[σ₁₂] M₂
f' : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun✝ : Continuous[inst✝¹⁰, inst✝⁸] (↑f').toFun
continuous_invFun✝ : Continuous[inst✝⁸, inst✝¹⁰] f'.invFun
h₁ :
  (↑↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }).toFun =
    (↑↑g).toFun
h₂ :
  (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }).invFun =
    (↑g).invFun
⊢ { toLinearEquiv := f', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ } = g

Tactic:
obtain ⟨g', _⟩ := g

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f' : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun✝¹ : Continuous[inst✝¹⁰, inst✝⁸] (↑f').toFun
continuous_invFun✝¹ : Continuous[inst✝⁸, inst✝¹⁰] f'.invFun
g' : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun✝ : Continuous[inst✝¹⁰, inst✝⁸] (↑g').toFun
continuous_invFun✝ : Continuous[inst✝⁸, inst✝¹⁰] g'.invFun
h₁ :
  (↑↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }).toFun =
    (↑↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }).toFun
h₂ :
  (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }).invFun =
    (↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }).invFun
⊢ { toLinearEquiv := f', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ } =
    { toLinearEquiv := g', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }