awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
⊢ IsSuccLimit (ω ^ a'.repr * ω * (↑m' : Ordinal.{0}) + ω ^ a'.repr * ω + ω ^ a'.repr * ω) ∧
    (∀ (i : ℕ),
        0 < ω ^ a'.repr ∧
          ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω ∧
            ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF)) ∧
      ∀ a < ω ^ a'.repr * ω * (↑m' : Ordinal.{0}) + ω ^ a'.repr * ω + ω ^ a'.repr * ω,
        ∃ (i : ℕ),
          a < ω ^ a'.repr * ω * (↑m' : Ordinal.{0}) + ω ^ a'.repr * ω + (ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr)
have oadd : ∀ (i : ℕ), ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω
Tactic: refine
        ⟨isSuccLimit_add _ (isSuccLimit_mul_right this isSuccLimit_omega0), fun i => ⟨this, ?_, ?_⟩,
          exists_lt_add exists_lt_mul_omega0'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
oadd : ∀ (i : ℕ), ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω
⊢ IsSuccLimit (ω ^ a'.repr * ω * (↑m' : Ordinal.{0}) + ω ^ a'.repr * ω + ω ^ a'.repr * ω) ∧
    (∀ (i : ℕ),
        0 < ω ^ a'.repr ∧
          ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω ∧
            ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF)) ∧
      ∀ a < ω ^ a'.repr * ω * (↑m' : Ordinal.{0}) + ω ^ a'.repr * ω + ω ^ a'.repr * ω,
        ∃ (i : ℕ),
          a < ω ^ a'.repr * ω * (↑m' : Ordinal.{0}) + ω ^ a'.repr * ω + (ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr)
have oadd₁ : ∀ (i : ℕ), (a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF
Tactic: refine
        ⟨isSuccLimit_add _ (isSuccLimit_mul_right this isSuccLimit_omega0), fun i => ⟨this, ?_, ?_⟩,
          exists_lt_add exists_lt_mul_omega0'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω
have oadd : ω ^ a'.repr * (↑(i + 1) : Ordinal.{0}) < ω ^ a'.repr * ω
Tactic: rw [← mul_add_one, ← Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * (↑(i + 1) : Ordinal.{0}) < ω ^ a'.repr * ω
have oadd : (↑(i + 1) : Ordinal.{0}) < ω
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ (a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF
have oadd : ∀ (H : (a.oadd (m' + 1).succPNat 0).NF), (a'.oadd i.succPNat 0).repr < ω ^ a.repr
Tactic: refine fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (iha.2 H.fst)))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ (a'.oadd i.succPNat 0).repr < ω ^ a.repr
have oadd : ω ^ a'.repr * (↑(↑i.succPNat : ℕ) : Ordinal.{0}) < ω ^ a'.repr * ω
Tactic: rw [repr, ← zero_def, repr, add_zero, iha.1, opow_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ a'.repr * (↑(↑i.succPNat : ℕ) : Ordinal.{0}) < ω ^ a'.repr * ω
have oadd : (↑(↑i.succPNat : ℕ) : Ordinal.{0}) < ω
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit (ω ^ a.repr) ∧
    (∀ (i : ℕ), (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)) ∧
      ∀ a_1 < ω ^ a.repr, ∃ (i : ℕ), a_1 < ω ^ (f i).repr
have h1 : IsSuccLimit a.repr
Tactic: rcases iha with ⟨h1, h2, h3⟩
Cleared hypotheses: iha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
⊢ IsSuccLimit (ω ^ a.repr) ∧
    (∀ (i : ℕ), (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)) ∧
      ∀ a_1 < ω ^ a.repr, ∃ (i : ℕ), a_1 < ω ^ (f i).repr
have h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
Tactic: rcases iha with ⟨h1, h2, h3⟩
Cleared hypotheses: iha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
⊢ IsSuccLimit (ω ^ a.repr) ∧
    (∀ (i : ℕ), (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)) ∧
      ∀ a_1 < ω ^ a.repr, ∃ (i : ℕ), a_1 < ω ^ (f i).repr
have h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
Tactic: rcases iha with ⟨h1, h2, h3⟩
Cleared hypotheses: iha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
⊢ IsSuccLimit (ω ^ a.repr) ∧
    (∀ (i : ℕ), (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)) ∧
      ∀ a_1 < ω ^ a.repr, ∃ (i : ℕ), a_1 < ω ^ (f i).repr
have oadd : ∀ (i : ℕ), (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)
Tactic: refine ⟨isSuccLimit_opow one_lt_omega0 h1, fun i => ?_,
        exists_lt_omega0_opow' one_lt_omega0 h1 h3⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
⊢ (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)
have h4 : f i < f (i + 1)
Tactic: obtain ⟨h4, h5, h6⟩ := h2 i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
⊢ (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)
have h5 : f i < a
Tactic: obtain ⟨h4, h5, h6⟩ := h2 i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
⊢ (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)
have h6 : a.NF → (f i).NF
Tactic: obtain ⟨h4, h5, h6⟩ := h2 i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ a.repr) ∧
    (∀ (i : ℕ),
        (f i).repr < (f (i + 1)).repr ∧
          (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ a.repr,
        ∃ (i : ℕ), a_1 < ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ (f i).repr
have h1 : IsSuccLimit a.repr
Tactic: rcases iha with ⟨h1, h2, h3⟩
Cleared hypotheses: iha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
⊢ IsSuccLimit (ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ a.repr) ∧
    (∀ (i : ℕ),
        (f i).repr < (f (i + 1)).repr ∧
          (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ a.repr,
        ∃ (i : ℕ), a_1 < ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ (f i).repr
have h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
Tactic: rcases iha with ⟨h1, h2, h3⟩
Cleared hypotheses: iha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
⊢ IsSuccLimit (ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ a.repr) ∧
    (∀ (i : ℕ),
        (f i).repr < (f (i + 1)).repr ∧
          (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ a.repr,
        ∃ (i : ℕ), a_1 < ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ (f i).repr
have h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
Tactic: rcases iha with ⟨h1, h2, h3⟩
Cleared hypotheses: iha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
⊢ IsSuccLimit (ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ a.repr) ∧
    (∀ (i : ℕ),
        (f i).repr < (f (i + 1)).repr ∧
          (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ a.repr,
        ∃ (i : ℕ), a_1 < ω ^ a.repr * (↑m' : Ordinal.{0}) + ω ^ a.repr + ω ^ (f i).repr
have oadd : ∀ (i : ℕ),
  (f i).repr < (f (i + 1)).repr ∧
    (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)
Tactic: refine
        ⟨isSuccLimit_add _ (isSuccLimit_opow one_lt_omega0 h1), fun i => ?_,
          exists_lt_add (exists_lt_omega0_opow' one_lt_omega0 h1 h3)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
⊢ (f i).repr < (f (i + 1)).repr ∧
    (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)
have h4 : f i < f (i + 1)
Tactic: obtain ⟨h4, h5, h6⟩ := h2 i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
⊢ (f i).repr < (f (i + 1)).repr ∧
    (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)
have h5 : f i < a
Tactic: obtain ⟨h4, h5, h6⟩ := h2 i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
⊢ (f i).repr < (f (i + 1)).repr ∧
    (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)
have h6 : a.NF → (f i).NF
Tactic: obtain ⟨h4, h5, h6⟩ := h2 i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
⊢ (f i).repr < (f (i + 1)).repr ∧
    (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)
have oadd : ∀ (H : (a.oadd (m' + 1).succPNat 0).NF), ((f i).oadd 1 0).repr < ω ^ a.repr
Tactic: refine ⟨h4, h5, fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (h6 H.fst)))⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ((f i).oadd 1 0).repr < ω ^ a.repr
have oadd : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + repr 0 < ω ^ a.repr
Tactic: rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
        opow_lt_opow_iff_right one_lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
oadd : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + repr 0 < ω ^ a.repr
⊢ ((f i).oadd 1 0).repr < ω ^ a.repr
have oadd₁ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + zero.repr < ω ^ a.repr
Tactic: rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
        opow_lt_opow_iff_right one_lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
oadd : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + repr 0 < ω ^ a.repr
oadd₁ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + zero.repr < ω ^ a.repr
⊢ ((f i).oadd 1 0).repr < ω ^ a.repr
have oadd₂ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + 0 < ω ^ a.repr
Tactic: rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
        opow_lt_opow_iff_right one_lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
oadd : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + repr 0 < ω ^ a.repr
oadd₁ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + zero.repr < ω ^ a.repr
oadd₂ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + 0 < ω ^ a.repr
⊢ ((f i).oadd 1 0).repr < ω ^ a.repr
have oadd₃ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) < ω ^ a.repr
Tactic: rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
        opow_lt_opow_iff_right one_lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
oadd : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + repr 0 < ω ^ a.repr
oadd₁ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + zero.repr < ω ^ a.repr
oadd₂ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + 0 < ω ^ a.repr
oadd₃ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) < ω ^ a.repr
⊢ ((f i).oadd 1 0).repr < ω ^ a.repr
have oadd₄ : ω ^ (f i).repr * (↑1 : Ordinal.{0}) < ω ^ a.repr
Tactic: rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
        opow_lt_opow_iff_right one_lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
oadd : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + repr 0 < ω ^ a.repr
oadd₁ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + zero.repr < ω ^ a.repr
oadd₂ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + 0 < ω ^ a.repr
oadd₃ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) < ω ^ a.repr
oadd₄ : ω ^ (f i).repr * (↑1 : Ordinal.{0}) < ω ^ a.repr
⊢ ((f i).oadd 1 0).repr < ω ^ a.repr
have oadd₅ : ω ^ (f i).repr * 1 < ω ^ a.repr
Tactic: rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
        opow_lt_opow_iff_right one_lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
oadd : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + repr 0 < ω ^ a.repr
oadd₁ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + zero.repr < ω ^ a.repr
oadd₂ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + 0 < ω ^ a.repr
oadd₃ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) < ω ^ a.repr
oadd₄ : ω ^ (f i).repr * (↑1 : Ordinal.{0}) < ω ^ a.repr
oadd₅ : ω ^ (f i).repr * 1 < ω ^ a.repr
⊢ ((f i).oadd 1 0).repr < ω ^ a.repr
have oadd₆ : ω ^ (f i).repr < ω ^ a.repr
Tactic: rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
        opow_lt_opow_iff_right one_lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
oadd : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + repr 0 < ω ^ a.repr
oadd₁ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + zero.repr < ω ^ a.repr
oadd₂ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) + 0 < ω ^ a.repr
oadd₃ : ω ^ (f i).repr * (↑(↑1 : ℕ) : Ordinal.{0}) < ω ^ a.repr
oadd₄ : ω ^ (f i).repr * (↑1 : Ordinal.{0}) < ω ^ a.repr
oadd₅ : ω ^ (f i).repr * 1 < ω ^ a.repr
oadd₆ : ω ^ (f i).repr < ω ^ a.repr
⊢ ((f i).oadd 1 0).repr < ω ^ a.repr
have oadd₇ : (f i).repr < a.repr
Tactic: rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
        opow_lt_opow_iff_right one_lt_omega0]
-- 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 ∧ ((a.oadd m b).NF → (a.oadd m b').NF)
have oadd : (a.oadd m b).repr = succ (a.oadd m b').repr
Tactic: refine ⟨?_, fun H ↦ H.fst.oadd _ (NF.below_of_lt' ?_ (ihb.2 H.snd))⟩
-- 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.oadd m b).repr = succ (a.oadd m b').repr
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr ∧ ((a.oadd m b).NF → (a.oadd m b').NF)
have oadd₁ : ∀ (H : (a.oadd m b).NF), b'.repr < ω ^ a.repr
Tactic: refine ⟨?_, fun H ↦ H.fst.oadd _ (NF.below_of_lt' ?_ (ihb.2 H.snd))⟩