awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
rwa :
  ∀
    (h :
      (↑(unzero ha) : WithZero (Multiplicative α)) ≤
        (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))),
    (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
rwa₁ : ∀ (h : unzero ha ≤ (ofAdd : (a : α) → Multiplicative α) b), (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
rwa₂ :
  ∀
    (h :
      LE.le (α := α) ((toAdd : (a : Multiplicative α) → α) (unzero ha) : α)
        ((toAdd : (a : Multiplicative α) → α) ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α) : α)),
    (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
⊢ (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
have rwa₃ : ∀ (h : (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b), (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
Tactic: rwa [← coe_unzero ha, coe_le_coe, ← toAdd_le, toAdd_ofAdd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
⊢ a ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
have rwa : (↑(unzero ha) : WithZero (Multiplicative α)) ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
Tactic: rwa [← coe_unzero ha, coe_le_coe, ← ofAdd_toAdd (unzero ha), ofAdd_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
rwa :
  (↑(unzero ha) : WithZero (Multiplicative α)) ≤
    (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
⊢ a ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
have rwa₁ : unzero ha ≤ (ofAdd : (a : α) → Multiplicative α) b
Tactic: rwa [← coe_unzero ha, coe_le_coe, ← ofAdd_toAdd (unzero ha), ofAdd_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
rwa :
  (↑(unzero ha) : WithZero (Multiplicative α)) ≤
    (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
rwa₁ : unzero ha ≤ (ofAdd : (a : α) → Multiplicative α) b
⊢ a ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
have rwa₂ : LE.le (α := Multiplicative α)
  ((ofAdd : (a : α) → Multiplicative α) ((toAdd : (a : Multiplicative α) → α) (unzero ha) : α) : Multiplicative α)
  ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α)
Tactic: rwa [← coe_unzero ha, coe_le_coe, ← ofAdd_toAdd (unzero ha), ofAdd_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
⊢ MulLeftReflectLT.{u_1} (WithZero α)
have refine : ∀ (a b c : WithZero α) (h : a * b < a * c), b < c
Tactic: refine ⟨fun a b c h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
a b c : WithZero α
h : a * b < a * c
⊢ b < c
have this : a * c ≠ 0
Tactic: have := h.ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
a b c : WithZero α
h : a * b < a * c
this : a * c ≠ 0
⊢ b < c
have zero : ∀ (h : 0 * b < 0 * c) (this : 0 * c ≠ 0), b < c
Tactic: induction a
Cleared hypotheses: a, h, this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
a b c : WithZero α
h : a * b < a * c
this : a * c ≠ 0
zero : ∀ (h : 0 * b < 0 * c) (this : 0 * c ≠ 0), b < c
⊢ b < c
have coe : ∀ (a : α) (h : (↑a : WithZero α) * b < (↑a : WithZero α) * c) (this : (↑a : WithZero α) * c ≠ 0), b < c
Tactic: induction a
Cleared hypotheses: a, h, this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
b c : WithZero α
a : α
h : (↑a : WithZero α) * b < (↑a : WithZero α) * c
this : (↑a : WithZero α) * c ≠ 0
⊢ b < c
have coe : ∀ (h : (↑a : WithZero α) * b < (↑a : WithZero α) * 0) (this : (↑a : WithZero α) * 0 ≠ 0), b < 0
Tactic: induction c
Cleared hypotheses: c, h, this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
b c : WithZero α
a : α
h : (↑a : WithZero α) * b < (↑a : WithZero α) * c
this : (↑a : WithZero α) * c ≠ 0
coe : ∀ (h : (↑a : WithZero α) * b < (↑a : WithZero α) * 0) (this : (↑a : WithZero α) * 0 ≠ 0), b < 0
⊢ b < c
have coe₁ : ∀ (a_1 : α) (h : (↑a : WithZero α) * b < (↑a : WithZero α) * (↑a_1 : WithZero α))
  (this : (↑a : WithZero α) * (↑a_1 : WithZero α) ≠ 0), b < (↑a_1 : WithZero α)
Tactic: induction c
Cleared hypotheses: c, h, this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
b : WithZero α
a a_1 : α
h : (↑a : WithZero α) * b < (↑a : WithZero α) * (↑a_1 : WithZero α)
this : (↑a : WithZero α) * (↑a_1 : WithZero α) ≠ 0
⊢ b < (↑a_1 : WithZero α)
have coe : ∀ (h : (↑a : WithZero α) * 0 < (↑a : WithZero α) * (↑a_1 : WithZero α)), 0 < (↑a_1 : WithZero α)
Tactic: induction b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
b : WithZero α
a a_1 : α
h : (↑a : WithZero α) * b < (↑a : WithZero α) * (↑a_1 : WithZero α)
this : (↑a : WithZero α) * (↑a_1 : WithZero α) ≠ 0
coe : ∀ (h : (↑a : WithZero α) * 0 < (↑a : WithZero α) * (↑a_1 : WithZero α)), 0 < (↑a_1 : WithZero α)
⊢ b < (↑a_1 : WithZero α)
have coe₁ : ∀ (a_2 : α) (h : (↑a : WithZero α) * (↑a_2 : WithZero α) < (↑a : WithZero α) * (↑a_1 : WithZero α)),
  (↑a_2 : WithZero α) < (↑a_1 : WithZero α)
Tactic: induction b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
x y : WithZero α
⊢ x ≤
    match (motive := WithZero α → WithZero α → WithZero α) x, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have zero : LE.le (α := WithZero α) (0 : WithZero α)
  (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α) :
    WithZero α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
x y : WithZero α
zero :
  LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
⊢ x ≤
    match (motive := WithZero α → WithZero α → WithZero α) x, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have coe : ∀ (a : α),
  (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
⊢ LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
have zero : LE.le.{u_1} (α := WithZero α) (0 : WithZero α)
  (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α) :
    WithZero α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
zero :
  LE.le.{u_1} (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
⊢ LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
have zero₁ : ∀ (a : α),
  LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
a : α
⊢ (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have coe : (↑a : WithZero α) ≤
  match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
  | none, none => 0
  | some a, none => (↑a : WithZero α)
  | none, some b => (↑b : WithZero α)
  | some a, some b => (↑(a ⊔ b) : WithZero α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
a : α
coe :
  (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
⊢ (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have coe₁ : ∀ (a_1 : α),
  (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
x y : WithZero α
⊢ y ≤
    match (motive := WithZero α → WithZero α → WithZero α) x, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have zero : y ≤
  match (motive := WithZero α → WithZero α → WithZero α) 0, y with
  | none, none => 0
  | some a, none => (↑a : WithZero α)
  | none, some b => (↑b : WithZero α)
  | some a, some b => (↑(a ⊔ b) : WithZero α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
x y : WithZero α
zero :
  y ≤
    match (motive := WithZero α → WithZero α → WithZero α) 0, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
⊢ y ≤
    match (motive := WithZero α → WithZero α → WithZero α) x, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have coe : ∀ (a : α),
  y ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
⊢ y ≤
    match (motive := WithZero α → WithZero α → WithZero α) 0, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have zero : LE.le.{u_1} (α := WithZero α) (0 : WithZero α)
  (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α) :
    WithZero α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
zero :
  LE.le.{u_1} (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
⊢ y ≤
    match (motive := WithZero α → WithZero α → WithZero α) 0, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have zero₁ : ∀ (a : α),
  (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
a : α
⊢ y ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have coe : LE.le (α := WithZero α) (0 : WithZero α)
  (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α) :
    WithZero α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
a : α
coe :
  LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
⊢ y ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
have coe₁ : ∀ (a_1 : α),
  (↑a_1 : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
x y z : WithZero α
⊢ x ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) x, y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
have zero : 0 ≤ z →
  y ≤ z →
    (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
      z
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
x y z : WithZero α
zero :
  0 ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
⊢ x ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) x, y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
have coe : ∀ (a : α),
  (↑a : WithZero α) ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y z : WithZero α
⊢ 0 ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
have zero : 0 ≤ z →
  0 ≤ z →
    (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
      z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y z : WithZero α
zero :
  0 ≤ z →
    0 ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
⊢ 0 ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
have zero₁ : ∀ (a : α),
  0 ≤ z →
    (↑a : WithZero α) ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y z : WithZero α
a : α
⊢ (↑a : WithZero α) ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
have coe : (↑a : WithZero α) ≤ z →
  0 ≤ z →
    (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
      z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y z : WithZero α
a : α
coe :
  (↑a : WithZero α) ≤ z →
    0 ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
⊢ (↑a : WithZero α) ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
have coe₁ : ∀ (a_1 : α),
  (↑a : WithZero α) ≤ z →
    (↑a_1 : WithZero α) ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
⊢ 0 ≤ z →
    0 ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
have zero : LE.le.{u_1} (α := WithZero α) 0 0 →
  LE.le.{u_1} (α := WithZero α) 0 0 →
    LE.le.{u_1} (α := WithZero α)
      (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α) :
        WithZero α)
      (0 : WithZero α)
Tactic: cases z
Cleared hypotheses: z