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₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun✝¹ : Continuous[inst✝¹⁰, inst✝⁸] (↑g').toFun
continuous_invFun✝¹ : Continuous[inst✝⁸, inst✝¹⁰] 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'✝ }.toFun (m • x) =
      σ₁₂ m • { toFun := toFun✝, map_add' := map_add'✝ }.toFun x
left_inv✝ : Function.LeftInverse invFun✝ { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun
right_inv✝ : Function.RightInverse invFun✝ { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun
continuous_toFun✝ :
  Continuous[inst✝¹⁰, inst✝⁸]
    (↑{ toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝, invFun := invFun✝, left_inv := left_inv✝,
          right_inv := right_inv✝ }).toFun
continuous_invFun✝ :
  Continuous[inst✝⁸, inst✝¹⁰]
    { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.invFun
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✝ }).toFun =
    (↑↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }).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✝ }).invFun =
    (↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }).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✝ } =
    { toLinearEquiv := g', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }

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

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₃
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'✝¹ }.toFun (m • x) =
      σ₁₂ m • { toFun := toFun✝¹, map_add' := map_add'✝¹ }.toFun x
left_inv✝¹ : Function.LeftInverse invFun✝¹ { toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun
right_inv✝¹ :
  Function.RightInverse invFun✝¹ { toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun
continuous_toFun✝¹ :
  Continuous[inst✝¹⁰, inst✝⁸]
    (↑{ toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
          right_inv := right_inv✝¹ }).toFun
continuous_invFun✝¹ :
  Continuous[inst✝⁸, inst✝¹⁰]
    { toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
        right_inv := right_inv✝¹ }.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'✝ }.toFun (m • x) =
      σ₁₂ m • { toFun := toFun✝, map_add' := map_add'✝ }.toFun x
left_inv✝ : Function.LeftInverse invFun✝ { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun
right_inv✝ : Function.RightInverse invFun✝ { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun
continuous_toFun✝ :
  Continuous[inst✝¹⁰, inst✝⁸]
    (↑{ toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝, invFun := invFun✝, left_inv := left_inv✝,
          right_inv := right_inv✝ }).toFun
continuous_invFun✝ :
  Continuous[inst✝⁸, inst✝¹⁰]
    { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.invFun
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✝¹ }).toFun =
    (↑↑{ 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✝ }).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✝¹ }).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✝ }).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✝¹ } =
    { 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✝ }