awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
⊢ StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (a : α), a < 0 → LT.lt.{u_3} (α := β) ((f : (a : α) → β) a : β) (0 : β)

Tactic:
strictAnti_comp_ofDual_iff.symm.trans <| strictAnti_iff_map_neg (α := αᵒᵈ) (iamhc := iamhc) _

Premises used: strictAnti_iff_map_neg, Iff.trans, Iff.symm, strictAnti_comp_ofDual_iff
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
⊢ StrictAnti.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (a : α), a < 0 → LT.lt.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)

Tactic:
strictMono_comp_ofDual_iff.symm.trans <| strictMono_iff_map_pos (α := αᵒᵈ) (iamhc := iamhc) _

Premises used: strictMono_iff_map_pos, strictMono_comp_ofDual_iff, Iff.trans, Iff.symm
-- 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 : MulOneClass α
inst_5 : MulOneClass β
inst_6 : MulOneClass γ
inst_7 : MulOneClass δ
f_1 g_1 f g : α →*o β
h :
  Eq (α := (a : α) → β) ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) f)
    ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)
obtain :
  ∀ (toFun : α → β) (map_one' : toFun 1 = 1)
    (map_mul' :
      ∀ (x y : α),
        { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun (x * y) =
          { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun x *
            { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun y)
    (monotone' : Monotone (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : α →* β } : OneHom α β).toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
          { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' })
        ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)),
    { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' : α →*o β } = g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
-- 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 : MulOneClass α
inst_5 : MulOneClass β
inst_6 : MulOneClass γ
inst_7 : MulOneClass δ
f g_1 g : α →*o β
toFun : α → β
map_one' : toFun 1 = 1
map_mul' :
  ∀ (x y : α),
    { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun (x * y) =
      { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun x *
        { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun y
monotone' : Monotone (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : α →* β } : OneHom α β).toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' })
    ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (map_one'_1 : toFun_1 1 = 1)
    (map_mul'_1 :
      ∀ (x y : α),
        { toFun := toFun_1, map_one' := map_one'_1 : OneHom α β }.toFun (x * y) =
          { toFun := toFun_1, map_one' := map_one'_1 : OneHom α β }.toFun x *
            { toFun := toFun_1, map_one' := map_one'_1 : OneHom α β }.toFun y)
    (monotone'_1 :
      Monotone (↑{ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : α →* β } : OneHom α β).toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
          { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' })
        ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
          { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, monotone' := monotone'_1 })),
    { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' : α →*o β } =
      { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, monotone' := monotone'_1 }
⊢ { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' : α →*o β } = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
-- 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 : MulOneClass α
inst_5 : MulOneClass β
inst_6 : MulOneClass γ
inst_7 : MulOneClass δ
f g : α →*o β
toFun : α → β
map_one' : toFun 1 = 1
map_mul' :
  ∀ (x y : α),
    { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun (x * y) =
      { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun x *
        { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun y
monotone' : Monotone (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : α →* β } : OneHom α β).toFun
toFun_1 : α → β
map_one'_1 : toFun_1 1 = 1
map_mul'_1 :
  ∀ (x y : α),
    { toFun := toFun_1, map_one' := map_one'_1 : OneHom α β }.toFun (x * y) =
      { toFun := toFun_1, map_one' := map_one'_1 : OneHom α β }.toFun x *
        { toFun := toFun_1, map_one' := map_one'_1 : OneHom α β }.toFun y
monotone'_1 :
  Monotone (↑{ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : α →* β } : OneHom α β).toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' })
    ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, monotone' := monotone'_1 })
⊢ { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' : α →*o β } =
    { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, monotone' := monotone'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulOneClass α
inst_3 : MulOneClass β
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.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulOneClass α
inst_3 : MulOneClass β
f : α →*o β
⊢ (↑f.toMonoidHom : OneHom α β).toFun = (⇑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 : MulOneClass α
inst_3 : MulOneClass β
f : α →* β
h : Monotone (↑f : OneHom α β).toFun
⊢ Eq (α := (a : α) → β) (⇑{ toMonoidHom := f, monotone' := h : α →*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 : MulOneClass α
inst_3 : MulOneClass β
f : α →*o β
h : Monotone (OneHom.toFun (↑(↑f : α →* β) : OneHom α β))
h₁ :
  ∀ (a : α),
    Eq.{u_3 + 1} (α := β) (({ toMonoidHom := (↑f : α →* β), monotone' := h : α →*o β } : (a : α) → β) a : β)
      ((f : (a : α) → β) a : β)
⊢ { toMonoidHom := (↑f : α →* β), monotone' := h : α →*o β } = f

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulOneClass α
inst_3 : MulOneClass β
f : α →*o β
h : Monotone (OneHom.toFun (↑(↑f : α →* β) : OneHom α β))
a : α
⊢ Eq.{u_3 + 1} (α := β) (({ toMonoidHom := (↑f : α →* β), monotone' := h : α →*o β } : (a : α) → β) a : β)
    ((f : (a : α) → β) a : β)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulOneClass α
inst_3 : MulOneClass β
f : α →*o β
⊢ Eq (α := (a : α) → β) (⇑(↑f : α →* β) : (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 : MulOneClass α
inst_3 : MulOneClass β
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 : MulOneClass α
inst_3 : MulOneClass β
f g : α →*o β
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f.toMonoidHom : (a : α) → β) x : β) ((g.toMonoidHom : (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 : MulOneClass α
inst_3 : MulOneClass β
f g : α →*o β
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (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 : MulOneClass α
inst_3 : MulOneClass β
f g : α →*o β
h : f.toOrderHom = g.toOrderHom
⊢ ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f.toOrderHom : (a : α) → β) x : β) ((g.toOrderHom : (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 : MulOneClass α
inst_3 : MulOneClass β
f g : α →*o β
h : f.toOrderHom = g.toOrderHom
⊢ ∀ (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 : MulOneClass α
inst_3 : MulOneClass β
f : α →*o β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

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 : MulOneClass α
inst_3 : MulOneClass β
f : α →*o β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
inst : Preorder α
inst_1 : MulOneClass α
⊢ Eq (α := (a : α) → α) (⇑(OrderMonoidHom.id α) : (a : α) → α) id

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 : MulOneClass α
inst_4 : MulOneClass β
inst_5 : MulOneClass γ
f : β →*o γ
g : α →*o β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (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 : MulOneClass α
inst_4 : MulOneClass β
inst_5 : MulOneClass γ
f : β →*o γ
g : α →*o β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (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 : MulOneClass α
inst_4 : MulOneClass β
inst_5 : MulOneClass γ
f : β →*o γ
g : α →*o β
⊢ Eq (α := α →* γ) (↑(f.comp g) : α →* γ) (MonoidHom.comp (↑f : β →* γ) (↑g : α →* β))

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 : MulOneClass α
inst_4 : MulOneClass β
inst_5 : MulOneClass γ
f : β →*o γ
g : α →*o β
⊢ Eq (α := α →o γ) (↑(f.comp g) : α →o γ) (OrderHom.comp (↑f : β →o γ) (↑g : α →o β))

Tactic:
rfl

Premises used: OrderHom.comp, OrderHomClass.toOrderHom, rfl
-- 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 : MulOneClass α
inst_5 : MulOneClass β
inst_6 : MulOneClass γ
inst_7 : MulOneClass δ
f : γ →*o δ
g : β →*o γ
h : α →*o β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: OrderMonoidHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulOneClass α
inst_3 : MulOneClass β
f : α →*o β
⊢ f.comp (OrderMonoidHom.id α) = f

Tactic:
rfl

Premises used: OrderMonoidHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulOneClass α
inst_3 : MulOneClass β
f : α →*o β
⊢ comp (OrderMonoidHom.id β) f = f

Tactic:
rfl

Premises used: OrderMonoidHom.comp, 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 : MulOneClass α
inst_4 : MulOneClass β
inst_5 : MulOneClass γ
g₁ g₂ : β →*o γ
f : α →*o β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : g₁ = g₂
⊢ g₁.comp f = g₂.comp f

Tactic:
congr
-- 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 : MulOneClass α
inst_4 : MulOneClass β
inst_5 : MulOneClass γ
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: OrderMonoidHom.comp_apply
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulOneClass α
inst_3 : MulOneClass β
⊢ Eq (α := (a : α) → β) (⇑1 : (a : α) → β) 1

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 : MulOneClass α
inst_3 : MulOneClass β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((1 : (a : α) → β) a : β) (1 : β)

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 : MulOneClass α
inst_4 : MulOneClass β
inst_5 : MulOneClass γ
f : α →*o β
⊢ Eq (α := α →*o γ) (comp 1 f) 1

Tactic:
rfl

Premises used: OrderMonoidHom.comp, 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 : MulOneClass α
inst_4 : MulOneClass β
inst_5 : MulOneClass γ
f : β →*o γ
⊢ Eq (α := α →*o γ) (f.comp 1) 1

Tactic:
ext fun _ => map_one f

Premises used: map_one, OrderMonoidHom.ext
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : CommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedMonoid β
f g : α →*o β
⊢ (⇑(f * g) : (a : α) → β) = HMul.hMul (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : CommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedMonoid β
f g : α →*o β
a : α
⊢ (f * g : (a : α) → β) a = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : CommMonoid β
inst_3 : Preorder β
inst_4 : CommMonoid γ
inst_5 : Preorder γ
inst_6 : IsOrderedMonoid γ
g₁ g₂ : β →*o γ
f : α →*o β
⊢ (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

Tactic:
rfl

Premises used: OrderMonoidHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : CommMonoid β
inst_3 : Preorder β
inst_4 : CommMonoid γ
inst_5 : Preorder γ
inst_6 : IsOrderedMonoid β
inst_7 : IsOrderedMonoid γ
g : β →*o γ
f₁ f₂ : α →*o β
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext fun _ => map_mul g _ _

Premises used: MonoidHomClass.toMonoidHom, map_mul, DFunLike.coe, OrderMonoidHom.ext
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
x : Preorder α
x_1 : Preorder β
x_2 : MulOneClass α
x_3 : MulOneClass β
f : α →*o β
⊢ f.toMonoidHom = (↑f : α →* β)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Order.Hom.Monoid
Goal:
α : Type u_2
β : Type u_3
x : Preorder α
x_1 : Preorder β
x_2 : MulOneClass α
x_3 : MulOneClass β
f : α →*o β
⊢ f.toOrderHom = (↑f : α →o β)

Tactic:
rfl

Premises used: OrderHomClass.toOrderHom, 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 g : α ≃*o β
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
obtain :
  ∀ (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' : α ≃*o β }.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' : α ≃*o β }.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' : α ≃*o β } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
-- 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 β
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_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_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 :
              α ≃* β }.toFun
          a ≤
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1,
              map_mul' := map_mul'_1 : α ≃* β }.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' : α ≃*o β }.toFun =
    { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_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_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_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_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_le_map_iff' := @map_le_map_iff'_1 }

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 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.Monoid
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
⊢ f.toFun = (⇑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 : α ≃* β
h : ∀ {a b : α}, f.toFun a ≤ f.toFun b ↔ a ≤ b
⊢ Eq (α := (a : α) → β) (⇑{ toMulEquiv := f, map_le_map_iff' := @h : α ≃*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 : α ≃*o β
h : ∀ {a b : α}, (MulEquiv.toEquiv (↑f : α ≃* β)).toFun a ≤ (MulEquiv.toEquiv (↑f : α ≃* β)).toFun b ↔ a ≤ b
⊢ { toMulEquiv := (↑f : α ≃* β), map_le_map_iff' := @h : α ≃*o β } = 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 β
⊢ Eq (α := (a : α) → β) (⇑(↑f : α ≃* β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl