awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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)
⊢ { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' : α →*o β } = g
have 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 }
Tactic: obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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 α β))
⊢ { toMonoidHom := (↑f : α →* β), monotone' := h : α →*o β } = f
have h₁ : ∀ (a : α),
  Eq.{u_3 + 1} (α := β) (({ toMonoidHom := (↑f : α →* β), monotone' := h : α →*o β } : (a : α) → β) a : β)
    ((f : (a : α) → β) a : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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
⊢ f = g
have 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
Tactic: obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g₁.trans f : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← trans_apply, h, trans_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g₂.trans f : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← trans_apply, h, trans_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
  ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← trans_apply, h, trans_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ LE.le.{u_2} (α := α) ((f.symm : (a : β) → α) a : α) ((f.symm : (a : β) → α) b : α)
have rw : a ≤ b ↔
  LE.le.{u_3} (α := β) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β)
    ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β)
Tactic: rw [← map_le_map_iff f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Mul α
inst_3 : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔
    LE.le.{u_3} (α := β) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β)
      ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β)
have h : (f : (a : α) → β) ((f.symm : (a : β) → α) a : α) = a
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
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
⊢ a ≤ b ↔
    LE.le.{u_3} (α := β) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β)
      ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β)
have h₁ : (f : (a : α) → β) ((f.symm : (a : β) → α) b : α) = b
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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)
⊢ f = g
have 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
Tactic: obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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)
⊢ { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul', monotone' := monotone' :
      α →*₀o β } =
    g
have 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 }
Tactic: obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ 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
have 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
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ 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
have 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
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ 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
have 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
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ 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
have 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)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ 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
have 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
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ 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
have 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)
Tactic: cases b
Cleared hypotheses: b