Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : Mul γ
inst✝ : Mul δ
f g✝ 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_le_map_iff'✝ :
  ∀ {a b : α},
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝ }.toFun
          a ≤
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝,
              map_mul' := map_mul'✝ }.toFun
          b ↔
      a ≤ b
h₁ :
  { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_le_map_iff' := map_le_map_iff'✝ }.toFun =
    g.toFun
h₂ :
  { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_le_map_iff' := map_le_map_iff'✝ }.invFun =
    g.invFun
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
      map_le_map_iff' := map_le_map_iff'✝ } =
    g

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

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : Mul γ
inst✝ : Mul δ
f 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_le_map_iff'✝¹ :
  ∀ {a b : α},
    { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹,
              map_mul' := map_mul'✝¹ }.toFun
          a ≤
        { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹,
              map_mul' := map_mul'✝¹ }.toFun
          b ↔
      a ≤ b
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_le_map_iff'✝ :
  ∀ {a b : α},
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝ }.toFun
          a ≤
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝,
              map_mul' := map_mul'✝ }.toFun
          b ↔
      a ≤ b
h₁ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
        map_le_map_iff' := map_le_map_iff'✝¹ }.toFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_le_map_iff' := map_le_map_iff'✝ }.toFun
h₂ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
        map_le_map_iff' := map_le_map_iff'✝¹ }.invFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_le_map_iff' := map_le_map_iff'✝ }.invFun
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
      map_le_map_iff' := map_le_map_iff'✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
      map_le_map_iff' := map_le_map_iff'✝ }