awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
rw : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw₁ : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) ((a₂, b₂).2, (a₂, b₂).1) ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
⊢ GameAdd rβ rα (a₁, b₁).swap (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
have rw₂ : rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ∨ rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ↔
  GameAdd rα rβ (a₁, b₁) (a₂, b₂)
Tactic: rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
rw : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw₁ : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) ((a₂, b₂).2, (a₂, b₂).1) ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw₂ :
  rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ∨ rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ↔
    GameAdd rα rβ (a₁, b₁) (a₂, b₂)
⊢ GameAdd rβ rα (a₁, b₁).swap (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
have rw₃ : rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ∨ rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ↔
  rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂
Tactic: rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
rw : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw₁ : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) ((a₂, b₂).2, (a₂, b₂).1) ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw₂ :
  rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ∨ rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ↔
    GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw₃ :
  rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ∨ rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ↔
    rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂
⊢ GameAdd rβ rα (a₁, b₁).swap (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
have rw₄ : rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ∨ rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ↔
  rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂
Tactic: rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a : α
b : β
ha : Acc rα a
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
have intro : ∀ (a : α),
  (∀ (y : α), rα y a → Acc rα y) →
    ∀ (iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)) {b : β} (hb : Acc rβ b),
      Acc (Prod.GameAdd rα rβ) (a, b)
Tactic: induction ha generalizing b with | _ a _ iha
Cleared hypotheses: b, ha, hb
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)
b : β
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
have intro : ∀ (b : β) (hb : ∀ (y : β), rβ y b → Acc rβ y) (ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)),
  Acc (Prod.GameAdd rα rβ) (a, b)
Tactic: induction hb with | _ b hb ihb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)
b_1 b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
have intro : ∀ (h : α × β), Prod.GameAdd rα rβ h (a, b) → Acc (Prod.GameAdd rα rβ) h
Tactic: refine Acc.intro _ fun h => ?_
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα_1 : α → α → Prop
rβ : β → β → Prop
a : α
b : β
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (a₁, b₁) (b₂, a₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (b₂, a₂))
have rw : (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
    (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
  (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
    (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))
Tactic: rw [Prod.gameAdd_swap_swap_mk _ _ b₁ b₂ a₁ a₂, Prod.gameAdd_swap_swap_mk _ _ a₁ b₂ b₁ a₂]
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(b, a₂)
have rw : GameAdd rα s(b, a₁) s(b, a₂)
Tactic: rw [Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(b, a₁) s(a₂, b)
have rw : GameAdd rα s(a₁, b) s(a₂, b)
Tactic: rw [Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
rα : α → α → Prop
a b : α
ha : Acc rα a
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) s(a, b)
have intro : ∀ (a : α),
  (∀ (y : α), rα y a → Acc rα y) →
    ∀ (iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)) {b : α} (hb : Acc rα b),
      Acc (Sym2.GameAdd rα) s(a, b)
Tactic: induction ha generalizing b with | _ a _ iha
Cleared hypotheses: b, ha, hb
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b : α
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) s(a, b)
have intro : ∀ (b : α) (hb : ∀ (y : α), rα y b → Acc rα y) (ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)),
  Acc (Sym2.GameAdd rα) s(a, b)
Tactic: induction hb with | _ b hb ihb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
⊢ Acc (Sym2.GameAdd rα) s(a, b)
have intro : ∀ (s : Sym2 α), Sym2.GameAdd rα s s(a, b) → Acc (Sym2.GameAdd rα) s
Tactic: refine Acc.intro _ fun s => ?_
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
s : Sym2 α
⊢ Sym2.GameAdd rα s s(a, b) → Acc (Sym2.GameAdd rα) s
have intro : ∀ (c d : α), Sym2.GameAdd rα s(c, d) s(a, b) → Acc (Sym2.GameAdd rα) s(c, d)
Tactic: induction s with | _ c d
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c d : α
⊢ (Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯)
      s(c, d) s(a, b) →
    Acc
      ((Sym2.lift₂ :
          (a :
              { f : α → α → α → α → Prop //
                ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
            Sym2 α → Sym2 α → Prop)
        (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
          ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
          (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
      s(c, d)
have intro : Prod.GameAdd rα rα (c, d) (a, b) ∨ Prod.GameAdd rα rα (d, c) (a, b) →
  Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) sorry))
    s(c, d)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(b, d)
have intro : Acc
  ((Sym2.lift₂ :
      (a :
          { f : α → α → α → α → Prop //
            ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
        Sym2 α → Sym2 α → Prop)
    (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
      ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
      (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) sorry))
  s(d, b)
Tactic: rw [Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c b
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(c, a)
have intro : Acc
  ((Sym2.lift₂ :
      (a :
          { f : α → α → α → α → Prop //
            ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
        Sym2 α → Sym2 α → Prop)
    (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
      ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
      (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) sorry))
  s(a, c)
Tactic: rw [Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
n : ℕ
inst_4 : GradeMinOrder (Fin n) α
a : Fin n
h : IsMin a
⊢ IsMin (↑a : ℕ)
have zero : ∀ [GradeMinOrder (Fin 0) α] (a : Fin 0) (h : IsMin a), IsMin (↑a : ℕ)
Tactic: cases n
Cleared hypotheses: n, inst_4, a, h
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
n : ℕ
inst_4 : GradeMinOrder (Fin n) α
a : Fin n
h : IsMin a
zero : ∀ [GradeMinOrder (Fin 0) α] (a : Fin 0) (h : IsMin a), IsMin (↑a : ℕ)
⊢ IsMin (↑a : ℕ)
have succ : ∀ (n : ℕ) [GradeMinOrder (Fin (n + 1)) α] (a : Fin (n + 1)) (h : IsMin a), IsMin (↑a : ℕ)
Tactic: cases n
Cleared hypotheses: n, inst_4, a, h
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
n : ℕ
inst_4 : GradeMinOrder (Fin (n + 1)) α
a : Fin (n + 1)
h : IsMin a
⊢ IsMin (↑a : ℕ)
have succ : IsMin (↑0 : ℕ)
Tactic: rw [h.eq_bot, bot_eq_zero]
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
⊢ (↑a : α) ⩿ (↑b : α) ↔ a ⩿ b
have refine : ∀ (h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b) (c : α) (hac : (↑a : α) < c) (hcb : c < (↑b : α)) (d : α) (hd : d ∈ s), c ≤ d ∨ d ≤ c
Tactic: refine and_congr_right' ⟨fun h c hac ↦ h hac, fun h c hac hcb ↦
    @h ⟨c, mem_iff_forall_le_or_ge.2 fun d hd ↦ ?_⟩ hac hcb⟩
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
⊢ c ≤ d ∨ d ≤ c
have inl : ∀ (hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a), c ≤ d ∨ d ≤ c
Tactic: obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
inl : ∀ (hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a), c ≤ d ∨ d ≤ c
⊢ c ≤ d ∨ d ≤ c
have inr : ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd), c ≤ d ∨ d ≤ c
Tactic: obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
⊢ c ≤ d ∨ d ≤ c
have inr : ∀ (hbd : b ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd), c ≤ d ∨ d ≤ c
Tactic: obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
inr : ∀ (hbd : b ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd), c ≤ d ∨ d ≤ c
⊢ c ≤ d ∨ d ≤ c
have inr₁ : ∀ (hdb : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd < b), c ≤ d ∨ d ≤ c
Tactic: obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
⊢ c ≤ d ∨ d ≤ c
have inl : ∀ (hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a), c ≤ d ∨ d ≤ c
Tactic: classical
  obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
  · exact .inr ((Subtype.coe_le_coe.2 hda).trans hac.le)
  obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
  · exact .inl (hcb.le.trans hbd)
  · cases h had hdb
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
inl : ∀ (hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a), c ≤ d ∨ d ≤ c
⊢ c ≤ d ∨ d ≤ c
have inr : ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd), c ≤ d ∨ d ≤ c
Tactic: classical
  obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
  · exact .inr ((Subtype.coe_le_coe.2 hda).trans hac.le)
  obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
  · exact .inl (hcb.le.trans hbd)
  · cases h had hdb
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
inl : ∀ (hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a), c ≤ d ∨ d ≤ c
inr inr₁ : ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd), c ≤ d ∨ d ≤ c
⊢ c ≤ d ∨ d ≤ c
have inr₂ : ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd) (hbd : b ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd),
  c ≤ d ∨ d ≤ c
Tactic: classical
  obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
  · exact .inr ((Subtype.coe_le_coe.2 hda).trans hac.le)
  obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
  · exact .inl (hcb.le.trans hbd)
  · cases h had hdb
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
inl : ∀ (hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a), c ≤ d ∨ d ≤ c
inr inr₁ : ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd), c ≤ d ∨ d ≤ c
inr₂ :
  ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd) (hbd : b ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd),
    c ≤ d ∨ d ≤ c
⊢ c ≤ d ∨ d ≤ c
have inr₃ : ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd) (hdb : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd < b),
  c ≤ d ∨ d ≤ c
Tactic: classical
  obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
  · exact .inr ((Subtype.coe_le_coe.2 hda).trans hac.le)
  obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
  · exact .inl (hcb.le.trans hbd)
  · cases h had hdb
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMax a
b : α
hab : (↑a : α) ≤ b
⊢ b ≤ (↑a : α)
have refine : ∀ (c : α) (hc : c ∈ s), b ≤ c ∨ c ≤ b
Tactic: refine @h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hab
-- Lean 4 proof step from Mathlib.Order.Grade (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMin a
b : α
hba : b ≤ (↑a : α)
⊢ (↑a : α) ≤ b
have refine : ∀ (c : α) (hc : c ∈ s), b ≤ c ∨ c ≤ b
Tactic: refine @h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hba
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
have pos : ∀ (h' : n = 0), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
Tactic: by_cases h' : n = 0
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
pos : ∀ (h' : n = 0), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
have neg : ∀ (h' : ¬n = 0), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
Tactic: by_cases h' : n = 0
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : ¬n = 0
⊢ ∃ t ⊆ s, IsChain r t ∧ (↑n : ℕ∞) ≤ t.encard
have contrapose! : ∀ (h : ∀ (t : Set α) (_ : t ⊆ s) (_ : IsChain r t), t.encard < (↑n : ℕ∞)), s.chainHeight r < (↑n : ℕ∞)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h' : ¬n = 0
h : ∀ (t : Set α) (_ : t ⊆ s) (_ : IsChain r t), t.encard < (↑n : ℕ∞)
⊢ s.chainHeight r < (↑n : ℕ∞)
have refine : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 < (↑n : ℕ∞)
Tactic: refine iSup_lt_iff.mpr ⟨n - 1, ?_, fun m ↦ ENat.le_sub_one_of_lt <| h m.1 m.2.1 m.2.2⟩
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : ¬n = 0
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
have neg : ∀ (t : Set α) (ht₁ : t ⊆ s) (ht₂ : IsChain r t) (ht₃ : (↑n : ℕ∞) ≤ t.encard),
  ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
Tactic: obtain ⟨t, ht₁, ht₂, ht₃⟩ : ∃ t ⊆ s, IsChain r t ∧ n ≤ t.encard := by
      contrapose! h
      refine iSup_lt_iff.mpr ⟨n - 1, ?_, fun m ↦ ENat.le_sub_one_of_lt <| h m.1 m.2.1 m.2.2⟩
      exact_mod_cast Nat.sub_one_lt h'
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : ¬n = 0
t : Set α
ht₁ : t ⊆ s
ht₂ : IsChain r t
ht₃ : (↑n : ℕ∞) ≤ t.encard
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
have neg : ∀ (u : Set α) (hu₁ : u ⊆ t) (hu₂ : u.encard = (↑n : ℕ∞)), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
Tactic: obtain ⟨u, hu₁, hu₂⟩ := exists_subset_encard_eq ht₃
-- Lean 4 proof step from Mathlib.Order.Height (hypothesis)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
⊢ ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t
have this : Nonempty.{max 1 (u_1 + 1)} { t : Set α // t ⊆ s ∧ IsChain r t }
Tactic: have : Nonempty { t // t ⊆ s ∧ IsChain r t } := ⟨∅, by simp⟩
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
this : Nonempty.{max 1 (u_1 + 1)} { t : Set α // t ⊆ s ∧ IsChain r t }
⊢ LT.lt (α := ℕ∞) (⨆ (i : { t : Set α // t ⊆ s ∧ IsChain r t }), (↑i : Set α).encard) ⊤
have rwa : s.chainHeight r < ⊤
Tactic: rwa [← chainHeight_eq_iSup, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
this : Nonempty.{max 1 (u_1 + 1)} { t : Set α // t ⊆ s ∧ IsChain r t }
⊢ ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t
have obtain : ∀ (t : { t : Set α // t ⊆ s ∧ IsChain r t })
  (ht : (↑t : Set α).encard = ⨆ (i : { t : Set α // t ⊆ s ∧ IsChain r t }), (↑i : Set α).encard),
  ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t
Tactic: obtain ⟨t, ht⟩ := exists_eq_iSup_of_lt_top (by rwa [← chainHeight_eq_iSup, lt_top_iff_ne_top])
-- Lean 4 proof step from Mathlib.Order.Height (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
ht : t ⊆ s
he : s.chainHeight r < t.encard
hh : IsChain r t
⊢ False
have he₁ : s.chainHeight r < s.chainHeight r
Tactic: grw [encard_le_chainHeight_of_isChain _ _ ht hh] at he
Cleared hypotheses: he, hh
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r = ⊤ ↔ ∀ (n : ℕ), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
have refine : ∀ (h : ∀ (n : ℕ), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t), s.chainHeight r = ⊤
Tactic: refine ⟨fun h _ ↦ exists_isChain_of_le_chainHeight _ (le_top.trans_eq h.symm), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : ∀ (n : ℕ), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
⊢ s.chainHeight r = ⊤
have contrapose! : ∀ (h : s.chainHeight r ≠ ⊤), ∃ (n : ℕ), ∀ (t : Set α) (_ : t ⊆ s) (_ : t.encard = (↑n : ℕ∞)), ¬IsChain r t
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
⊢ ∃ (n : ℕ), ∀ (t : Set α) (_ : t ⊆ s) (_ : t.encard = (↑n : ℕ∞)), ¬IsChain r t
have obtain : ∀ (n : ℕ) (hn : (↑n : WithTop ℕ) = s.chainHeight r),
  ∃ (n : ℕ), ∀ (t : Set α) (_ : t ⊆ s) (_ : t.encard = (↑n : ℕ∞)), ¬IsChain r t
Tactic: obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 h
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = s.chainHeight r
⊢ ∃ (n : ℕ), ∀ (t : Set α) (_ : t ⊆ s) (_ : t.encard = (↑n : ℕ∞)), ¬IsChain r t
have refine : ∀ (l : Set α) (hl : l ⊆ s) (he : l.encard = (↑(n + 1) : ℕ∞)), s.chainHeight r < l.encard
Tactic: refine ⟨n + 1, fun l hl he ↦ not_isChain_of_chainHeight_lt_encard r s l hl ?_⟩
-- Lean 4 proof step from Mathlib.Order.Height (goal)
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = s.chainHeight r
l : Set α
hl : l ⊆ s
he : l.encard = (↑(n + 1) : ℕ∞)
⊢ s.chainHeight r < l.encard
have rw : n < n + 1
Tactic: rw [← hn, some_eq_coe, he, Nat.cast_lt]