awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithBot α
a : αᵒᵈ
coe :
  (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ↔
    LE.le (α := WithBot α) (⊥ : WithBot α)
      ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
⊢ (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔
    y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)
have coe₁ : ∀ (a_1 : α),
  (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a_1 : WithBot α) ↔
    (↑a_1 : WithBot α) ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x y : WithBot α
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) x : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ x
have bot : LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
    ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
  y ≤ ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x y : WithBot α
bot :
  LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ ⊥
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) x : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ x
have coe : ∀ (a : α),
  LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    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 : WithBot α
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ ⊥
have bot : LE.le.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
    ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
  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 : LE α
y : WithBot α
bot :
  LE.le.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ ⊥
have bot₁ : ∀ (a : α),
  LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ) ↔
    (↑a : 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 : α
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ (↑a : WithBot α)
have coe : LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
    ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
  ⊥ ≤ (↑a : 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 : α
coe :
  LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    ⊥ ≤ (↑a : WithBot α)
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ (↑a : WithBot α)
have coe₁ : ∀ (a_1 : α),
  LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a_1 : WithBot α) : WithTop αᵒᵈ) ↔
    (↑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 : LE α
x : WithBot αᵒᵈ
y : WithTop α
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) x ≤ y ↔ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y ≤ x
have bot : (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ≤ y ↔
  LE.le (α := WithBot αᵒᵈ) ((WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ≤ y ↔
    LE.le (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) x ≤ y ↔ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y ≤ x
have coe : ∀ (a : αᵒᵈ),
  (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) ≤ y ↔
    (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ≤ y ↔
    LE.le (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
have bot : LE.le.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) (⊤ : WithTop α) ↔
  LE.le.{u_1} (α := WithBot αᵒᵈ) ((WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) (⊤ : WithTop α) ↔
    LE.le.{u_1} (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ≤ y ↔
    LE.le (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
have bot₁ : ∀ (a : α),
  (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ≤ (↑a : WithTop α) ↔
    LE.le (α := WithBot αᵒᵈ) ((WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) ≤ y ↔
    (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y ≤ (↑a : WithBot αᵒᵈ)
have coe : LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
    (⊤ : WithTop α) ↔
  (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      (⊤ : WithTop α) ↔
    (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ ≤ (↑a : WithBot αᵒᵈ)
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) ≤ y ↔
    (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y ≤ (↑a : WithBot αᵒᵈ)
have coe₁ : ∀ (a_1 : α),
  (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) ≤ (↑a_1 : WithTop α) ↔
    (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y ↔ y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) x
have top : LE.le (α := WithTop α) (⊤ : WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
  y ≤ (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤
⊢ x ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y ↔ y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) x
have coe : ∀ (a : α),
  (↑a : WithTop α) ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y ↔
    y ≤ (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤
have top : LE.le.{u_1} (α := WithTop α) (⊤ : WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
  LE.le.{u_1} (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ) ((WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LE.le.{u_1} (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ : WithBot αᵒᵈ)
⊢ LE.le (α := WithTop α) (⊤ : WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤
have top₁ : ∀ (a : αᵒᵈ),
  LE.le (α := WithTop α) (⊤ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α) ↔
    (↑a : WithBot αᵒᵈ) ≤ (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y ↔
    y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α)
have coe : (↑a : WithTop α) ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ↔
  LE.le (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
    ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑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 : α
coe :
  (↑a : WithTop α) ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ↔
    LE.le (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
      ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α) : WithBot αᵒᵈ)
⊢ (↑a : WithTop α) ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y ↔
    y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α)
have coe₁ : ∀ (a_1 : αᵒᵈ),
  (↑a : WithTop α) ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a_1 : WithBot αᵒᵈ) ↔
    (↑a_1 : WithBot αᵒᵈ) ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x y : WithBot αᵒᵈ
⊢ LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) x : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ x
have bot : LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
    ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
  y ≤ ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x y : WithBot αᵒᵈ
bot :
  LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ ⊥
⊢ LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) x : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ x
have coe : ∀ (a : αᵒᵈ),
  LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    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 : WithBot αᵒᵈ
⊢ LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ ⊥
have bot : LE.le.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
    ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
  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 : LE α
y : WithBot αᵒᵈ
bot :
  LE.le.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LE.le.{u_1} (α := WithBot αᵒᵈ) ⊥ ⊥
⊢ LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ ⊥
have bot₁ : ∀ (a : αᵒᵈ),
  LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α) ↔
    (↑a : 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 : αᵒᵈ
⊢ LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ (↑a : WithBot αᵒᵈ)
have coe : LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
    ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
  ⊥ ≤ (↑a : 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 : αᵒᵈ
coe :
  LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    ⊥ ≤ (↑a : WithBot αᵒᵈ)
⊢ LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ (↑a : WithBot αᵒᵈ)
have coe₁ : ∀ (a_1 : αᵒᵈ),
  LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a_1 : WithBot αᵒᵈ) : WithTop α) ↔
    (↑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 : LT α
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 ↔
  LT.lt (α := 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 : LT α
x : WithBot α
y : WithTop αᵒᵈ
bot :
  (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ < y ↔
    LT.lt (α := 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 : LT α
y : WithTop αᵒᵈ
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ < y ↔
    LT.lt (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y : WithBot α) (⊥ : WithBot α)
have bot : LT.lt.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ↔
  LT.lt.{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 : LT α
y : WithTop αᵒᵈ
bot :
  LT.lt.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ↔
    LT.lt.{u_1} (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α) (⊥ : WithBot α)
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ < y ↔
    LT.lt (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y : WithBot α) (⊥ : WithBot α)
have bot₁ : ∀ (a : αᵒᵈ),
  (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ < (↑a : WithTop αᵒᵈ) ↔
    LT.lt (α := 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 : LT α
y : WithTop αᵒᵈ
a : α
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) < y ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y < (↑a : WithBot α)
have coe : LT.lt (α := 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 : LT α
y : WithTop αᵒᵈ
a : α
coe :
  LT.lt (α := 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 : LT α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x < (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔ y < (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) x
have top : LT.lt (α := 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 : LT α
x : WithTop αᵒᵈ
y : WithBot α
top :
  LT.lt (α := 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 : LT α
y : WithBot α
⊢ LT.lt (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
have top : LT.lt.{u_1} (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
  LT.lt.{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 : LT α
y : WithBot α
top :
  LT.lt.{u_1} (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LT.lt.{u_1} (α := WithBot α) (⊥ : WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α)
⊢ LT.lt (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
have top₁ : ∀ (a : α),
  LT.lt (α := 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 : LT α
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 αᵒᵈ) ⊥ ↔
  LT.lt (α := WithBot α) (⊥ : WithBot α)
    ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
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 : WithTop αᵒᵈ) < (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ↔
    LT.lt (α := WithBot α) (⊥ : WithBot α)
      ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
⊢ (↑a : WithTop αᵒᵈ) < (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔
    y < (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)
have coe₁ : ∀ (a_1 : α),
  (↑a : WithTop αᵒᵈ) < (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a_1 : WithBot α) ↔
    (↑a_1 : WithBot α) < (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
⊢ LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) x : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < x
have bot : LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
    ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
  y < ⊥
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 :
  LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < ⊥
⊢ LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) x : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < x
have coe : ∀ (a : α),
  LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < (↑a : WithBot α)
Tactic: cases x
Cleared hypotheses: x