awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
y : WithBot α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ y → y ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = y
have coe : (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
y : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = ⊥
⊢ (↑a_1 : WithBot α) ≤ y → y ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = y
have coe₁ : ∀ (a : α),
  (↑a_1 : WithBot α) ≤ (↑a : WithBot α) → (↑a : WithBot α) ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = (↑a : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_2 : WithBot α) ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = (↑a_2 : WithBot α)
have coe : a_1 ≤ a_2 → a_2 ≤ a_1 → a_1 = a_2
Tactic: simp [le_def]
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : PartialOrder α
y : WithBot α
a b : α
hy : (↑b : WithBot α) ≤ y
⊢ b ≤ unbotD a y
have rwa : y ≠ ⊥
Tactic: rwa [le_unbotD_iff]
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Nonempty α
inst_2 : NoTopOrder α
x : WithBot (WithTop α)
⊢ x = ⊤ ↔ ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ x
have refine : ∀ (H : ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ x), x = ⊤
Tactic: refine ⟨by simp_all, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Nonempty α
inst_2 : NoTopOrder α
x : WithBot (WithTop α)
H : ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ x
⊢ x = ⊤
have bot : ∀ (H : ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ ⊥), Eq.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤
Tactic: induction x
Cleared hypotheses: x, H
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Nonempty α
inst_2 : NoTopOrder α
x : WithBot (WithTop α)
H : ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ x
bot : ∀ (H : ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ ⊥), Eq.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤
⊢ x = ⊤
have coe : ∀ (a : WithTop α) (H : ∀ (a_1 : α), (↑(↑a_1 : WithTop α) : WithBot (WithTop α)) ≤ (↑a : WithBot (WithTop α))),
  (↑a : WithBot (WithTop α)) = ⊤
Tactic: induction x
Cleared hypotheses: x, H
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y : WithBot α
⊢ x ≤
    match (motive := WithBot α → WithBot α → WithBot α) x, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have bot : LE.le (α := WithBot α) (⊥ : WithBot α)
  (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
    WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y : WithBot α
bot :
  LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
⊢ x ≤
    match (motive := WithBot α → WithBot α → WithBot α) x, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have coe : ∀ (a : α),
  (↑a : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a : WithBot α), y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
⊢ LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
have bot : LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α)
  (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
    WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
bot :
  LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
⊢ LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
have bot₁ : ∀ (a : α),
  LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a : WithBot α) with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have coe : (↑a_1 : WithBot α) ≤
  match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
  | none, none => ⊥
  | Option.some a, none => (↑a : WithBot α)
  | none, Option.some b => (↑b : WithBot α)
  | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
a_1 : α
coe :
  (↑a_1 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
⊢ (↑a_1 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have coe₁ : ∀ (a : α),
  (↑a_1 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a : WithBot α) with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y : WithBot α
⊢ y ≤
    match (motive := WithBot α → WithBot α → WithBot α) x, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have bot : y ≤
  match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
  | none, none => ⊥
  | Option.some a, none => (↑a : WithBot α)
  | none, Option.some b => (↑b : WithBot α)
  | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y : WithBot α
bot :
  y ≤
    match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
⊢ y ≤
    match (motive := WithBot α → WithBot α → WithBot α) x, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have coe : ∀ (a : α),
  y ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a : WithBot α), y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
⊢ y ≤
    match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have bot : LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α)
  (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
    WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
bot :
  LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
⊢ y ≤
    match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have bot₁ : ∀ (a : α),
  (↑a : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a : WithBot α) with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
a_1 : α
⊢ y ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have coe : LE.le (α := WithBot α) (⊥ : WithBot α)
  (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
    WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
a_1 : α
coe :
  LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
⊢ y ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
have coe₁ : ∀ (a : α),
  (↑a : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a : WithBot α) with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y z : WithBot α
⊢ x ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) x, y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have bot : ⊥ ≤ z →
  y ≤ z →
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
      z
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y z : WithBot α
bot :
  ⊥ ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
⊢ x ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) x, y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have coe : ∀ (a : α),
  (↑a : WithBot α) ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a : WithBot α), y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y z : WithBot α
⊢ ⊥ ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have bot : ⊥ ≤ z →
  ⊥ ≤ z →
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
      z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y z : WithBot α
bot :
  ⊥ ≤ z →
    ⊥ ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
⊢ ⊥ ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have bot₁ : ∀ (a : α),
  ⊥ ≤ z →
    (↑a : WithBot α) ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y z : WithBot α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have coe : (↑a_1 : WithBot α) ≤ z →
  ⊥ ≤ z →
    (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
      z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y z : WithBot α
a_1 : α
coe :
  (↑a_1 : WithBot α) ≤ z →
    ⊥ ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
⊢ (↑a_1 : WithBot α) ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have coe₁ : ∀ (a : α),
  (↑a_1 : WithBot α) ≤ z →
    (↑a : WithBot α) ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
⊢ ⊥ ≤ z →
    ⊥ ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    LE.le.{u_1} (α := WithBot α)
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
        WithBot α)
      (⊥ : WithBot α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
bot :
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
      LE.le.{u_1} (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)
⊢ ⊥ ≤ z →
    ⊥ ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have bot₁ : ∀ (a : α),
  ⊥ ≤ (↑a : WithBot α) →
    ⊥ ≤ (↑a : WithBot α) →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        (↑a : WithBot α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
a_1 : α
⊢ ⊥ ≤ z →
    (↑a_1 : WithBot α) ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
  (↑a_1 : WithBot α) ≤ ⊥ →
    LE.le (α := WithBot α)
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
        WithBot α)
      (⊥ : WithBot α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
a_1 : α
bot :
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    (↑a_1 : WithBot α) ≤ ⊥ →
      LE.le (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)
⊢ ⊥ ≤ z →
    (↑a_1 : WithBot α) ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
have bot₁ : ∀ (a : α),
  ⊥ ≤ (↑a : WithBot α) →
    (↑a_1 : WithBot α) ≤ (↑a : WithBot α) →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        (↑a : WithBot α)
Tactic: cases z
Cleared hypotheses: z