Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e g : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ f
right_inv✝ : Function.RightInverse invFun✝ f
map_mul'✝ :
  ∀ (x y : A₁),
    { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x * y) =
      { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x *
        { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
map_add'✝ :
  ∀ (x y : A₁),
    { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x + y) =
      { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x +
        { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
commutes'✝ :
  ∀ (r : R),
    { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun ((algebraMap R A₁) r) =
      (algebraMap R A₂) r
h₁ :
  { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝ }.toFun =
    g.toFun
h₂ :
  { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝ }.invFun =
    g.invFun
⊢ { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
      map_add' := map_add'✝, commutes' := commutes'✝ } =
    g

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

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝¹ : A₂ → A₁
left_inv✝¹ : Function.LeftInverse invFun✝¹ f
right_inv✝¹ : Function.RightInverse invFun✝¹ f
map_mul'✝¹ :
  ∀ (x y : A₁),
    { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun (x * y) =
      { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun x *
        { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun y
map_add'✝¹ :
  ∀ (x y : A₁),
    { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun (x + y) =
      { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun x +
        { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun y
commutes'✝¹ :
  ∀ (r : R),
    { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun ((algebraMap R A₁) r) =
      (algebraMap R A₂) r
g : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ g
right_inv✝ : Function.RightInverse invFun✝ g
map_mul'✝ :
  ∀ (x y : A₁),
    { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x * y) =
      { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x *
        { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
map_add'✝ :
  ∀ (x y : A₁),
    { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x + y) =
      { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x +
        { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
commutes'✝ :
  ∀ (r : R),
    { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun ((algebraMap R A₁) r) =
      (algebraMap R A₂) r
h₁ :
  { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
        map_add' := map_add'✝¹, commutes' := commutes'✝¹ }.toFun =
    { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝ }.toFun
h₂ :
  { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
        map_add' := map_add'✝¹, commutes' := commutes'✝¹ }.invFun =
    { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝ }.invFun
⊢ { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
      map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
      map_add' := map_add'✝, commutes' := commutes'✝ }