awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β
h : Monotone (ZeroHom.toFun (↑(↑f : α →*₀ β) : ZeroHom α β))
⊢ { toMonoidWithZeroHom := (↑f : α →*₀ β), monotone' := h : α →*₀o β } = f

Tactic:
rfl

Premises used: MonoidWithZeroHomClass.toMonoidWithZeroHom, 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 : α →*₀o β
⊢ Eq (α := (a : α) → β) (⇑(↑f : α →*₀ β) : (a : α) → β) (⇑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 : α →*₀o β
⊢ Eq (α := (a : α) → β) (⇑(↑f : α →*o β) : (a : α) → β) (⇑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 g : α →*₀o β
h : f.toOrderMonoidHom = g.toOrderMonoidHom
⊢ ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f.toOrderMonoidHom : (a : α) → β) x : β) ((g.toOrderMonoidHom : (a : α) → β) x : β)

Tactic:
DFunLike.ext_iff.1 h

Premises used: DFunLike.ext_iff, Iff.mp
-- 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 : f.toOrderMonoidHom = g.toOrderMonoidHom
⊢ ∀ (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.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulZeroOneClass α
inst_3 : MulZeroOneClass β
f g : α →*₀o β
h : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom
⊢ ∀ (x : α),
    Eq.{u_3 + 1} (α := β) ((f.toMonoidWithZeroHom : (a : α) → β) x : β) ((g.toMonoidWithZeroHom : (a : α) → β) x : β)

Tactic:
DFunLike.ext_iff.1 h

Premises used: DFunLike.ext_iff, Iff.mp
-- 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 : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom
⊢ ∀ (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.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulZeroOneClass α
inst_3 : MulZeroOneClass β
f : α →*₀o β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

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

Tactic:
DFunLike.ext' h

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : MulZeroOneClass α
inst_4 : MulZeroOneClass β
inst_5 : MulZeroOneClass γ
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.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : MulZeroOneClass α
inst_4 : MulZeroOneClass β
inst_5 : MulZeroOneClass γ
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.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : MulZeroOneClass α
inst_4 : MulZeroOneClass β
inst_5 : MulZeroOneClass γ
f : β →*₀o γ
g : α →*₀o β
⊢ Eq (α := α →*₀ γ) (↑(f.comp g) : α →*₀ γ) (MonoidWithZeroHom.comp (↑f : β →*₀ γ) (↑g : α →*₀ β))

Tactic:
rfl

Premises used: MonoidWithZeroHomClass.toMonoidWithZeroHom, MonoidWithZeroHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : MulZeroOneClass α
inst_4 : MulZeroOneClass β
inst_5 : MulZeroOneClass γ
f : β →*₀o γ
g : α →*₀o β
⊢ Eq (α := α →*o γ) (↑(f.comp g) : α →*o γ) (OrderMonoidHom.comp (↑f : β →*o γ) (↑g : α →*o β))

Tactic:
rfl

Premises used: OrderMonoidHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
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 : MulZeroOneClass α
inst_5 : MulZeroOneClass β
inst_6 : MulZeroOneClass γ
inst_7 : MulZeroOneClass δ
f : γ →*₀o δ
g : β →*₀o γ
h : α →*₀o β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: MonoidWithZeroHom.comp, OrderMonoidWithZeroHom.comp, 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 : α →*₀o β
⊢ f.comp (OrderMonoidWithZeroHom.id α) = f

Tactic:
rfl

Premises used: MonoidWithZeroHom.comp, OrderMonoidWithZeroHom.comp, 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 : α →*₀o β
⊢ comp (OrderMonoidWithZeroHom.id β) f = f

Tactic:
rfl

Premises used: MonoidWithZeroHom.comp, OrderMonoidWithZeroHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : MulZeroOneClass α
inst_4 : MulZeroOneClass β
inst_5 : MulZeroOneClass γ
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.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : MulZeroOneClass α
inst_4 : MulZeroOneClass β
inst_5 : MulZeroOneClass γ
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: OrderMonoidWithZeroHom.comp_apply
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrderedCommMonoidWithZero α
inst_1 : LinearOrderedCommMonoidWithZero β
f g : α →*₀o β
⊢ (⇑(f * g) : (a : α) → β) = HMul.hMul (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrderedCommMonoidWithZero α
inst_1 : LinearOrderedCommMonoidWithZero β
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.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : LinearOrderedCommMonoidWithZero α
inst_1 : LinearOrderedCommMonoidWithZero β
inst_2 : LinearOrderedCommMonoidWithZero γ
g₁ g₂ : β →*₀o γ
f : α →*₀o β
⊢ (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

Tactic:
rfl

Premises used: MonoidWithZeroHom.comp, OrderMonoidWithZeroHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : LinearOrderedCommMonoidWithZero α
inst_1 : LinearOrderedCommMonoidWithZero β
inst_2 : LinearOrderedCommMonoidWithZero γ
g : β →*₀o γ
f₁ f₂ : α →*₀o β
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext fun _ => map_mul g _ _

Premises used: MonoidWithZeroHomClass.toMonoidWithZeroHom, OrderMonoidWithZeroHom.ext, MonoidHomClass.toMonoidHom, map_mul, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀o β
⊢ f.toMonoidWithZeroHom = (↑f : α →*₀ β)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀ β
hf : Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ (↑{ toMonoidWithZeroHom := f, monotone' := hf : α →*₀o β } : α →*₀ β) = f

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
hγ : Preorder γ
hγ' : MulZeroOneClass γ
f : β →*₀o γ
g : α →*₀o β
⊢ Eq (α := α →*₀ γ) (↑(f.comp g) : α →*₀ γ) (MonoidWithZeroHom.comp (↑f : β →*₀ γ) (↑g : α →*₀ β))

Tactic:
rfl

Premises used: MonoidWithZeroHomClass.toMonoidWithZeroHom, MonoidWithZeroHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀o β
⊢ f.toOrderMonoidHom = (↑f : α →*o β)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, OrderMonoidHomClass.toOrderMonoidHom, OrderMonoidWithZeroHom.toOrderMonoidHom, rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
hγ : Preorder γ
hγ' : MulZeroOneClass γ
f : β →*₀o γ
g : α →*₀o β
⊢ Eq (α := α →*o γ) (↑(f.comp g) : α →*o γ) (OrderMonoidHom.comp (↑f : β →*o γ) (↑g : α →*o β))

Tactic:
rfl

Premises used: OrderMonoidHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst : Group α
inst_1 : Preorder α
a b : (WithZero α)ˣ
⊢ Equiv.toFun (MulEquiv.toEquiv WithZero.unitsWithZeroEquiv) a ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.unitsWithZeroEquiv) b ↔
    a ≤ b

Tactic:
simp [WithZero.unitsWithZeroEquiv]

Premises used: WithZero.unitsWithZeroEquiv
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
e : G ≃*o H
a b : WithZero G
zero :
  LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
        (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0)
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) b) ↔
    0 ≤ b
coe :
  ∀ (a : G),
    LE.le.{u_7} (α := WithZero H)
        (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
          (↑a : WithZero G))
        (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
          b) ↔
      (↑a : WithZero G) ≤ b
⊢ LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) a)
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) b) ↔
    a ≤ b

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
e : G ≃*o H
b : WithZero G
zero :
  LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
        (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0)
      (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
        (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0) ↔
    LE.le.{u_6} (α := WithZero G) 0 0
zero₁ :
  ∀ (a : G),
    LE.le.{u_7} (α := WithZero H)
        (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
          (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0)
        (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
          (↑a : WithZero G)) ↔
      0 ≤ (↑a : WithZero G)
⊢ LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
        (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0)
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) b) ↔
    0 ≤ b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
e : G ≃*o H
b : WithZero G
a : G
coe :
  LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
        (↑a : WithZero G))
      (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
        (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0) ↔
    (↑a : WithZero G) ≤ 0
coe₁ :
  ∀ (a_1 : G),
    LE.le.{u_7} (α := WithZero H)
        (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
          (↑a : WithZero G))
        (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
          (↑a_1 : WithZero G)) ↔
      (↑a : WithZero G) ≤ (↑a_1 : WithZero G)
⊢ LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
        (↑a : WithZero G))
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) b) ↔
    (↑a : WithZero G) ≤ b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
e : G ≃*o H
⊢ LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
        (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0)
      (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
        (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0) ↔
    LE.le.{u_6} (α := WithZero G) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
e : G ≃*o H
a : G
⊢ LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
        (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0)
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
        (↑a : WithZero G)) ↔
    0 ≤ (↑a : WithZero G)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
e : G ≃*o H
a : G
⊢ LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
        (↑a : WithZero G))
      (Equiv.toFun.{u_6 + 1, u_7 + 1} (α := WithZero G)
        (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv)) 0) ↔
    (↑a : WithZero G) ≤ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
e : G ≃*o H
a a_1 : G
⊢ LE.le.{u_7} (α := WithZero H)
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
        (↑a : WithZero G))
      (Equiv.toFun (MulEquiv.toEquiv ((MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv))
        (↑a_1 : WithZero G)) ↔
    (↑a : WithZero G) ≤ (↑a_1 : WithZero G)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)
a b : G
⊢ LE.le.{u_7} (α := H)
      (Equiv.toFun
        (MulEquiv.toEquiv
          ((Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H) (↑e : WithZero G ≃* WithZero H)))
        a)
      (Equiv.toFun
        (MulEquiv.toEquiv
          ((Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H) (↑e : WithZero G ≃* WithZero H)))
        b) ↔
    a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
x : G ≃*o H
h :
  ∀ (a : G),
    Eq.{u_7 + 1} (α := H)
      (((fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
                ({
                    toMulEquiv :=
                      (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H)
                        (↑e : WithZero G ≃* WithZero H),
                    map_le_map_iff' := ⋯ } :
                  G ≃*o H))
              ((fun (e : G ≃*o H) ↦
                  ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
                      map_le_map_iff' := ⋯ } :
                    OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
                x) :
            (a : G) → H)
          a :
        H)
      ((x : (a : G) → H) a : H)
⊢ (fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
        ({
            toMulEquiv :=
              (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H) (↑e : WithZero G ≃* WithZero H),
            map_le_map_iff' := ⋯ } :
          G ≃*o H))
      ((fun (e : G ≃*o H) ↦
          ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
              map_le_map_iff' := ⋯ } :
            OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
x : G ≃*o H
a : G
⊢ Eq.{u_7 + 1} (α := H)
    (((fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
              ({
                  toMulEquiv :=
                    (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H)
                      (↑e : WithZero G ≃* WithZero H),
                  map_le_map_iff' := ⋯ } :
                G ≃*o H))
            ((fun (e : G ≃*o H) ↦
                ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
                    map_le_map_iff' := ⋯ } :
                  OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
              x) :
          (a : G) → H)
        a :
      H)
    ((x : (a : G) → H) a : H)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
x : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)
h :
  ∀ (x_1 : WithZero G),
    Eq.{u_7 + 1} (α := WithZero H)
      ((((fun (e : G ≃*o H) ↦
                  ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
                      map_le_map_iff' := ⋯ } :
                    OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
                ((fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
                    ({
                        toMulEquiv :=
                          (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H)
                            (↑e : WithZero G ≃* WithZero H),
                        map_le_map_iff' := ⋯ } :
                      G ≃*o H))
                  x) :
              OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) :
            (a : WithZero G) → WithZero H)
          x_1 :
        WithZero H)
      ((x : (a : WithZero G) → WithZero H) x_1 : WithZero H)
⊢ (fun (e : G ≃*o H) ↦
        ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
            map_le_map_iff' := ⋯ } :
          OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
      ((fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
          ({
              toMulEquiv :=
                (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H)
                  (↑e : WithZero G ≃* WithZero H),
              map_le_map_iff' := ⋯ } :
            G ≃*o H))
        x) =
    x

Tactic:
ext x