awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr
have oadd : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b.repr = succ (a.oadd m b').repr
Tactic: rw [repr, ihb.1, succ_eq_add_one, succ_eq_add_one, ← add_assoc, repr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
oadd : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b.repr = succ (a.oadd m b').repr
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr
have oadd₁ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + succ b'.repr = succ (a.oadd m b').repr
Tactic: rw [repr, ihb.1, succ_eq_add_one, succ_eq_add_one, ← add_assoc, repr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
oadd : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b.repr = succ (a.oadd m b').repr
oadd₁ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + succ b'.repr = succ (a.oadd m b').repr
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr
have oadd₂ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + (b'.repr + 1) = succ (a.oadd m b').repr
Tactic: rw [repr, ihb.1, succ_eq_add_one, succ_eq_add_one, ← add_assoc, repr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
oadd : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b.repr = succ (a.oadd m b').repr
oadd₁ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + succ b'.repr = succ (a.oadd m b').repr
oadd₂ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + (b'.repr + 1) = succ (a.oadd m b').repr
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr
have oadd₃ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + (b'.repr + 1) = (a.oadd m b').repr + 1
Tactic: rw [repr, ihb.1, succ_eq_add_one, succ_eq_add_one, ← add_assoc, repr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
oadd : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b.repr = succ (a.oadd m b').repr
oadd₁ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + succ b'.repr = succ (a.oadd m b').repr
oadd₂ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + (b'.repr + 1) = succ (a.oadd m b').repr
oadd₃ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + (b'.repr + 1) = (a.oadd m b').repr + 1
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr
have oadd₄ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b'.repr + 1 = (a.oadd m b').repr + 1
Tactic: rw [repr, ihb.1, succ_eq_add_one, succ_eq_add_one, ← add_assoc, repr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
oadd : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b.repr = succ (a.oadd m b').repr
oadd₁ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + succ b'.repr = succ (a.oadd m b').repr
oadd₂ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + (b'.repr + 1) = succ (a.oadd m b').repr
oadd₃ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + (b'.repr + 1) = (a.oadd m b').repr + 1
oadd₄ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b'.repr + 1 = (a.oadd m b').repr + 1
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr
have oadd₅ : ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b'.repr + 1 = ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b'.repr + 1
Tactic: rw [repr, ihb.1, succ_eq_add_one, succ_eq_add_one, ← add_assoc, repr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
H : (a.oadd m b).NF
⊢ b'.repr < ω ^ a.repr
have this : b.repr < ω ^ a.repr
Tactic: have := H.snd'.repr_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
H : (a.oadd m b).NF
this : b.repr < ω ^ a.repr
⊢ b'.repr < ω ^ a.repr
have this₁ : succ b'.repr < ω ^ a.repr
Tactic: rw [ihb.1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
ihb :
  IsSuccLimit b.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ (i : ℕ), a < (f i).repr
e : b.fundamentalSequence = Sum.inr f
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m (f i)).repr
have h1 : IsSuccLimit b.repr
Tactic: rcases ihb with ⟨h1, h2, h3⟩
Cleared hypotheses: ihb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
ihb :
  IsSuccLimit b.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ (i : ℕ), a < (f i).repr
e : b.fundamentalSequence = Sum.inr f
h1 : IsSuccLimit b.repr
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m (f i)).repr
have h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)
Tactic: rcases ihb with ⟨h1, h2, h3⟩
Cleared hypotheses: ihb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
ihb :
  IsSuccLimit b.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ (i : ℕ), a < (f i).repr
e : b.fundamentalSequence = Sum.inr f
h1 : IsSuccLimit b.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m (f i)).repr
have h3 : ∀ a < b.repr, ∃ (i : ℕ), a < (f i).repr
Tactic: rcases ihb with ⟨h1, h2, h3⟩
Cleared hypotheses: ihb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
x : ONote
o : ONote := x
a : ONote
h : o.FundamentalSequenceProp (Sum.inl (some a))
⊢ a < o
have rw : a.repr < succ a.repr
Tactic: rw [lt_def, h.1]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
x : Option ONote ⊕ (ℕ → ONote)
e : o.fundamentalSequence = x
⊢ o.fastGrowing =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) x, ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun (i : ℕ) ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun (i : ℕ) ↦ (f i).fastGrowing i
have subst : o.fastGrowing =
  match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence, sorry with
  | Sum.inl none, x => Nat.succ
  | Sum.inl (some a), x => fun (i : ℕ) ↦ a.fastGrowing^[i] i
  | Sum.inr f, x => fun (i : ℕ) ↦ (f i).fastGrowing i
Tactic: subst x
Cleared hypotheses: x, e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
⊢ o.fastGrowing =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
      ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun (i : ℕ) ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun (i : ℕ) ↦ (f i).fastGrowing i
have rw : Eq (α := ℕ → ℕ)
  (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
      sorry with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), h =>
      have this := sorry;
      fun (i : ℕ) ↦ a.fastGrowing^[i] i
    | Sum.inr f, h => fun (i : ℕ) ↦
      have this := sorry;
      (f i).fastGrowing i :
    ℕ → ℕ)
  (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
      sorry with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun (i : ℕ) ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun (i : ℕ) ↦ (f i).fastGrowing i :
    ℕ → ℕ)
Tactic: rw [fastGrowing]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
h : o.fundamentalSequence = Sum.inl none
⊢ o.fastGrowing = Nat.succ
have rw : (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inl none, sorry with
  | Sum.inl none, x => Nat.succ
  | Sum.inl (some a), x => fun (i : ℕ) ↦ a.fastGrowing^[i] i
  | Sum.inr f, x => fun (i : ℕ) ↦ (f i).fastGrowing i) =
  Nat.succ
Tactic: rw [fastGrowing_def h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o a : ONote
h : o.fundamentalSequence = Sum.inl (some a)
⊢ o.fastGrowing = fun (i : ℕ) ↦ a.fastGrowing^[i] i
have rw : Eq (α := ℕ → ℕ)
  (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inl (some a), sorry with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun (i : ℕ) ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun (i : ℕ) ↦ (f i).fastGrowing i :
    ℕ → ℕ)
  fun (i : ℕ) ↦ a.fastGrowing^[i] i
Tactic: rw [fastGrowing_def h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
f : ℕ → ONote
h : o.fundamentalSequence = Sum.inr f
⊢ o.fastGrowing = fun (i : ℕ) ↦ (f i).fastGrowing i
have rw : Eq (α := ℕ → ℕ)
  (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inr f, sorry with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun (i : ℕ) ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun (i : ℕ) ↦ (f i).fastGrowing i :
    ℕ → ℕ)
  fun (i : ℕ) ↦ (f i).fastGrowing i
Tactic: rw [fastGrowing_def h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
⊢ fastGrowing 1 = fun (n : ℕ) ↦ 2 * n
have rw : Eq (α := ℕ → ℕ) (fun (i : ℕ) ↦ (fastGrowing 0)^[i] i) fun (n : ℕ) ↦ 2 * n
Tactic: rw [@fastGrowing_succ 1 0 rfl]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
⊢ Eq (α := ℕ → ℕ) (fun (i : ℕ) ↦ (fastGrowing 0)^[i] i) fun (n : ℕ) ↦ 2 * n
have h : ∀ (i : ℕ), (fastGrowing 0)^[i] i = 2 * i
Tactic: funext i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
i : ℕ
⊢ (fastGrowing 0)^[i] i = 2 * i
have h : Nat.succ^[i] i = i + i
Tactic: rw [two_mul, fastGrowing_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
⊢ fastGrowing 2 = fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n * n
have rw : Eq (α := ℕ → ℕ) (fun (i : ℕ) ↦ (fastGrowing 1)^[i] i) fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n * n
Tactic: rw [@fastGrowing_succ 2 1 rfl]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (cmp (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)).Compares
    (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
have dsimp : (a.cmp b).Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
Tactic: dsimp [cmp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (a.cmp b).Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
have this : (a.cmp b).Compares a b
Tactic: have := ONote.cmp_compares a b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
⊢ (a.cmp b).Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
have lt : ∀ (h : a.cmp b = Ordering.lt),
  Ordering.lt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
Tactic: cases h : ONote.cmp a b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
lt :
  ∀ (h : a.cmp b = Ordering.lt),
    Ordering.lt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
⊢ (a.cmp b).Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
have eq : ∀ (h : a.cmp b = Ordering.eq),
  Ordering.eq.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
Tactic: cases h : ONote.cmp a b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
lt :
  ∀ (h : a.cmp b = Ordering.lt),
    Ordering.lt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
eq :
  ∀ (h : a.cmp b = Ordering.eq),
    Ordering.eq.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
⊢ (a.cmp b).Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
have gt : ∀ (h : a.cmp b = Ordering.gt),
  Ordering.gt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
Tactic: cases h : ONote.cmp a b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.lt
⊢ Ordering.lt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
have this₁ : Ordering.lt.Compares a b
Tactic: simp only [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.eq
⊢ Ordering.eq.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
have this₁ : Ordering.eq.Compares a b
Tactic: simp only [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.gt
⊢ Ordering.gt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)
have this₁ : Ordering.gt.Compares a b
Tactic: simp only [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
C : NONote → Sort u_1
o : NONote
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
⊢ C o
have obtain : (o : ONote) → (h : o.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) o h)
Tactic: obtain ⟨o, h⟩ := o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
C : NONote → Sort u_1
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
o : ONote
h : o.NF
⊢ C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) o h)
have zero : (h : ONote.zero.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) ONote.zero h)
Tactic: induction o with
  | zero => exact H0
  | oadd e n a IHe IHa => exact H1 ⟨e, h.fst⟩ n ⟨a, h.snd⟩ h.snd' (IHe _) (IHa _)
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
C : NONote → Sort u_1
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
o : ONote
h : o.NF
zero : (h : ONote.zero.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) ONote.zero h)
⊢ C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) o h)
have oadd : (e : ONote) →
  (n : ℕ+) →
    (a : ONote) →
      (IHe : (h : e.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) e h)) →
        (IHa : (h : a.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a h)) →
          (h : (e.oadd n a).NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) (e.oadd n a) h)
Tactic: induction o with
  | zero => exact H0
  | oadd e n a IHe IHa => exact H1 ⟨e, h.fst⟩ n ⟨a, h.snd⟩ h.snd' (IHe _) (IHa _)
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o ↔ IsPrincipal op o
have mp : IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o → IsPrincipal op o
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
mp : IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o → IsPrincipal op o
⊢ IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o ↔ IsPrincipal op o
have mpr : IsPrincipal op o → IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
⊢ IsPrincipal op o ↔ ∀ a < o, op a a < o
have mpr : (∀ a < o, op a a < o) → IsPrincipal op o
Tactic: use fun h a ha => h ha ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
⊢ op a b < o
have mpr : ∀ (hab : a ≤ b), op a b < o
Tactic: obtain hab | hba := le_or_gt a b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
mpr : ∀ (hab : a ≤ b), op a b < o
⊢ op a b < o
have mpr₁ : ∀ (hba : b < a), op a b < o
Tactic: obtain hab | hba := le_or_gt a b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
⊢ (op a)^[0] a < o
have zero : id a < o
Tactic: rwa [Function.iterate_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a)^[n + 1] a < o
have succ : (op a ∘ (op a)^[n]) a < o
Tactic: rw [Function.iterate_succ']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
⊢ (op a)^[n] a < o
have zero : (op a)^[0] a < o
Tactic: induction n with
  | zero => rwa [Function.iterate_zero]
  | succ n hn =>
    rw [Function.iterate_succ']
    exact ho hao hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
zero : (op a)^[0] a < o
⊢ (op a)^[n] a < o
have succ : ∀ (n : ℕ) (hn : (op a)^[n] a < o), (op a)^[n + 1] a < o
Tactic: induction n with
  | zero => rwa [Function.iterate_zero]
  | succ n hn =>
    rw [Function.iterate_succ']
    exact ho hao hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ op a o = o
have apply : op a o ≤ o
Tactic: apply H.strictMono.le_apply.antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ op a o ≤ o
have rw : ∀ (i : (↑(Set.Iio o) : Type (u + 1))), op a (↑i : Ordinal.{u}) ≤ o
Tactic: rw [H.apply_of_isSuccLimit ho', Ordinal.iSup_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
⊢ IsPrincipal op (sSup s)
have this : IsPrincipal op (sSup ∅)
Tactic: have : IsPrincipal op (sSup ∅) := by simp
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
⊢ IsPrincipal op (sSup s)
have pos : ∀ (hs : BddAbove s), IsPrincipal op (sSup s)
Tactic: by_cases hs : BddAbove s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
pos : ∀ (hs : BddAbove s), IsPrincipal op (sSup s)
⊢ IsPrincipal op (sSup s)
have neg : ∀ (hs : ¬BddAbove s), IsPrincipal op (sSup s)
Tactic: by_cases hs : BddAbove s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
⊢ IsPrincipal op (sSup s)
have pos : ∀ (H : ∀ (x : Ordinal.{u_1}), Membership.mem (γ := Set Ordinal.{u_1}) ∅ x → IsPrincipal op x)
  (hs : BddAbove.{u_1 + 1} (α := Ordinal.{u_1}) ∅), IsPrincipal op (sSup ∅)
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
Cleared hypotheses: s, H, hs
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
pos :
  ∀ (H : ∀ (x : Ordinal.{u_1}), Membership.mem (γ := Set Ordinal.{u_1}) ∅ x → IsPrincipal op x)
    (hs : BddAbove.{u_1 + 1} (α := Ordinal.{u_1}) ∅), IsPrincipal op (sSup ∅)
⊢ IsPrincipal op (sSup s)
have pos₁ : ∀ (hs' : s.Nonempty), IsPrincipal op (sSup s)
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
⊢ IsPrincipal op (sSup s)
have pos : ∀ ⦃a b : Ordinal.{u_1}⦄, ∀ x ∈ s, a < x → ∀ x ∈ s, b < x → ∃ b_1 ∈ s, op a b < b_1
Tactic: simp only [IsPrincipal, lt_csSup_iff hs hs', forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
b : Ordinal.{u_1}
hbs : b ∈ s
hb : y < b
⊢ ∃ b ∈ s, op x y < b
have h : max a b ∈ s
Tactic: have h : max a b ∈ s := max_rec' _ has hbs