awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ Eq (α := (a : α) → β) (⇑(↑f : α →o β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f g : α ≃*o β
h : f.toMulEquiv = g.toMulEquiv
⊢ ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f.toMulEquiv : (a : α) → β) x : β) ((g.toMulEquiv : (a : α) → β) x : β)

Tactic:
DFunLike.ext_iff.1 h

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f g : α ≃*o β
h : f.toMulEquiv = g.toMulEquiv
⊢ ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
convert! DFunLike.ext_iff.1 h using 0

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f g : α ≃*o β
h : f.toOrderIso = g.toOrderIso
⊢ ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f.toOrderIso : (a : α) → β) x : β) ((g.toOrderIso : (a : α) → β) x : β)

Tactic:
DFunLike.ext_iff.1 h

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f g : α ≃*o β
h : f.toOrderIso = g.toOrderIso
⊢ ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
convert! DFunLike.ext_iff.1 h using 0

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
inst_4 : Mul α
inst_5 : Mul β
inst_6 : Mul γ
inst_7 : Mul δ
f g : α ≃*o β
⊢ ∀ {a b : α}, (MulEquiv.toEquiv (MulEquiv.refl α)).toFun a ≤ (MulEquiv.toEquiv (MulEquiv.refl α)).toFun b ↔ a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Mul α
⊢ Eq (α := (a : α) → α) (⇑(OrderMonoidIso.refl α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
inst_4 : Mul α
inst_5 : Mul β
inst_6 : Mul γ
inst_7 : Mul δ
f_1 g_1 f : α ≃*o β
g : β ≃*o γ
⊢ ∀ {a b : α},
    (MulEquiv.toEquiv (MulEquiv.trans (↑f : α ≃* β) (↑g : β ≃* γ))).toFun a ≤
        (MulEquiv.toEquiv (MulEquiv.trans (↑f : α ≃* β) (↑g : β ≃* γ))).toFun b ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Mul α
inst_4 : Mul β
inst_5 : Mul γ
f : α ≃*o β
g : β ≃*o γ
⊢ Eq (α := (a : α) → γ) (⇑(f.trans g) : (a : α) → γ)
    (comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Mul α
inst_4 : Mul β
inst_5 : Mul γ
f : α ≃*o β
g : β ≃*o γ
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.trans g : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Mul α
inst_4 : Mul β
inst_5 : Mul γ
f : α ≃*o β
g : β ≃*o γ
⊢ Eq (α := α ≃* γ) (↑(f.trans g) : α ≃* γ) (MulEquiv.trans (↑f : α ≃* β) (↑g : β ≃* γ))

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.trans, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Mul α
inst_4 : Mul β
inst_5 : Mul γ
f : α ≃*o β
g : β ≃*o γ
⊢ Eq (α := α ≃o γ) (↑(f.trans g) : α ≃o γ) (OrderIso.trans (↑f : α ≃o β) (↑g : β ≃o γ))

Tactic:
rfl

Premises used: Equiv.trans, RelIso.trans, rfl, OrderIso.trans
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
inst_4 : Mul α
inst_5 : Mul β
inst_6 : Mul γ
inst_7 : Mul δ
f : α ≃*o β
g : β ≃*o γ
h : γ ≃*o δ
⊢ (f.trans g).trans h = f.trans (g.trans h)

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.trans, OrderMonoidIso.trans, MulEquivClass.toMulEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ f.trans (OrderMonoidIso.refl β) = f

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.trans, OrderMonoidIso.trans, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ trans (OrderMonoidIso.refl α) f = f

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.trans, OrderMonoidIso.trans, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Mul α
inst_4 : Mul β
inst_5 : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑f : (a : β) → γ)
h : g₁.trans f = g₂.trans f
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g₁.trans f : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g₂.trans f : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← trans_apply, h, trans_apply]

Premises used: OrderMonoidIso.trans_apply
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Mul α
inst_4 : Mul β
inst_5 : Mul γ
g₁ : α ≃*o β
f : β ≃*o γ
hf : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑f : (a : β) → γ)
⊢ g₁.trans f = g₁.trans f

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Mul α
inst_4 : Mul β
inst_5 : Mul γ
g : α ≃*o β
f₁ f₂ : β ≃*o γ
hg : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑g : (a : α) → β)
h : f₁ = f₂
⊢ g.trans f₁ = g.trans f₂

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ f.toMulEquiv = (↑f : α ≃* β)

Tactic:
rfl

Premises used: MulEquivClass.toMulEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ f.toOrderIso = (↑f : α ≃o β)

Tactic:
rfl

Premises used: OrderMonoidIso.toOrderIso, OrderIsoClass.toOrderIso, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ f.invFun = (⇑f.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ Eq (α := (a : β) → α) (⇑(↑f : α ≃ β).symm : (a : β) → α) (⇑f.symm : (a : β) → α)

Tactic:
rfl

Premises used: EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ EquivLike.inv f = (⇑f.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ (↑f.symm : β ≃ α) = (↑f : α ≃ β).symm

Tactic:
rfl

Premises used: Equiv.symm, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ f.symm.symm = f

Tactic:
rfl

Premises used: OrderMonoidIso.symm, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
⊢ Bijective (α := α ≃*o β) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, OrderMonoidIso.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Mul α
⊢ Eq (α := α ≃*o α) (symm (OrderMonoidIso.refl α)) (OrderMonoidIso.refl α)

Tactic:
rfl

Premises used: MulEquiv.refl, OrderMonoidIso.refl, OrderMonoidIso.symm, Equiv.symm, MulEquiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
y : β
⊢ (e : (a : α) → β) ((e.symm : (a : β) → α) y : α) = y

Tactic:
e.toEquiv.apply_symm_apply y

Premises used: Equiv.apply_symm_apply, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
x : α
⊢ (e.symm : (a : β) → α) ((e : (a : α) → β) x : β) = x

Tactic:
e.toEquiv.symm_apply_apply x

Premises used: Equiv.symm_apply_apply, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
⊢ Eq.{u_2 + 1} (α := α → α) (comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) id

Tactic:
funext e.symm_apply_apply

Premises used: OrderMonoidIso.symm_apply_apply, funext
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
⊢ Eq.{u_3 + 1} (α := β → β) (comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) id

Tactic:
funext e.apply_symm_apply

Premises used: OrderMonoidIso.apply_symm_apply, funext
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
x : α
y : β
⊢ (e : (a : α) → β) x = y ↔ x = (e.symm : (a : β) → α) y

Tactic:
e.toEquiv.apply_eq_iff_eq_symm_apply

Premises used: MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
x : β
y : α
⊢ (e.symm : (a : β) → α) x = y ↔ x = (e : (a : α) → β) y

Tactic:
e.toEquiv.symm_apply_eq

Premises used: Equiv.symm_apply_eq, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
x : β
y : α
⊢ y = (e.symm : (a : β) → α) x ↔ (e : (a : α) → β) y = x

Tactic:
e.toEquiv.eq_symm_apply

Premises used: MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv, Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
f : β → α
g : α → α
⊢ f = g ∘ (⇑e.symm : (a : β) → α) ↔ f ∘ (⇑e : (a : α) → β) = g

Tactic:
e.toEquiv.eq_comp_symm f g

Premises used: MulEquiv.toEquiv, Equiv.eq_comp_symm, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
f : β → α
g : α → α
⊢ g ∘ (⇑e.symm : (a : β) → α) = f ↔ g = f ∘ (⇑e : (a : α) → β)

Tactic:
e.toEquiv.comp_symm_eq f g

Premises used: MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv, Equiv.comp_symm_eq
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
f : α → α
g : α → β
⊢ f = (⇑e.symm : (a : β) → α) ∘ g ↔ (⇑e : (a : α) → β) ∘ f = g

Tactic:
e.toEquiv.eq_symm_comp f g

Premises used: Equiv.eq_symm_comp, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
f : α → α
g : α → β
⊢ (⇑e.symm : (a : β) → α) ∘ g = f ↔ g = (⇑e : (a : α) → β) ∘ f

Tactic:
e.toEquiv.symm_comp_eq f g

Premises used: Equiv.symm_comp_eq, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
x : α
y : β
⊢ x < (e.symm : (a : β) → α) y ↔ (e : (a : α) → β) x < y

Tactic:
e.toOrderIso.lt_symm_apply

Premises used: OrderMonoidIso.toOrderIso, OrderIso.lt_symm_apply
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
e : α ≃*o β
x : α
y : β
⊢ (e.symm : (a : β) → α) y < x ↔ y < (e : (a : α) → β) x

Tactic:
e.toOrderIso.symm_apply_lt

Premises used: OrderMonoidIso.toOrderIso, OrderIso.symm_apply_lt
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
strictMono_of_le_iff_le fun _ _ ↦ (map_le_map_iff _).symm

Premises used: OrderIsoClass.map_le_map_iff, strictMono_of_le_iff_le, Iff.symm
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
a b : β
rw :
  a ≤ b ↔
    LE.le.{u_3} (α := β) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β)
      ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β)
⊢ a ≤ b ↔ LE.le.{u_2} (α := α) ((f.symm : (a : β) → α) a : α) ((f.symm : (a : β) → α) b : α)

Tactic:
rw [← map_le_map_iff f]

Premises used: OrderIsoClass.map_le_map_iff
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
a b : β
h : (f : (a : α) → β) ((f.symm : (a : β) → α) a : α) = a
h₁ : (f : (a : α) → β) ((f.symm : (a : β) → α) b : α) = b
⊢ a ≤ b ↔
    LE.le.{u_3} (α := β) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β)
      ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β)

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
a b : β
⊢ (f : (a : α) → β) ((f.symm : (a : β) → α) a : α) = a

Tactic:
f.toEquiv.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
a b : β
⊢ (f : (a : α) → β) ((f.symm : (a : β) → α) a : α) = a

Tactic:
exact f.toEquiv.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
a b : β
⊢ (f : (a : α) → β) ((f.symm : (a : β) → α) b : α) = b

Tactic:
f.toEquiv.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
a b : β
⊢ (f : (a : α) → β) ((f.symm : (a : β) → α) b : α) = b

Tactic:
exact f.toEquiv.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
inst_4 : MulZeroOneClass α
inst_5 : MulZeroOneClass β
inst_6 : MulZeroOneClass γ
inst_7 : MulZeroOneClass δ
f_1 g_1 f g : α →*₀o β
h :
  Eq (α := (a : α) → β) ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun) f)
    ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun) g)
obtain :
  ∀ (toFun : α → β) (map_zero' : toFun 0 = 0)
    (map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun 1 = 1)
    (map_mul' :
      ∀ (x y : α),
        { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun (x * y) =
          { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun x *
            { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun y)
    (monotone' :
      Monotone
        (↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : α →*₀ β } :
            ZeroHom α β).toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun)
          { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul',
            monotone' := monotone' })
        ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun) g)),
    { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul', monotone' := monotone' :
        α →*₀o β } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
inst_4 : MulZeroOneClass α
inst_5 : MulZeroOneClass β
inst_6 : MulZeroOneClass γ
inst_7 : MulZeroOneClass δ
f g_1 g : α →*₀o β
toFun : α → β
map_zero' : toFun 0 = 0
map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun 1 = 1
map_mul' :
  ∀ (x y : α),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun (x * y) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun x *
        { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun y
monotone' :
  Monotone
    (↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : α →*₀ β } :
        ZeroHom α β).toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun)
      { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul', monotone' := monotone' })
    ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (map_zero'_1 : toFun_1 0 = 0)
    (map_one'_1 : { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun 1 = 1)
    (map_mul'_1 :
      ∀ (x y : α),
        { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun (x * y) =
          { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun x *
            { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun y)
    (monotone'_1 :
      Monotone
        (↑{ toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : α →*₀ β } :
            ZeroHom α β).toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun)
          { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul',
            monotone' := monotone' })
        ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun)
          { toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1,
            monotone' := monotone'_1 })),
    { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul', monotone' := monotone' :
        α →*₀o β } =
      { toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1,
        monotone' := monotone'_1 }
⊢ { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul', monotone' := monotone' :
      α →*₀o β } =
    g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
inst_4 : MulZeroOneClass α
inst_5 : MulZeroOneClass β
inst_6 : MulZeroOneClass γ
inst_7 : MulZeroOneClass δ
f g : α →*₀o β
toFun : α → β
map_zero' : toFun 0 = 0
map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun 1 = 1
map_mul' :
  ∀ (x y : α),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun (x * y) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun x *
        { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun y
monotone' :
  Monotone
    (↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : α →*₀ β } :
        ZeroHom α β).toFun
toFun_1 : α → β
map_zero'_1 : toFun_1 0 = 0
map_one'_1 : { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun 1 = 1
map_mul'_1 :
  ∀ (x y : α),
    { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun (x * y) =
      { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun x *
        { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun y
monotone'_1 :
  Monotone
    (↑{ toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : α →*₀ β } :
        ZeroHom α β).toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun)
      { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul', monotone' := monotone' })
    ((fun (f : α →*₀o β) ↦ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun)
      { toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1,
        monotone' := monotone'_1 })
⊢ { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul', monotone' := monotone' :
      α →*₀o β } =
    { toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1,
      monotone' := monotone'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulZeroOneClass α
inst_3 : MulZeroOneClass β
f g : α →*₀o β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulZeroOneClass α
inst_3 : MulZeroOneClass β
f : α →*₀o β
⊢ (↑f.toMonoidWithZeroHom : ZeroHom α β).toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulZeroOneClass α
inst_3 : MulZeroOneClass β
f : α →*₀ β
h : Monotone (↑f : ZeroHom α β).toFun
⊢ Eq (α := (a : α) → β) (⇑{ toMonoidWithZeroHom := f, monotone' := h : α →*₀o β } : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl