awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ x.unbot hx ≤ a ↔ x ≤ (↑a : WithBot α)
have lift : ∀ (x : α) (hx : (↑x : WithBot α) ≠ ⊥), (↑x : WithBot α).unbot hx ≤ a ↔ (↑x : WithBot α) ≤ (↑a : WithBot α)
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a b : α
inst : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ b ≤ unbotD a x ↔ (↑b : WithBot α) ≤ x
have lift : ∀ (x : α), b ≤ unbotD a (↑x : WithBot α) ↔ (↑b : WithBot α) ≤ (↑x : WithBot α)
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a b : α
inst : LE α
x : WithBot α
hx : x = ⊥ → a ≤ b
⊢ unbotD a x ≤ b ↔ x ≤ (↑b : WithBot α)
have bot : ∀ (hx : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ → a ≤ b), unbotD a ⊥ ≤ b ↔ ⊥ ≤ (↑b : WithBot α)
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a b : α
inst : LE α
x : WithBot α
hx : x = ⊥ → a ≤ b
bot : ∀ (hx : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ → a ≤ b), unbotD a ⊥ ≤ b ↔ ⊥ ≤ (↑b : WithBot α)
⊢ unbotD a x ≤ b ↔ x ≤ (↑b : WithBot α)
have coe : ∀ (a_1 : α) (hx : (↑a_1 : WithBot α) = ⊥ → a ≤ b),
  unbotD a (↑a_1 : WithBot α) ≤ b ↔ (↑a_1 : WithBot α) ≤ (↑b : WithBot α)
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LE α
x y : WithBot α
hx : x ≠ ⊥
h : x ≤ y
⊢ unbotD a x ≤ unbotD a y
have lift : ∀ (x : α) (h : (↑x : WithBot α) ≤ y), unbotD a (↑x : WithBot α) ≤ unbotD a y
Tactic: lift x to α using hx
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LE α
y : WithBot α
x : α
h : (↑x : WithBot α) ≤ y
⊢ unbotD a (↑x : WithBot α) ≤ unbotD a y
have bot : ∀ (h : (↑x : WithBot α) ≤ ⊥), unbotD a (↑x : WithBot α) ≤ unbotD a ⊥
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LE α
y : WithBot α
x : α
h : (↑x : WithBot α) ≤ y
bot : ∀ (h : (↑x : WithBot α) ≤ ⊥), unbotD a (↑x : WithBot α) ≤ unbotD a ⊥
⊢ unbotD a (↑x : WithBot α) ≤ unbotD a y
have coe : ∀ (a_1 : α) (h : (↑x : WithBot α) ≤ (↑a_1 : WithBot α)), unbotD a (↑x : WithBot α) ≤ unbotD a (↑a_1 : WithBot α)
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
inst_1 : Nonempty α
hx : x ≠ ⊥
⊢ x.unbotA ≤ a ↔ x ≤ (↑a : WithBot α)
have lift : ∀ (x : α), (↑x : WithBot α).unbotA ≤ a ↔ (↑x : WithBot α) ≤ (↑a : WithBot α)
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
⊢ x < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a : α), x = (↑a : WithBot α) → a < b
have bot : ⊥ < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
bot : ⊥ < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
⊢ x < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a : α), x = (↑a : WithBot α) → a < b
have coe : ∀ (a : α),
  (↑a : WithBot α) < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → a_1 < b
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
y : WithBot α
⊢ ⊥ < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
have bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
y : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
⊢ ⊥ < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
have bot₁ : ∀ (a : α),
  ⊥ < (↑a : WithBot α) ↔ ∃ (b : α), (↑a : WithBot α) = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
y : WithBot α
a : α
⊢ (↑a : WithBot α) < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → a_1 < b
have coe : (↑a : WithBot α) < ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → a_1 < b
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
y : WithBot α
a : α
coe :
  (↑a : WithBot α) < ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → a_1 < b
⊢ (↑a : WithBot α) < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → a_1 < b
have coe₁ : ∀ (a_1 : α),
  (↑a : WithBot α) < (↑a_1 : WithBot α) ↔
    ∃ (b : α), (↑a_1 : WithBot α) = (↑b : WithBot α) ∧ ∀ (a_2 : α), (↑a : WithBot α) = (↑a_2 : WithBot α) → a_2 < b
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
⊢ x < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ x < (↑b : WithBot α)
have bot : x < ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ x < (↑b : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
bot : x < ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ x < (↑b : WithBot α)
⊢ x < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ x < (↑b : WithBot α)
have coe : ∀ (a : α), x < (↑a : WithBot α) ↔ ∃ (b : α), (↑a : WithBot α) = (↑b : WithBot α) ∧ x < (↑b : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
x : WithBot α
⊢ ⊥ < x ↔ x ≠ ⊥
have bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
x : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ ⊥ < x ↔ x ≠ ⊥
have coe : ∀ (a : α), ⊥ < (↑a : WithBot α) ↔ (↑a : WithBot α) ≠ ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ a < x.unbot hx ↔ (↑a : WithBot α) < x
have lift : ∀ (x : α) (hx : (↑x : WithBot α) ≠ ⊥), a < (↑x : WithBot α).unbot hx ↔ (↑a : WithBot α) < (↑x : WithBot α)
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
b : α
inst : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ x.unbot hx < b ↔ x < (↑b : WithBot α)
have lift : ∀ (x : α) (hx : (↑x : WithBot α) ≠ ⊥), (↑x : WithBot α).unbot hx < b ↔ (↑x : WithBot α) < (↑b : WithBot α)
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a b : α
inst : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ b < unbotD a x ↔ (↑b : WithBot α) < x
have lift : ∀ (x : α), b < unbotD a (↑x : WithBot α) ↔ (↑b : WithBot α) < (↑x : WithBot α)
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a b : α
inst : LT α
x : WithBot α
hx : x = ⊥ → a < b
⊢ unbotD a x < b ↔ x < (↑b : WithBot α)
have bot : ∀ (hx : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ → a < b), unbotD a ⊥ < b ↔ ⊥ < (↑b : WithBot α)
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a b : α
inst : LT α
x : WithBot α
hx : x = ⊥ → a < b
bot : ∀ (hx : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ → a < b), unbotD a ⊥ < b ↔ ⊥ < (↑b : WithBot α)
⊢ unbotD a x < b ↔ x < (↑b : WithBot α)
have coe : ∀ (a_1 : α) (hx : (↑a_1 : WithBot α) = ⊥ → a < b),
  unbotD a (↑a_1 : WithBot α) < b ↔ (↑a_1 : WithBot α) < (↑b : WithBot α)
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LT α
x : WithBot α
inst_1 : Nonempty α
hx : x ≠ ⊥
⊢ x.unbotA < a ↔ x < (↑a : WithBot α)
have lift : ∀ (x : α), (↑x : WithBot α).unbotA < a ↔ (↑x : WithBot α) < (↑a : WithBot α)
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- 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 : Preorder α
x : WithBot α
⊢ x ≤ x
have bot : LE.le.{u_1} (α := 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 : Preorder α
x : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ x ≤ x
have coe : ∀ (a : α), (↑a : WithBot α) ≤ (↑a : 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 : Preorder α
x y z : WithBot α
⊢ x ≤ y → y ≤ z → x ≤ z
have bot : ⊥ ≤ y → y ≤ z → ⊥ ≤ 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 : Preorder α
x y z : WithBot α
bot : ⊥ ≤ y → y ≤ z → ⊥ ≤ z
⊢ x ≤ y → y ≤ z → x ≤ z
have coe : ∀ (a : α), (↑a : WithBot α) ≤ y → y ≤ z → (↑a : 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 : Preorder α
y z : WithBot α
⊢ ⊥ ≤ y → y ≤ z → ⊥ ≤ z
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → ⊥ ≤ 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 : Preorder α
y z : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → ⊥ ≤ z
⊢ ⊥ ≤ y → y ≤ z → ⊥ ≤ z
have bot₁ : ∀ (a : α), ⊥ ≤ (↑a : WithBot α) → (↑a : WithBot α) ≤ z → ⊥ ≤ 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 : Preorder α
y z : WithBot α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ y → y ≤ z → (↑a_1 : WithBot α) ≤ z
have coe : (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ z → (↑a_1 : 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 : Preorder α
y z : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ z → (↑a_1 : WithBot α) ≤ z
⊢ (↑a_1 : WithBot α) ≤ y → y ≤ z → (↑a_1 : WithBot α) ≤ z
have coe₁ : ∀ (a : α), (↑a_1 : WithBot α) ≤ (↑a : WithBot α) → (↑a : WithBot α) ≤ z → (↑a_1 : 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 : Preorder α
z : WithBot α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → ⊥ ≤ z
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := 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 : Preorder α
z : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → ⊥ ≤ z
have bot₁ : ∀ (a : α), LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ (↑a : 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 : Preorder α
z : WithBot α
a_1 : α
⊢ ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ z → ⊥ ≤ z
have bot : ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ ⊥ → LE.le.{u_1} (α := 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 : Preorder α
z : WithBot α
a_1 : α
bot : ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ z → ⊥ ≤ z
have bot₁ : ∀ (a : α), ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a : 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 : Preorder α
z : WithBot α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ z → (↑a_1 : WithBot α) ≤ z
have coe : (↑a_1 : WithBot α) ≤ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → (↑a_1 : 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 : Preorder α
z : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → (↑a_1 : WithBot α) ≤ ⊥
⊢ (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ z → (↑a_1 : WithBot α) ≤ z
have coe₁ : ∀ (a : α), (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a : WithBot α) → (↑a_1 : 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 : Preorder α
z : WithBot α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) → (↑a_2 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ z
have coe : (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) → (↑a_2 : WithBot α) ≤ ⊥ → (↑a_1 : 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 : Preorder α
z : WithBot α
a_1 a_2 : α
coe : (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) → (↑a_2 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ ⊥
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) → (↑a_2 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ z
have coe₁ : ∀ (a : α),
  (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_2 : WithBot α) ≤ (↑a : WithBot α) → (↑a_1 : 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 : Preorder α
a_1 a_2 a_3 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_2 : WithBot α) ≤ (↑a_3 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a_3 : WithBot α)
have coe : a_1 ≤ a_2 → a_2 ≤ a_3 → a_1 ≤ a_3
Tactic: simp [le_def]
-- 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 : Preorder α
x y : WithBot α
⊢ x < y ↔ x ≤ y ∧ ¬y ≤ x
have bot : ⊥ < y ↔ ⊥ ≤ y ∧ ¬y ≤ ⊥
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 : Preorder α
x y : WithBot α
bot : ⊥ < y ↔ ⊥ ≤ y ∧ ¬y ≤ ⊥
⊢ x < y ↔ x ≤ y ∧ ¬y ≤ x
have coe : ∀ (a : α), (↑a : WithBot α) < y ↔ (↑a : WithBot α) ≤ y ∧ ¬y ≤ (↑a : 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 : Preorder α
y : WithBot α
⊢ ⊥ < y ↔ ⊥ ≤ y ∧ ¬y ≤ ⊥
have bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ∧ ¬LE.le.{u_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 : Preorder α
y : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ∧ ¬LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ ⊥ < y ↔ ⊥ ≤ y ∧ ¬y ≤ ⊥
have bot₁ : ∀ (a : α), ⊥ < (↑a : WithBot α) ↔ ⊥ ≤ (↑a : 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 : Preorder α
y : WithBot α
a_1 : α
⊢ (↑a_1 : WithBot α) < y ↔ (↑a_1 : WithBot α) ≤ y ∧ ¬y ≤ (↑a_1 : WithBot α)
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 : Preorder α
y : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) < ⊥ ↔ (↑a_1 : WithBot α) ≤ ⊥ ∧ ¬⊥ ≤ (↑a_1 : WithBot α)
⊢ (↑a_1 : WithBot α) < y ↔ (↑a_1 : WithBot α) ≤ y ∧ ¬y ≤ (↑a_1 : WithBot α)
have coe₁ : ∀ (a : α),
  (↑a_1 : WithBot α) < (↑a : WithBot α) ↔ (↑a_1 : WithBot α) ≤ (↑a : WithBot α) ∧ ¬(↑a : 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
inst : Preorder α
inst_1 : Preorder β
x y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f x ≤ map f y ↔ x ≤ y
have bot : map f ⊥ ≤ map f y ↔ ⊥ ≤ y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
bot : map f ⊥ ≤ map f y ↔ ⊥ ≤ y
⊢ map f x ≤ map f y ↔ x ≤ y
have coe : ∀ (a : α), map f (↑a : WithBot α) ≤ map f y ↔ (↑a : WithBot α) ≤ y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f ⊥ ≤ map f y ↔ ⊥ ≤ y
have bot : map f ⊥ ≤ map f ⊥ ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
bot : map f ⊥ ≤ map f ⊥ ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ map f ⊥ ≤ map f y ↔ ⊥ ≤ y
have bot₁ : ∀ (a : α), map f ⊥ ≤ map f (↑a : 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
inst : Preorder α
inst_1 : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a : α
⊢ map f (↑a : WithBot α) ≤ map f y ↔ (↑a : WithBot α) ≤ y
have coe : map f (↑a : WithBot α) ≤ map f ⊥ ↔ (↑a : WithBot α) ≤ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a : α
coe : map f (↑a : WithBot α) ≤ map f ⊥ ↔ (↑a : WithBot α) ≤ ⊥
⊢ map f (↑a : WithBot α) ≤ map f y ↔ (↑a : WithBot α) ≤ y
have coe₁ : ∀ (a_1 : α), map f (↑a : WithBot α) ≤ map f (↑a_1 : WithBot α) ↔ (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
b : α
⊢ x ≤ (↑(unbotD b x) : WithBot α)
have bot : ⊥ ≤ (↑(unbotD b ⊥) : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
b : α
bot : ⊥ ≤ (↑(unbotD b ⊥) : WithBot α)
⊢ x ≤ (↑(unbotD b x) : WithBot α)
have coe : ∀ (a : α), (↑a : WithBot α) ≤ (↑(unbotD b (↑a : WithBot α)) : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
inst_1 : OrderBot α
⊢ x < (↑⊥ : WithBot α) ↔ x = ⊥
have bot : LT.lt.{u_1} (α := WithBot α) ⊥ (↑⊥ : WithBot α) ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
inst_1 : OrderBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ (↑⊥ : WithBot α) ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ x < (↑⊥ : WithBot α) ↔ x = ⊥
have coe : ∀ (a : α), (↑a : WithBot α) < (↑⊥ : WithBot α) ↔ (↑a : WithBot α) = ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
⊢ x = ⊥ ↔ ∀ (b : α), x < (↑b : WithBot α)
have bot : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ↔ ∀ (b : α), ⊥ < (↑b : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
bot : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ↔ ∀ (b : α), ⊥ < (↑b : WithBot α)
⊢ x = ⊥ ↔ ∀ (b : α), x < (↑b : WithBot α)
have coe : ∀ (a : α), (↑a : WithBot α) = ⊥ ↔ ∀ (b : α), (↑a : WithBot α) < (↑b : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑a : WithBot α) = ⊥ ↔ ∀ (b : α), (↑a : WithBot α) < (↑b : WithBot α)
have coe : ∃ (x : α), ¬a < x
Tactic: simp
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
inst_1 : NoBotOrder α
⊢ x = ⊥ ↔ ∀ (b : α), x ≤ (↑b : WithBot α)
have refine : ∀ (h : ∀ (b : α), x ≤ (↑b : WithBot α)) (y : α), (↑y : WithBot α) ≠ x
Tactic: refine ⟨by simp +contextual, fun h ↦ (x.eq_bot_iff_forall_ne).2 fun y => ?_⟩
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x y : WithBot α
inst_1 : NoBotOrder α
⊢ (∀ (a : α), (↑a : WithBot α) ≤ x → (↑a : WithBot α) ≤ y) ↔ x ≤ y
have none : (∀ (a : α), (↑a : WithBot α) ≤ none → (↑a : WithBot α) ≤ y) ↔ none ≤ y
Tactic: obtain _ | a := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x y : WithBot α
inst_1 : NoBotOrder α
none : (∀ (a : α), (↑a : WithBot α) ≤ Option.none → (↑a : WithBot α) ≤ y) ↔ Option.none ≤ y
⊢ (∀ (a : α), (↑a : WithBot α) ≤ x → (↑a : WithBot α) ≤ y) ↔ x ≤ y
have some : ∀ (a : α), (∀ (a_1 : α), (↑a_1 : WithBot α) ≤ Option.some a → (↑a_1 : WithBot α) ≤ y) ↔ Option.some a ≤ y
Tactic: obtain _ | a := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x y : WithBot α
inst_1 : NoBotOrder α
⊢ (∀ (a : α), y ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ y
have none : (∀ (a : α), none ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ none
Tactic: obtain _ | y := y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
x y : WithBot α
inst_1 : NoBotOrder α
none : (∀ (a : α), Option.none ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ Option.none
⊢ (∀ (a : α), y ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ y
have some : ∀ (y : α), (∀ (a : α), Option.some y ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ Option.some y
Tactic: obtain _ | y := 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 α
x y : WithBot α
⊢ x ≤ y → y ≤ x → x = y
have bot : ⊥ ≤ y → y ≤ ⊥ → ⊥ = y
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 : PartialOrder α
x y : WithBot α
bot : ⊥ ≤ y → y ≤ ⊥ → ⊥ = y
⊢ x ≤ y → y ≤ x → x = y
have coe : ∀ (a : α), (↑a : WithBot α) ≤ y → y ≤ (↑a : WithBot α) → (↑a : WithBot α) = y
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 : PartialOrder α
y : WithBot α
⊢ ⊥ ≤ y → y ≤ ⊥ → ⊥ = y
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → Eq.{u_1 + 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 α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ ⊥ ≤ y → y ≤ ⊥ → ⊥ = y
have bot₁ : ∀ (a : α), ⊥ ≤ (↑a : WithBot α) → (↑a : WithBot α) ≤ ⊥ → ⊥ = (↑a : WithBot α)
Tactic: cases y
Cleared hypotheses: y