-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : 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 : A₁ ≃ A₂ }.toFun (x * y) =
      { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun x *
        { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun y
map_add' :
  ∀ (x y : A₁),
    { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun (x + y) =
      { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun x +
        { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun y
commutes' :
  ∀ (r : R),
    { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun
        ((algebraMap R A₁ : (a : R) → A₁) r) =
      (algebraMap R A₂ : (a : 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' : A₁ ≃ₐ[R] A₂ }.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' : A₁ ≃ₐ[R] A₂ }.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' : A₁ ≃ₐ[R] A₂ } =
    g
have obtain : ∀ (g : A₁ → A₂) (invFun_1 : A₂ → A₁) (left_inv_1 : Function.LeftInverse invFun_1 g)
  (right_inv_1 : Function.RightInverse invFun_1 g)
  (map_mul'_1 :
    ∀ (x y : A₁),
      { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A₁ ≃ A₂ }.toFun (x * y) =
        { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A₁ ≃ A₂ }.toFun x *
          { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A₁ ≃ A₂ }.toFun y)
  (map_add'_1 :
    ∀ (x y : A₁),
      { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A₁ ≃ A₂ }.toFun (x + y) =
        { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A₁ ≃ A₂ }.toFun x +
          { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A₁ ≃ A₂ }.toFun y)
  (commutes'_1 :
    ∀ (r : R),
      { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A₁ ≃ A₂ }.toFun
          ((algebraMap R A₁ : (a : R) → A₁) r) =
        (algebraMap R A₂ : (a : 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' : A₁ ≃ₐ[R] A₂ }.toFun =
      { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
          map_add' := map_add'_1, commutes' := commutes'_1 : A₁ ≃ₐ[R] A₂ }.toFun)
  (h₂ :
    { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', commutes' := commutes' : A₁ ≃ₐ[R] A₂ }.invFun =
      { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
          map_add' := map_add'_1, commutes' := commutes'_1 : A₁ ≃ₐ[R] A₂ }.invFun),
  { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
      map_add' := map_add', commutes' := commutes' : A₁ ≃ₐ[R] A₂ } =
    { toFun := g, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
      map_add' := map_add'_1, commutes' := commutes'_1 }
Tactic: obtain ⟨⟨g, _⟩, _⟩ := g
Cleared hypotheses: g, h₁, h₂