awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
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 α)
⊢ 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₁ : ∀ (a : α),
  0 ≤ (↑a : WithZero α) →
    0 ≤ (↑a : 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 α)) ≤
        (↑a : WithZero α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
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
have zero : LE.le.{u_1} (α := WithZero α) 0 0 →
  (↑a : WithZero α) ≤ 0 →
    LE.le (α := 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 α)
      (0 : WithZero α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
a : α
zero :
  LE.le.{u_1} (α := WithZero α) 0 0 →
    (↑a : WithZero α) ≤ 0 →
      LE.le (α := 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 α)
        (0 : WithZero α)
⊢ 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
have zero₁ : ∀ (a_1 : α),
  0 ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ (↑a_1 : 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 α)) ≤
        (↑a_1 : WithZero α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
a : α
⊢ (↑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
have coe : (↑a : WithZero α) ≤ 0 →
  LE.le.{u_1} (α := WithZero α) 0 0 →
    LE.le (α := 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 α)
      (0 : WithZero α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
a : α
coe :
  (↑a : WithZero α) ≤ 0 →
    LE.le.{u_1} (α := WithZero α) 0 0 →
      LE.le (α := 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 α)
        (0 : WithZero α)
⊢ (↑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
have coe₁ : ∀ (a_1 : α),
  (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    0 ≤ (↑a_1 : 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_1 : WithZero α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
a 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
have coe : (↑a : WithZero α) ≤ 0 →
  (↑a_1 : WithZero α) ≤ 0 →
    LE.le (α := 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 α) :
        WithZero α)
      (0 : WithZero α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
a a_1 : α
coe :
  (↑a : WithZero α) ≤ 0 →
    (↑a_1 : WithZero α) ≤ 0 →
      LE.le (α := 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 α) :
          WithZero α)
        (0 : WithZero α)
⊢ (↑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
have coe₁ : ∀ (a_2 : α),
  (↑a : WithZero α) ≤ (↑a_2 : WithZero α) →
    (↑a_1 : WithZero α) ≤ (↑a_2 : 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 α)) ≤
        (↑a_2 : WithZero α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a a_1 a_2 : α
⊢ (↑a : WithZero α) ≤ (↑a_2 : WithZero α) →
    (↑a_1 : WithZero α) ≤ (↑a_2 : 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 α)) ≤
        (↑a_2 : WithZero α)
have coe : a ≤ a_2 → a_1 ≤ a_2 → a ≤ a_2 ∧ a_1 ≤ a_2
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ x
have zero : LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y) 0
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 : SemilatticeInf α
x y : WithZero α
zero : LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y) 0
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ x
have coe : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ (↑a : 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 : SemilatticeInf α
y : WithZero α
⊢ LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y) 0
have zero : LE.le.{u_1} (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0) 0
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 : SemilatticeInf α
y : WithZero α
zero : LE.le.{u_1} (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0) 0
⊢ LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y) 0
have zero₁ : ∀ (a : α), LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a : WithZero α)) 0
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 : SemilatticeInf α
y : WithZero α
a : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ (↑a : WithZero α)
have coe : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0 ≤ (↑a : 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 : SemilatticeInf α
y : WithZero α
a : α
coe : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0 ≤ (↑a : WithZero α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ (↑a : WithZero α)
have coe₁ : ∀ (a_1 : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) (↑a_1 : WithZero α) ≤ (↑a : 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 : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ y
have zero : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y ≤ y
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 : SemilatticeInf α
x y : WithZero α
zero : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y ≤ y
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ y
have coe : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ y
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 : SemilatticeInf α
y : WithZero α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y ≤ y
have zero : LE.le.{u_1} (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0) 0
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 : SemilatticeInf α
y : WithZero α
zero : LE.le.{u_1} (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0) 0
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y ≤ y
have zero₁ : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a : WithZero α) ≤ (↑a : 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 : SemilatticeInf α
y : WithZero α
a : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ y
have coe : LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0) 0
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 : SemilatticeInf α
y : WithZero α
a : α
coe : LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0) 0
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ y
have coe₁ : ∀ (a_1 : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) (↑a_1 : WithZero α) ≤ (↑a_1 : 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 : SemilatticeInf α
x y z : WithZero α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z
have zero : 0 ≤ y → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y 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 : SemilatticeInf α
x y z : WithZero α
zero : 0 ≤ y → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z
have coe : ∀ (a : α), (↑a : WithZero α) ≤ y → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y 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 : SemilatticeInf α
y z : WithZero α
⊢ 0 ≤ y → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)
have zero : LE.le.{u_1} (α := WithZero α) 0 0 → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 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 : SemilatticeInf α
y z : WithZero α
zero : LE.le.{u_1} (α := WithZero α) 0 0 → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z)
⊢ 0 ≤ y → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)
have zero₁ : ∀ (a : α),
  0 ≤ (↑a : WithZero α) → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : 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 : SemilatticeInf α
y z : WithZero α
a : α
⊢ (↑a : WithZero α) ≤ y → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z
have coe : (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 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 : SemilatticeInf α
y z : WithZero α
a : α
coe : (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z
⊢ (↑a : WithZero α) ≤ y → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z
have coe₁ : ∀ (a_1 : α),
  (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : 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 : SemilatticeInf α
z : WithZero α
⊢ LE.le.{u_1} (α := WithZero α) 0 0 → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z)
have zero : LE.le.{u_1} (α := WithZero α) 0 0 →
  LE.le.{u_1} (α := WithZero α) 0 0 → LE.le.{u_1} (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
zero :
  LE.le.{u_1} (α := WithZero α) 0 0 →
    LE.le.{u_1} (α := WithZero α) 0 0 → LE.le.{u_1} (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0)
⊢ LE.le.{u_1} (α := WithZero α) 0 0 → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z)
have zero₁ : ∀ (a : α),
  LE.le.{u_1} (α := WithZero α) 0 0 →
    0 ≤ (↑a : WithZero α) → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a : WithZero α))
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
a : α
⊢ 0 ≤ (↑a : WithZero α) → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) z)
have zero : 0 ≤ (↑a : WithZero α) →
  LE.le.{u_1} (α := WithZero α) 0 0 → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
a : α
zero :
  0 ≤ (↑a : WithZero α) →
    LE.le.{u_1} (α := WithZero α) 0 0 → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0)
⊢ 0 ≤ (↑a : WithZero α) → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) z)
have zero₁ : ∀ (a_1 : α),
  0 ≤ (↑a : WithZero α) →
    0 ≤ (↑a_1 : WithZero α) →
      LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) (↑a_1 : WithZero α))
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
a : α
⊢ (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z
have coe : (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
a : α
coe : (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0
⊢ (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z
have coe₁ : ∀ (a_1 : α),
  (↑a : WithZero α) ≤ 0 →
    (↑a : WithZero α) ≤ (↑a_1 : WithZero α) → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a_1 : WithZero α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
a a_1 : α
⊢ (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) z
have coe : (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
  (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) 0
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
a a_1 : α
coe :
  (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) 0
⊢ (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) z
have coe₁ : ∀ (a_2 : α),
  (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ (↑a_2 : WithZero α) →
      (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) (↑a_2 : WithZero α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a a_1 a_2 : α
⊢ (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ (↑a_2 : WithZero α) →
      (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) (↑a_2 : WithZero α)
have coe : a ≤ a_1 → a ≤ a_2 → a ≤ a_1 ∧ a ≤ a_2
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : WithZero α
⊢ x ≤ y ∨ y ≤ x
have zero : 0 ≤ y ∨ y ≤ 0
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 : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : WithZero α
zero : 0 ≤ y ∨ y ≤ 0
⊢ x ≤ y ∨ y ≤ x
have coe : ∀ (a : α), (↑a : WithZero α) ≤ y ∨ y ≤ (↑a : 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 : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithZero α
⊢ 0 ≤ y ∨ y ≤ 0
have zero : LE.le.{u_1} (α := WithZero α) 0 0 ∨ LE.le.{u_1} (α := WithZero α) 0 0
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 : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithZero α
zero : LE.le.{u_1} (α := WithZero α) 0 0 ∨ LE.le.{u_1} (α := WithZero α) 0 0
⊢ 0 ≤ y ∨ y ≤ 0
have zero₁ : ∀ (a : α), 0 ≤ (↑a : WithZero α) ∨ (↑a : WithZero α) ≤ 0
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 : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithZero α
a : α
⊢ (↑a : WithZero α) ≤ y ∨ y ≤ (↑a : WithZero α)
have coe : (↑a : WithZero α) ≤ 0 ∨ 0 ≤ (↑a : 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 : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithZero α
a : α
coe : (↑a : WithZero α) ≤ 0 ∨ 0 ≤ (↑a : WithZero α)
⊢ (↑a : WithZero α) ≤ y ∨ y ≤ (↑a : WithZero α)
have coe₁ : ∀ (a_1 : α), (↑a : WithZero α) ≤ (↑a_1 : WithZero α) ∨ (↑a_1 : WithZero α) ≤ (↑a : 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 : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a a_1 : α
⊢ (↑a : WithZero α) ≤ (↑a_1 : WithZero α) ∨ (↑a_1 : WithZero α) ≤ (↑a : WithZero α)
have coe : a ≤ a_1 ∨ a_1 ≤ a
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y
have obtain : ∀ (z' : WithZero α) (hnz' : z' ≠ 0) (hzx : z' ≤ x) (hzy : z' ≤ y), ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y
Tactic: obtain ⟨z', hnz', hzx, hzy⟩ := exists_ne_zero_and_le_and_le hx hy
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
⊢ ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y
have obtain : ∀ (z : WithZero α) (hnz : z ≠ 0) (hlt : z < z'), ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y
Tactic: obtain ⟨z, hnz, hlt⟩ := exists_ne_zero_and_lt hnz'
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y
have right : z < x ∧ z < y
Tactic: use z, hnz