-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
inst_6 : Mul γ
inst_7 : Add γ
inst_8 : LE γ
g : α ≃+*o β
toFun : α → β
invFun : β → α
left_inv : LeftInverse invFun toFun
right_inv : RightInverse invFun toFun
map_mul' :
  ∀ (x y : α),
    { 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 : α),
    { 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_le_map_iff' :
  ∀ {a b : α},
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
              map_add' := map_add' : α ≃+* β }.toFun
          a ≤
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
              map_add' := map_add' : α ≃+* β }.toFun
          b ↔
      a ≤ b
h₁ :
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
        map_add' := map_add', map_le_map_iff' := @map_le_map_iff' : α ≃+*o β }.toFun =
    g.toFun
h₂ :
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
        map_add' := map_add', map_le_map_iff' := @map_le_map_iff' : α ≃+*o β }.invFun =
    g.invFun
⊢ { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
      map_add' := map_add', map_le_map_iff' := @map_le_map_iff' : α ≃+*o β } =
    g
have obtain : ∀ (toFun_1 : α → β) (invFun_1 : β → α) (left_inv_1 : LeftInverse invFun_1 toFun_1)
  (right_inv_1 : RightInverse invFun_1 toFun_1)
  (map_mul'_1 :
    ∀ (x y : α),
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : α ≃ β }.toFun (x * y) =
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : α ≃ β }.toFun x *
          { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : α ≃ β }.toFun y)
  (map_add'_1 :
    ∀ (x y : α),
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : α ≃ β }.toFun (x + y) =
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : α ≃ β }.toFun x +
          { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : α ≃ β }.toFun y)
  (map_le_map_iff'_1 :
    ∀ {a b : α},
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
                map_add' := map_add'_1 : α ≃+* β }.toFun
            a ≤
          { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1,
                map_mul' := map_mul'_1, map_add' := map_add'_1 : α ≃+* β }.toFun
            b ↔
        a ≤ b)
  (h₁ :
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', map_le_map_iff' := @map_le_map_iff' : α ≃+*o β }.toFun =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
          map_add' := map_add'_1, map_le_map_iff' := @map_le_map_iff'_1 : α ≃+*o β }.toFun)
  (h₂ :
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', map_le_map_iff' := @map_le_map_iff' : α ≃+*o β }.invFun =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
          map_add' := map_add'_1, map_le_map_iff' := @map_le_map_iff'_1 : α ≃+*o β }.invFun),
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
      map_add' := map_add', map_le_map_iff' := @map_le_map_iff' : α ≃+*o β } =
    { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
      map_add' := map_add'_1, map_le_map_iff' := @map_le_map_iff'_1 }
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
Cleared hypotheses: g, h₁, h₂