Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring B
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring C
inst✝³ : TopologicalSpace C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f' : A ≃ₐ[R] B
continuous_toFun✝¹ : Continuous[inst✝⁷, inst✝⁵] f'.toFun
continuous_invFun✝¹ : Continuous[inst✝⁵, inst✝⁷] f'.invFun
g' : A ≃ₐ[R] B
continuous_toFun✝ : Continuous[inst✝⁷, inst✝⁵] g'.toFun
continuous_invFun✝ : Continuous[inst✝⁵, inst✝⁷] g'.invFun
h₁ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.toFun =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toFun
h₂ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.invFun =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.invFun
⊢ { toAlgEquiv := f', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ } =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }

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

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring B
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring C
inst✝³ : TopologicalSpace C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
g' : A ≃ₐ[R] B
continuous_toFun✝¹ : Continuous[inst✝⁷, inst✝⁵] g'.toFun
continuous_invFun✝¹ : Continuous[inst✝⁵, inst✝⁷] g'.invFun
toFun✝ : A → B
invFun✝ : B → A
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : A),
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x * y) =
      { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x *
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
map_add'✝ :
  ∀ (x y : A),
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x + y) =
      { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x +
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
commutes'✝ :
  ∀ (r : R),
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun ((algebraMap R A) r) =
      (algebraMap R B) r
continuous_toFun✝ :
  Continuous[inst✝⁷, inst✝⁵]
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝ }.toFun
continuous_invFun✝ :
  Continuous[inst✝⁵, inst✝⁷]
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝ }.invFun
h₁ :
  { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝, continuous_toFun := continuous_toFun✝,
        continuous_invFun := continuous_invFun✝ }.toFun =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.toFun
h₂ :
  { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝, continuous_toFun := continuous_toFun✝,
        continuous_invFun := continuous_invFun✝ }.invFun =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.invFun
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
      map_add' := map_add'✝, commutes' := commutes'✝, continuous_toFun := continuous_toFun✝,
      continuous_invFun := continuous_invFun✝ } =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }