awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LT α
y : WithBot α
⊢ LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < ⊥
have bot : LT.lt.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
    ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
  LT.lt.{u_1} (α := WithBot α) ⊥ ⊥
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} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LT.lt.{u_1} (α := WithBot α) ⊥ ⊥
⊢ LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < ⊥
have bot₁ : ∀ (a : α),
  LT.lt (α := 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 : LT α
y : WithBot α
a : α
⊢ LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < (↑a : WithBot α)
have coe : LT.lt (α := 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 : LT α
y : WithBot α
a : α
coe :
  LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    ⊥ < (↑a : WithBot α)
⊢ LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < (↑a : WithBot α)
have coe₁ : ∀ (a_1 : α),
  LT.lt (α := 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 : LT α
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 ↔
  LT.lt (α := 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 : LT α
x : WithBot αᵒᵈ
y : WithTop α
bot :
  (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ < y ↔
    LT.lt (α := 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 : LT α
y : WithTop α
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ < y ↔
    LT.lt (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
have bot : LT.lt.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) (⊤ : WithTop α) ↔
  LT.lt.{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 : LT α
y : WithTop α
bot :
  LT.lt.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) (⊤ : WithTop α) ↔
    LT.lt.{u_1} (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ < y ↔
    LT.lt (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
have bot₁ : ∀ (a : α),
  (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ < (↑a : WithTop α) ↔
    LT.lt (α := 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 : LT α
y : WithTop α
a : αᵒᵈ
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) < y ↔
    (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y < (↑a : WithBot αᵒᵈ)
have coe : LT.lt (α := 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 : LT α
y : WithTop α
a : αᵒᵈ
coe :
  LT.lt (α := 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 : LT α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x < (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y ↔ y < (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) x
have top : LT.lt (α := 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 : LT α
x : WithTop α
y : WithBot αᵒᵈ
top :
  LT.lt (α := 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 : LT α
y : WithBot αᵒᵈ
⊢ LT.lt (α := WithTop α) (⊤ : WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤
have top : LT.lt.{u_1} (α := WithTop α) (⊤ : WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
  LT.lt.{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 : LT α
y : WithBot αᵒᵈ
top :
  LT.lt.{u_1} (α := WithTop α) (⊤ : WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LT.lt.{u_1} (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ : WithBot αᵒᵈ)
⊢ LT.lt (α := WithTop α) (⊤ : WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤
have top₁ : ∀ (a : αᵒᵈ),
  LT.lt (α := 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 : LT α
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 α) ⊥ ↔
  LT.lt (α := 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 : LT α
y : WithBot αᵒᵈ
a : α
coe :
  (↑a : WithTop α) < (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ↔
    LT.lt (α := 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 : LT α
x y : WithBot αᵒᵈ
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) x : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < x
have bot : LT.lt (α := 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 : LT α
x y : WithBot αᵒᵈ
bot :
  LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < ⊥
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) x : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < x
have coe : ∀ (a : αᵒᵈ),
  LT.lt (α := 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 : LT α
y : WithBot αᵒᵈ
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < ⊥
have bot : LT.lt.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
    ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
  LT.lt.{u_1} (α := WithBot αᵒᵈ) ⊥ ⊥
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} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LT.lt.{u_1} (α := WithBot αᵒᵈ) ⊥ ⊥
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < ⊥
have bot₁ : ∀ (a : αᵒᵈ),
  LT.lt (α := 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 : LT α
y : WithBot αᵒᵈ
a : αᵒᵈ
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < (↑a : WithBot αᵒᵈ)
have coe : LT.lt (α := 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 : LT α
y : WithBot αᵒᵈ
a : αᵒᵈ
coe :
  LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    ⊥ < (↑a : WithBot αᵒᵈ)
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < (↑a : WithBot αᵒᵈ)
have coe₁ : ∀ (a_1 : αᵒᵈ),
  LT.lt (α := 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.WithBotTop (goal)
Goal:
ι : Type u_1
inst : LE ι
a b : ι
⊢ coe a ≤ coe b ↔ a ≤ b
have rw : coe a ≤ coe b ↔ (↑a : WithTop ι) ≤ (↑b : WithTop ι)
Tactic: rw [← WithTop.coe_le_coe (α := ι)]
-- Lean 4 proof step from Mathlib.Order.WithBotTop (goal)
Goal:
ι : Type u_1
inst : LT ι
a b : ι
⊢ coe a < coe b ↔ a < b
have rw : coe a < coe b ↔ (↑a : WithTop ι) < (↑b : WithTop ι)
Tactic: rw [← WithTop.coe_lt_coe (α := ι)]
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ (ub : α), ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this_1 : ∃ (ub : α), ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ maxChain r
have rw : a ∈ insert a (maxChain r)
Tactic: rw [maxChain_spec.right this (subset_insert _ _)]
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
⊢ ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m
have refine_2 : ∀ (H : ∃ (m : α), Maximal (fun (x_1 : α) ↦ Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} x_1) m),
  ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m
Tactic: have H := zorn_le₀ ({ y ∈ s | x ≤ y }) fun c hcs hc => ?_
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
refine_2 :
  ∀ (H : ∃ (m : α), Maximal (fun (x_1 : α) ↦ Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} x_1) m),
    ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m
⊢ ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m
have refine_1 : ∀ (c : Set α) (hcs : c ⊆ {y : α | y ∈ s ∧ x ≤ y}) (hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c),
  ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub
Tactic: have H := zorn_le₀ ({ y ∈ s | x ≤ y }) fun c hcs hc => ?_
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
H : ∃ (m : α), Maximal (fun (x_1 : α) ↦ Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} x_1) m
⊢ ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m
have refine_2 : ∀ (m : α) (hm : ∀ ⦃y : α⦄, (fun (x_1 : α) ↦ Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} x_1) y → m ≤ y → y ≤ m)
  (hms : m ∈ s) (hxm : x ≤ m), ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m
Tactic: rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y : α | y ∈ s ∧ x ≤ y}
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
⊢ ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub
have refine_1 : ∀ (hcs : Subset.{u_1} (α := Set α) ∅ {y : α | y ∈ s ∧ x ≤ y}) (hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅),
  ∃ (ub : α),
    Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ (z : α), Membership.mem (γ := Set α) ∅ z → z ≤ ub
Tactic: rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
Cleared hypotheses: c, hcs, hc
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y : α | y ∈ s ∧ x ≤ y}
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
refine_1 :
  ∀ (hcs : Subset.{u_1} (α := Set α) ∅ {y : α | y ∈ s ∧ x ≤ y}) (hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅),
    ∃ (ub : α),
      Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ (z : α), Membership.mem (γ := Set α) ∅ z → z ≤ ub
⊢ ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub
have refine_1₁ : ∀ (y : α) (hy : y ∈ c), ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub
Tactic: rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y : α | y ∈ s ∧ x ≤ y}
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub
have refine_1 : ∀ (z : α) (hzs : z ∈ s) (hz : ∀ z_1 ∈ c, z_1 ≤ z),
  ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub
Tactic: rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
⊢ ∃ (m : α), x ≤ m ∧ IsMax m
have refine_2 : ∀ (m : α) (hxm : x ≤ m) (ham : m ∈ Ici a) (hm : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ Ici a) y → m ≤ y → y ≤ m),
  ∃ (m : α), x ≤ m ∧ IsMax m
Tactic: let ⟨m, hxm, ham, hm⟩ := zorn_le_nonempty₀ (Ici a) (fun c hca hc y hy ↦ ?_) x hax
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
refine_2 :
  ∀ (m : α) (hxm : x ≤ m) (ham : m ∈ Ici a) (hm : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ Ici a) y → m ≤ y → y ≤ m),
    ∃ (m : α), x ≤ m ∧ IsMax m
⊢ ∃ (m : α), x ≤ m ∧ IsMax m
have refine_1 : ∀ (c : Set α) (hca : c ⊆ Ici a) (hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c) (y : α) (hy : y ∈ c),
  ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub
Tactic: let ⟨m, hxm, ham, hm⟩ := zorn_le_nonempty₀ (Ici a) (fun c hca hc y hy ↦ ?_) x hax
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub
have refine_1 : ∀ (ub : α) (hub : ∀ z ∈ c, z ≤ ub), ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub
Tactic: have ⟨ub, hub⟩ := ih c hca hc y hy
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M
have refine_2 : ∀
  (H :
    ∃ (m : Set α),
      c ⊆ m ∧ Maximal (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} x) m),
  ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M
Tactic: have H := zorn_subset_nonempty { s | c ⊆ s ∧ IsChain r s } ?_ c ⟨Subset.rfl, hc⟩
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
refine_2 :
  ∀
    (H :
      ∃ (m : Set α),
        c ⊆ m ∧ Maximal (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} x) m),
    ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M
⊢ ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M
have refine_1 : ∀ c_1 ⊆ {s : Set α | c ⊆ s ∧ IsChain r s},
  IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c_1 →
    c_1.Nonempty →
      ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} ub ∧ ∀ s ∈ c_1, s ⊆ ub
Tactic: have H := zorn_subset_nonempty { s | c ⊆ s ∧ IsChain r s } ?_ c ⟨Subset.rfl, hc⟩
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
H :
  ∃ (m : Set α),
    c ⊆ m ∧ Maximal (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} x) m
⊢ ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M
have refine_2 : ∀ (M : Set α) (hcM : c ⊆ M)
  (hM : Maximal (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} x) M),
  ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M
Tactic: obtain ⟨M, hcM, hM⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} ub ∧ ∀ s ∈ cs, s ⊆ ub
have refine_1 : IsChain r (⋃₀ cs)
Tactic: refine
    ⟨⋃₀cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, ?_⟩, fun _ =>
      Set.subset_sUnion_of_mem⟩
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
⊢ r y z ∨ r z y
have refine_1 : ∀ (hsz : sy ∈ cs) (hzsz : z ∈ sy), r y z ∨ r z y
Tactic: obtain rfl | hsseq := eq_or_ne sy sz
Cleared hypotheses: sz, hsz, hzsz
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
refine_1 : ∀ (hsz : sy ∈ cs) (hzsz : z ∈ sy), r y z ∨ r z y
⊢ r y z ∨ r z y
have refine_1₁ : ∀ (hsseq : sy ≠ sz), r y z ∨ r z y
Tactic: obtain rfl | hsseq := eq_or_ne sy sz
-- Lean 4 proof step from Mathlib.Order.Zorn (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
⊢ r y z ∨ r z y
have refine_1 : ∀ (h : sy ⊆ sz), r y z ∨ r z y
Tactic: rcases hcs₁ hsy hsz hsseq with h | h