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
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✝¹ }

Tactic:
rcases g' 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
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
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 =
    { 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
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 =
    { 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
⊢ { 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 := 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✝ }