awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
oadd :
  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)
⊢ IsSuccLimit (a.oadd (m' + 1).succPNat b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m'.succPNat (a'.oadd (i + 1).succPNat zero) ∧
          a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd (m' + 1).succPNat b ∧
            ((a.oadd (m' + 1).succPNat b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd (m' + 1).succPNat b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr

Tactic:
simp only [repr, iha, ihb, opow_lt_opow_iff_right one_lt_omega0, add_lt_add_iff_left,
        add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
        _root_.zero_add, zero_def]

Premises used: lt_add_iff_pos_right, Nat.cast_succ, ONote.lt_def, Nat.succPNat_coe, PNat.one_coe, zero_add, ONote.repr, Ordinal.opow_zero, Ordinal.opow_lt_opow_iff_right, Nat.cast_zero, Ordinal.opow_succ, mul_one, add_zero, mul_add_one, ONote.zero_def, Ordinal.one_lt_omega0, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
oadd :
  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
⊢ IsSuccLimit (a.oadd 1 b).repr ∧
    (∀ (i : ℕ),
        (f i).oadd 1 zero < (f (i + 1)).oadd 1 zero ∧
          (f i).oadd 1 zero < a.oadd 1 b ∧ ((a.oadd 1 b).NF → ((f i).oadd 1 zero).NF)) ∧
      ∀ a_1 < (a.oadd 1 b).repr, ∃ (i : ℕ), a_1 < ((f i).oadd 1 zero).repr

Tactic:
simp only [repr, iha, ihb, opow_lt_opow_iff_right one_lt_omega0, add_lt_add_iff_left,
        add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
        _root_.zero_add, zero_def]

Premises used: lt_add_iff_pos_right, Nat.cast_succ, ONote.lt_def, Nat.succPNat_coe, PNat.one_coe, zero_add, ONote.repr, Ordinal.opow_zero, Ordinal.opow_lt_opow_iff_right, Nat.cast_zero, Ordinal.opow_succ, mul_one, add_zero, mul_add_one, ONote.zero_def, Ordinal.one_lt_omega0, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
oadd :
  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
⊢ IsSuccLimit (a.oadd (m' + 1).succPNat b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m'.succPNat ((f (i + 1)).oadd 1 zero) ∧
          a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd (m' + 1).succPNat b ∧
            ((a.oadd (m' + 1).succPNat b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd (m' + 1).succPNat b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr

Tactic:
simp only [repr, iha, ihb, opow_lt_opow_iff_right one_lt_omega0, add_lt_add_iff_left,
        add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
        _root_.zero_add, zero_def]

Premises used: lt_add_iff_pos_right, Nat.cast_succ, ONote.lt_def, Nat.succPNat_coe, PNat.one_coe, zero_add, ONote.repr, Ordinal.opow_zero, Ordinal.opow_lt_opow_iff_right, Nat.cast_zero, Ordinal.opow_succ, mul_one, add_zero, mul_add_one, ONote.zero_def, Ordinal.one_lt_omega0, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
oadd : Eq (α := Ordinal.{0}) 1 (succ 0)
oadd₁ : (ONote.oadd 0 1 0).NF → NF 0
⊢ Eq (α := Ordinal.{0}) 1 (succ 0) ∧ ((ONote.oadd 0 1 0).NF → NF 0)

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ Eq (α := Ordinal.{0}) 1 (succ 0)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ (oadd 0 1 0).NF → NF 0

Tactic:
decide
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ HMul.hMul (α := Ordinal.{0}) 1 (↑m' : Ordinal.{0}) + 1 + 1 =
      succ (HMul.hMul (α := Ordinal.{0}) 1 (↑m' : Ordinal.{0}) + 1) ∧
    ((oadd 0 (m' + 1).succPNat 0).NF → (oadd 0 m'.succPNat 0).NF)

Tactic:
⟨rfl, inferInstance⟩

Premises used: inferInstance, And.intro, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ HMul.hMul (α := Ordinal.{0}) 1 (↑m' : Ordinal.{0}) + 1 + 1 =
      succ (HMul.hMul (α := Ordinal.{0}) 1 (↑m' : Ordinal.{0}) + 1) ∧
    ((oadd 0 (m' + 1).succPNat 0).NF → (oadd 0 m'.succPNat 0).NF)

Tactic:
exact ⟨rfl, inferInstance⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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')
e' : m.natPred = 0
⊢ 0 < ω ^ a'.repr

Tactic:
have := opow_pos (repr a') omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
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')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
⊢ IsSuccLimit (ω ^ a'.repr * ω) ∧
    (∀ (i : ℕ),
        0 < ω ^ a'.repr ∧
          ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω ∧
            ((a.oadd 1 0).NF → (a'.oadd i.succPNat 0).NF)) ∧
      ∀ a < ω ^ a'.repr * ω, ∃ (i : ℕ), a < ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr

Tactic:
⟨isSuccLimit_mul_right this isSuccLimit_omega0, fun i =>
          ⟨this, ?_, fun H => @NF.oadd_zero _ _ (iha.2 H.fst)⟩, exists_lt_mul_omega0'⟩

Premises used: Ordinal.isSuccLimit_omega0, ONote.NF.oadd_zero, Nat.succPNat, And.intro, Ordinal.isSuccLimit_mul_right, _private.0.ONote.exists_lt_mul_omega0'
-- Module: Mathlib.SetTheory.Ordinal.Notation
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')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
oadd : ∀ (i : ℕ), ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω
⊢ IsSuccLimit (ω ^ a'.repr * ω) ∧
    (∀ (i : ℕ),
        0 < ω ^ a'.repr ∧
          ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω ∧
            ((a.oadd 1 0).NF → (a'.oadd i.succPNat 0).NF)) ∧
      ∀ a < ω ^ a'.repr * ω, ∃ (i : ℕ), a < ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr

Tactic:
refine
        ⟨isSuccLimit_mul_right this isSuccLimit_omega0, fun i =>
          ⟨this, ?_, fun H => @NF.oadd_zero _ _ (iha.2 H.fst)⟩, exists_lt_mul_omega0'⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
oadd : ω ^ a'.repr * (↑(i + 1) : Ordinal.{0}) < ω ^ a'.repr * ω
⊢ ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω

Tactic:
rw [← mul_add_one, ← Nat.cast_add_one]

Premises used: mul_add_one, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Ordinal.Notation
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')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
oadd : (↑(i + 1) : Ordinal.{0}) < ω
⊢ ω ^ a'.repr * (↑(i + 1) : Ordinal.{0}) < ω ^ a'.repr * ω

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Notation
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')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
⊢ (↑(i + 1) : Ordinal.{0}) < ω

Tactic:
apply natCast_lt_omega0

Premises used: Ordinal.natCast_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
⊢ 0 < ω ^ a'.repr

Tactic:
have := opow_pos (repr a') omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
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)

Tactic:
⟨isSuccLimit_add _ (isSuccLimit_mul_right this isSuccLimit_omega0), fun i => ⟨this, ?_, ?_⟩,
          exists_lt_add exists_lt_mul_omega0'⟩

Premises used: Ordinal.isSuccLimit_omega0, _private.0.ONote.exists_lt_add, And.intro, Ordinal.isSuccLimit_add, Ordinal.isSuccLimit_mul_right, _private.0.ONote.exists_lt_mul_omega0'
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 * ω
oadd₁ : ∀ (i : ℕ), (a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF
⊢ 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)

Tactic:
refine
        ⟨isSuccLimit_add _ (isSuccLimit_mul_right this isSuccLimit_omega0), fun i => ⟨this, ?_, ?_⟩,
          exists_lt_add exists_lt_mul_omega0'⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 : ℕ
oadd : ω ^ a'.repr * (↑(i + 1) : Ordinal.{0}) < ω ^ a'.repr * ω
⊢ ω ^ a'.repr * (↑i : Ordinal.{0}) + ω ^ a'.repr < ω ^ a'.repr * ω

Tactic:
rw [← mul_add_one, ← Nat.cast_add_one]

Premises used: mul_add_one, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 : ℕ
oadd : (↑(i + 1) : Ordinal.{0}) < ω
⊢ ω ^ a'.repr * (↑(i + 1) : Ordinal.{0}) < ω ^ a'.repr * ω

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 : ℕ
⊢ (↑(i + 1) : Ordinal.{0}) < ω

Tactic:
apply natCast_lt_omega0

Premises used: Ordinal.natCast_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
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

Tactic:
fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (iha.2 H.fst)))

Premises used: ONote.NF.oadd, ONote.NF.oadd_zero, ONote.NF.below_of_lt', Nat.succPNat, ONote.NF.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 : ℕ
oadd : ∀ (H : (a.oadd (m' + 1).succPNat 0).NF), (a'.oadd i.succPNat 0).repr < ω ^ a.repr
⊢ (a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF

Tactic:
refine fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (iha.2 H.fst)))
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
oadd : ω ^ a'.repr * (↑(↑i.succPNat : ℕ) : Ordinal.{0}) < ω ^ a'.repr * ω
⊢ (a'.oadd i.succPNat 0).repr < ω ^ a.repr

Tactic:
rw [repr, ← zero_def, repr, add_zero, iha.1, opow_succ]

Premises used: And.left, ONote.repr, Ordinal.opow_succ, add_zero, ONote.zero_def
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
oadd : (↑(↑i.succPNat : ℕ) : Ordinal.{0}) < ω
⊢ ω ^ a'.repr * (↑(↑i.succPNat : ℕ) : Ordinal.{0}) < ω ^ a'.repr * ω

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
⊢ (↑(↑i.succPNat : ℕ) : Ordinal.{0}) < ω

Tactic:
apply natCast_lt_omega0

Premises used: Ordinal.natCast_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
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

Tactic:
rcases iha with ⟨h1, h2, h3⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
⊢ ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)

Tactic:
rcases iha with ⟨h1, h2, h3⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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)
⊢ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr

Tactic:
rcases iha with ⟨h1, h2, h3⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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

Tactic:
⟨isSuccLimit_opow one_lt_omega0 h1, fun i => ?_,
        exists_lt_omega0_opow' one_lt_omega0 h1 h3⟩

Premises used: Ordinal.isSuccLimit_opow, And.intro, _private.0.ONote.exists_lt_omega0_opow', Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
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)
⊢ 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

Tactic:
refine ⟨isSuccLimit_opow one_lt_omega0 h1, fun i => ?_,
        exists_lt_omega0_opow' one_lt_omega0 h1 h3⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 < f (i + 1)

Tactic:
obtain ⟨h4, h5, h6⟩ := h2 i
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 < a

Tactic:
obtain ⟨h4, h5, h6⟩ := h2 i
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
⊢ a.NF → (f i).NF

Tactic:
obtain ⟨h4, h5, h6⟩ := h2 i
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
h6 : a.NF → (f i).NF
⊢ (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)

Tactic:
⟨h4, h5, fun H => @NF.oadd_zero _ _ (h6 H.fst)⟩

Premises used: ONote.NF.oadd_zero, And.intro, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
h6 : a.NF → (f i).NF
⊢ (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)

Tactic:
exact ⟨h4, h5, fun H => @NF.oadd_zero _ _ (h6 H.fst)⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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

Tactic:
rcases iha with ⟨h1, h2, h3⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
⊢ ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)

Tactic:
rcases iha with ⟨h1, h2, h3⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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)
⊢ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr

Tactic:
rcases iha with ⟨h1, h2, h3⟩