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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : WithTop α
top : ⊤ ≤ y ∨ y ≤ ⊤
⊢ x ≤ y ∨ y ≤ x
have coe : ∀ (a : α), (↑a : WithTop α) ≤ y ∨ y ≤ (↑a : WithTop α)
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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithTop α
⊢ ⊤ ≤ y ∨ y ≤ ⊤
have top : LE.le.{u_1} (α := WithTop α) ⊤ ⊤ ∨ LE.le.{u_1} (α := WithTop α) ⊤ ⊤
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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithTop α
top : LE.le.{u_1} (α := WithTop α) ⊤ ⊤ ∨ LE.le.{u_1} (α := WithTop α) ⊤ ⊤
⊢ ⊤ ≤ y ∨ y ≤ ⊤
have top₁ : ∀ (a : α), ⊤ ≤ (↑a : WithTop α) ∨ (↑a : WithTop α) ≤ ⊤
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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithTop α
a_1 : α
⊢ (↑a_1 : WithTop α) ≤ y ∨ y ≤ (↑a_1 : WithTop α)
have coe : (↑a_1 : WithTop α) ≤ ⊤ ∨ ⊤ ≤ (↑a_1 : WithTop α)
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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithTop α
a_1 : α
coe : (↑a_1 : WithTop α) ≤ ⊤ ∨ ⊤ ≤ (↑a_1 : WithTop α)
⊢ (↑a_1 : WithTop α) ≤ y ∨ y ≤ (↑a_1 : WithTop α)
have coe₁ : ∀ (a : α), (↑a_1 : WithTop α) ≤ (↑a : WithTop α) ∨ (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a_1 a_2 : α
⊢ (↑a_1 : WithTop α) ≤ (↑a_2 : WithTop α) ∨ (↑a_2 : WithTop α) ≤ (↑a_1 : WithTop α)
have coe : a_1 ≤ a_2 ∨ a_2 ≤ a_1
Tactic: simp
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
⊢ DenselyOrdered.{u_1} (WithBot α) ↔ DenselyOrdered α
have mp : DenselyOrdered.{u_1} (WithBot α) → DenselyOrdered α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
mp : DenselyOrdered.{u_1} (WithBot α) → DenselyOrdered α
⊢ DenselyOrdered.{u_1} (WithBot α) ↔ DenselyOrdered α
have mpr : DenselyOrdered α → DenselyOrdered.{u_1} (WithBot α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
⊢ DenselyOrdered α
have mp : ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered α
⊢ DenselyOrdered.{u_1} (WithBot α)
have mpr : ∀ (a₁ a₂ : WithBot α), a₁ < a₂ → ∃ (a : WithBot α), a₁ < a ∧ a < a₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
a b : α
hab : a < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b
have mp : ∀ (c : WithBot α) (hc : (↑a : WithBot α) < c ∧ c < (↑b : WithBot α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
Tactic: obtain ⟨c, hc⟩ := exists_between (WithBot.coe_lt_coe.mpr hab)
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
a b : α
hab : a < b
c : WithBot α
hc : (↑a : WithBot α) < c ∧ c < (↑b : WithBot α)
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b
have mp : ∀ (hc : (↑a : WithBot α) < ⊥ ∧ ⊥ < (↑b : WithBot α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
Tactic: induction c with
    | bot => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
a b : α
hab : a < b
c : WithBot α
hc : (↑a : WithBot α) < c ∧ c < (↑b : WithBot α)
mp : ∀ (hc : (↑a : WithBot α) < ⊥ ∧ ⊥ < (↑b : WithBot α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b
have mp₁ : ∀ (c : α) (hc : (↑a : WithBot α) < (↑c : WithBot α) ∧ (↑c : WithBot α) < (↑b : WithBot α)),
  ∃ (a_1 : α), a < a_1 ∧ a_1 < b
Tactic: induction c with
    | bot => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
⊢ DenselyOrdered.{u_1} (WithTop α) ↔ DenselyOrdered α
have mp : DenselyOrdered.{u_1} (WithTop α) → DenselyOrdered α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
mp : DenselyOrdered.{u_1} (WithTop α) → DenselyOrdered α
⊢ DenselyOrdered.{u_1} (WithTop α) ↔ DenselyOrdered α
have mpr : DenselyOrdered α → DenselyOrdered.{u_1} (WithTop α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
⊢ DenselyOrdered α
have mp : ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered α
⊢ DenselyOrdered.{u_1} (WithTop α)
have mpr : ∀ (a₁ a₂ : WithTop α), a₁ < a₂ → ∃ (a : WithTop α), a₁ < a ∧ a < a₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
a b : α
hab : a < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b
have mp : ∀ (c : WithTop α) (hc : (↑a : WithTop α) < c ∧ c < (↑b : WithTop α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
Tactic: obtain ⟨c, hc⟩ := exists_between (WithTop.coe_lt_coe.mpr hab)
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
a b : α
hab : a < b
c : WithTop α
hc : (↑a : WithTop α) < c ∧ c < (↑b : WithTop α)
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b
have mp : ∀ (hc : (↑a : WithTop α) < ⊤ ∧ ⊤ < (↑b : WithTop α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
Tactic: induction c with
    | top => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
a b : α
hab : a < b
c : WithTop α
hc : (↑a : WithTop α) < c ∧ c < (↑b : WithTop α)
mp : ∀ (hc : (↑a : WithTop α) < ⊤ ∧ ⊤ < (↑b : WithTop α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b
have mp₁ : ∀ (c : α) (hc : (↑a : WithTop α) < (↑c : WithTop α) ∧ (↑c : WithTop α) < (↑b : WithTop α)),
  ∃ (a_1 : α), a < a_1 ∧ a_1 < b
Tactic: induction c with
    | top => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩
Cleared hypotheses: c, hc
-- 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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
y : WithBot α
⊢ ⊥ < y ∨ ⊥ = y ∨ y < ⊥
have bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∨ LT.lt.{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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
y : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∨ LT.lt.{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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
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
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
x y : WithTop α
⊢ x < y ∨ x = y ∨ y < x
have top : ⊤ < 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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
x y : WithTop α
top : ⊤ < y ∨ ⊤ = y ∨ y < ⊤
⊢ x < y ∨ x = y ∨ y < x
have coe : ∀ (a : α), (↑a : WithTop α) < y ∨ (↑a : WithTop α) = y ∨ y < (↑a : WithTop α)
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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
y : WithTop α
⊢ ⊤ < y ∨ ⊤ = y ∨ y < ⊤
have top : LT.lt.{u_1} (α := WithTop α) ⊤ ⊤ ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ LT.lt.{u_1} (α := WithTop α) ⊤ ⊤
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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
y : WithTop α
top : LT.lt.{u_1} (α := WithTop α) ⊤ ⊤ ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ LT.lt.{u_1} (α := WithTop α) ⊤ ⊤
⊢ ⊤ < y ∨ ⊤ = y ∨ y < ⊤
have top₁ : ∀ (a : α), ⊤ < (↑a : WithTop α) ∨ ⊤ = (↑a : WithTop α) ∨ (↑a : WithTop α) < ⊤
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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
y : WithTop α
a_1 : α
⊢ (↑a_1 : WithTop α) < y ∨ (↑a_1 : WithTop α) = y ∨ y < (↑a_1 : WithTop α)
have coe : (↑a_1 : WithTop α) < ⊤ ∨ (↑a_1 : WithTop α) = ⊤ ∨ ⊤ < (↑a_1 : WithTop α)
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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
y : WithTop α
a_1 : α
coe : (↑a_1 : WithTop α) < ⊤ ∨ (↑a_1 : WithTop α) = ⊤ ∨ ⊤ < (↑a_1 : WithTop α)
⊢ (↑a_1 : WithTop α) < y ∨ (↑a_1 : WithTop α) = y ∨ y < (↑a_1 : WithTop α)
have coe₁ : ∀ (a : α),
  (↑a_1 : WithTop α) < (↑a : WithTop α) ∨ (↑a_1 : WithTop α) = (↑a : WithTop α) ∨ (↑a : WithTop α) < (↑a_1 : WithTop α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
⊢ (∀ (z : α), x < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ x
have bot : (∀ (z : α), ⊥ < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
bot : (∀ (z : α), ⊥ < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ ⊥
⊢ (∀ (z : α), x < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ x
have coe : ∀ (a : α), (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ (↑a : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
⊢ (∀ (z : α), ⊥ < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ ⊥
have bot : (∀ (z : α), ⊥ < (↑z : WithBot α) → ⊥ ≤ (↑z : 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
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
bot : (∀ (z : α), ⊥ < (↑z : WithBot α) → ⊥ ≤ (↑z : WithBot α)) ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ (∀ (z : α), ⊥ < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ ⊥
have bot₁ : ∀ (a : α), (∀ (z : α), ⊥ < (↑z : WithBot α) → (↑a : WithBot α) ≤ (↑z : WithBot α)) ↔ (↑a : WithBot α) ≤ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
⊢ (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ (↑a : WithBot α)
have coe : (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → ⊥ ≤ (↑z : WithBot α)) ↔ ⊥ ≤ (↑a : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
coe : (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → ⊥ ≤ (↑z : WithBot α)) ↔ ⊥ ≤ (↑a : WithBot α)
⊢ (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ (↑a : WithBot α)
have coe₁ : ∀ (a_1 : α),
  (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → (↑a_1 : WithBot α) ≤ (↑z : 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
inst : LinearOrder α
x y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
⊢ (∀ (z : α), (↑z : WithBot α) < x → (↑z : WithBot α) ≤ y) ↔ x ≤ y
have bot : (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ y) ↔ ⊥ ≤ y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
bot : (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ y) ↔ ⊥ ≤ y
⊢ (∀ (z : α), (↑z : WithBot α) < x → (↑z : WithBot α) ≤ y) ↔ x ≤ y
have coe : ∀ (a : α), (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ y) ↔ (↑a : WithBot α) ≤ y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
⊢ (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ y) ↔ ⊥ ≤ y
have bot : (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : 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
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
bot : (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ ⊥) ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ y) ↔ ⊥ ≤ y
have bot₁ : ∀ (a : α), (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ (↑a : WithBot α)) ↔ ⊥ ≤ (↑a : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
⊢ (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ y) ↔ (↑a : WithBot α) ≤ y
have coe : (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ ⊥) ↔ (↑a : WithBot α) ≤ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
coe : (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ ⊥) ↔ (↑a : WithBot α) ≤ ⊥
⊢ (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ y) ↔ (↑a : WithBot α) ≤ y
have coe₁ : ∀ (a_1 : α),
  (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ (↑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 α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a b : WithBot α
⊢ a < b ↔ ∃ (x : α), (↑x : WithBot α) < b ∧ a < (↑x : WithBot α)
have rw : (∃ (x : α), a < (↑x : WithBot α) ∧ (↑x : WithBot α) < b) ↔ ∃ (x : α), (↑x : WithBot α) < b ∧ a < (↑x : WithBot α)
Tactic: rw [lt_iff_exists_coe_btwn]
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x : WithBot α
y : WithTop αᵒᵈ
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) x ≤ y ↔ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y ≤ x
have bot : (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ≤ y ↔
  LE.le (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y : WithBot α) (⊥ : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x : WithBot α
y : WithTop αᵒᵈ
bot :
  (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ≤ y ↔
    LE.le (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y : WithBot α) (⊥ : WithBot α)
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) x ≤ y ↔ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y ≤ x
have coe : ∀ (a : α),
  (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) ≤ y ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y ≤ (↑a : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithTop αᵒᵈ
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ≤ y ↔
    LE.le (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y : WithBot α) (⊥ : WithBot α)
have bot : LE.le.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ↔
  LE.le.{u_1} (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α) (⊥ : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithTop αᵒᵈ
bot :
  LE.le.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ↔
    LE.le.{u_1} (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α) (⊥ : WithBot α)
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ≤ y ↔
    LE.le (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y : WithBot α) (⊥ : WithBot α)
have bot₁ : ∀ (a : αᵒᵈ),
  (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ≤ (↑a : WithTop αᵒᵈ) ↔
    LE.le (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
      (⊥ : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithTop αᵒᵈ
a : α
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) ≤ y ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y ≤ (↑a : WithBot α)
have coe : LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
    (⊤ : WithTop αᵒᵈ) ↔
  (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ ≤ (↑a : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithTop αᵒᵈ
a : α
coe :
  LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      (⊤ : WithTop αᵒᵈ) ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ ≤ (↑a : WithBot α)
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) ≤ y ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y ≤ (↑a : WithBot α)
have coe₁ : ∀ (a_1 : αᵒᵈ),
  (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) ≤ (↑a_1 : WithTop αᵒᵈ) ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a_1 : WithTop αᵒᵈ) ≤ (↑a : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔ y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) x
have top : LE.le (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
  y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x : WithTop αᵒᵈ
y : WithBot α
top :
  LE.le (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
⊢ x ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔ y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) x
have coe : ∀ (a : αᵒᵈ),
  (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔
    y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithBot α
⊢ LE.le (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
have top : LE.le.{u_1} (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
  LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithBot α
top :
  LE.le.{u_1} (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α)
⊢ LE.le (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
have top₁ : ∀ (a : α),
  LE.le (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ) ↔
    (↑a : WithBot α) ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithBot α
a : αᵒᵈ
⊢ (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔
    y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)
have coe : (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ↔
  LE.le (α := WithBot α) (⊥ : WithBot α)
    ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
Tactic: cases y
Cleared hypotheses: y