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
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

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

Premises used: Ordinal.isSuccLimit_opow, _private.0.ONote.exists_lt_add, And.intro, Ordinal.isSuccLimit_add, _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
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
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)
⊢ 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

Tactic:
refine
        ⟨isSuccLimit_add _ (isSuccLimit_opow one_lt_omega0 h1), fun i => ?_,
          exists_lt_add (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
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 < 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
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 < 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
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
⊢ 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
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)

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

Premises used: ONote.NF.oadd, ONote.NF.oadd_zero, ONote.NF.below_of_lt', Nat.succPNat, And.intro, ONote.NF.fst, 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
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
oadd : ∀ (H : (a.oadd (m' + 1).succPNat 0).NF), ((f i).oadd 1 0).repr < ω ^ a.repr
⊢ (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 ⟨h4, h5, fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@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
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
oadd₇ oadd₈ oadd₉ oadd₁₀ : (f i).repr < a.repr
⊢ ((f i).oadd 1 0).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]

Premises used: PNat.one_coe, ONote.repr, Ordinal.opow_lt_opow_iff_right, mul_one, add_zero, Nat.cast_one, ONote.zero_def, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
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)

Tactic:
⟨?_, fun H ↦ H.fst.oadd _ (NF.below_of_lt' ?_ (ihb.2 H.snd))⟩

Premises used: ONote.NF.snd, ONote.NF.oadd, ONote.NF.below_of_lt', And.right, And.intro, ONote.NF.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
oadd₁ : ∀ (H : (a.oadd m b).NF), b'.repr < ω ^ a.repr
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr ∧ ((a.oadd m b).NF → (a.oadd m b').NF)

Tactic:
refine ⟨?_, fun H ↦ H.fst.oadd _ (NF.below_of_lt' ?_ (ihb.2 H.snd))⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
oadd₅ oadd₆ :
  ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b'.repr + 1 = ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b'.repr + 1
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr

Tactic:
rw [repr, ihb.1, succ_eq_add_one, succ_eq_add_one, ← add_assoc, repr]

Premises used: Order.succ_eq_add_one, add_assoc, And.left, ONote.repr
-- Module: Mathlib.SetTheory.Ordinal.Notation
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

Tactic:
have := H.snd'.repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
⊢ succ b'.repr < ω ^ a.repr

Tactic:
rw [ihb.1] at this

Premises used: And.left
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 : succ b'.repr < ω ^ a.repr
⊢ b'.repr < ω ^ a.repr

Tactic:
(lt_succ _).trans this

Premises used: Order.lt_succ, LT.lt.trans
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 : succ b'.repr < ω ^ a.repr
⊢ b'.repr < ω ^ a.repr

Tactic:
exact (lt_succ _).trans this

Premises used: Order.lt_succ, LT.lt.trans
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 b.repr

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

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

Tactic:
rcases ihb with ⟨h1, h2, h3⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
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)
h3 : ∀ a < b.repr, ∃ (i : ℕ), a < (f i).repr
⊢ IsSuccLimit (ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + 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.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b.repr,
        ∃ (i : ℕ), a_1 < ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + (f i).repr

Tactic:
⟨isSuccLimit_add _ h1, fun i =>
        ⟨oadd_lt_oadd_3 (h2 i).1, oadd_lt_oadd_3 (h2 i).2.1, fun H =>
          H.fst.oadd _ (NF.below_of_lt' (lt_trans (h2 i).2.1 H.snd'.repr_lt) ((h2 i).2.2 H.snd))⟩,
        exists_lt_add h3⟩

Premises used: lt_trans, ONote.oadd_lt_oadd_3, ONote.NF.snd, _private.0.ONote.exists_lt_add, ONote.NF.oadd, ONote.NF.below_of_lt', And.right, And.left, And.intro, ONote.NF.fst, Ordinal.isSuccLimit_add, ONote.NF.snd', ONote.NFBelow.repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
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)
h3 : ∀ a < b.repr, ∃ (i : ℕ), a < (f i).repr
⊢ IsSuccLimit (ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + 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.repr * (↑(↑m : ℕ) : Ordinal.{0}) + b.repr,
        ∃ (i : ℕ), a_1 < ω ^ a.repr * (↑(↑m : ℕ) : Ordinal.{0}) + (f i).repr

Tactic:
exact
      ⟨isSuccLimit_add _ h1, fun i =>
        ⟨oadd_lt_oadd_3 (h2 i).1, oadd_lt_oadd_3 (h2 i).2.1, fun H =>
          H.fst.oadd _ (NF.below_of_lt' (lt_trans (h2 i).2.1 H.snd'.repr_lt) ((h2 i).2.2 H.snd))⟩,
        exists_lt_add h3⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
o : ONote := x
a : ONote
h : o.FundamentalSequenceProp (Sum.inl (some a))
rw : a.repr < succ a.repr
⊢ a < o

Tactic:
rw [lt_def, h.1]

Premises used: ONote.lt_def, And.left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
o : ONote := x
a : ONote
h : o.FundamentalSequenceProp (Sum.inl (some a))
⊢ a.repr < succ a.repr

Tactic:
apply lt_succ

Premises used: Order.lt_succ
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
x : Option ONote ⊕ (ℕ → ONote)
e : o.fundamentalSequence = x
subst :
  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
⊢ 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

Tactic:
subst x
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
rw rw₁ :
  Eq (α := ℕ → ℕ)
    (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
        ⋯ with
      | Sum.inl none, x => Nat.succ
      | Sum.inl (some a), h =>
        have this := ⋯;
        fun (i : ℕ) ↦ a.fastGrowing^[i] i
      | Sum.inr f, h => fun (i : ℕ) ↦
        have this := ⋯;
        (f i).fastGrowing i :
      ℕ → ℕ)
    (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 :
      ℕ → ℕ)
⊢ 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

Tactic:
rw [fastGrowing]

Premises used: ONote.fastGrowing
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
h : o.fundamentalSequence = Sum.inl none
rw rw₁ :
  (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inl none, ⋯ 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
⊢ o.fastGrowing = Nat.succ

Tactic:
rw [fastGrowing_def h]

Premises used: ONote.fastGrowing_def
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o a : ONote
h : o.fundamentalSequence = Sum.inl (some a)
rw rw₁ :
  Eq (α := ℕ → ℕ)
    (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inl (some a), ⋯ 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
⊢ o.fastGrowing = fun (i : ℕ) ↦ a.fastGrowing^[i] i

Tactic:
rw [fastGrowing_def h]

Premises used: ONote.fastGrowing_def
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
f : ℕ → ONote
h : o.fundamentalSequence = Sum.inr f
rw rw₁ :
  Eq (α := ℕ → ℕ)
    (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inr f, ⋯ 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
⊢ o.fastGrowing = fun (i : ℕ) ↦ (f i).fastGrowing i

Tactic:
rw [fastGrowing_def h]

Premises used: ONote.fastGrowing_def
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ fastGrowing 0 = Nat.succ

Tactic:
fastGrowing_zero' _ rfl

Premises used: ONote.fastGrowing_zero', rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
rw : Eq (α := ℕ → ℕ) (fun (i : ℕ) ↦ (fastGrowing 0)^[i] i) fun (n : ℕ) ↦ 2 * n
⊢ fastGrowing 1 = fun (n : ℕ) ↦ 2 * n

Tactic:
rw [@fastGrowing_succ 1 0 rfl]

Premises used: ONote.fastGrowing_succ, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : ∀ (i : ℕ), (fastGrowing 0)^[i] i = 2 * i
⊢ Eq (α := ℕ → ℕ) (fun (i : ℕ) ↦ (fastGrowing 0)^[i] i) fun (n : ℕ) ↦ 2 * n

Tactic:
funext i
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
i : ℕ
h : Nat.succ^[i] i = i + i
⊢ (fastGrowing 0)^[i] i = 2 * i

Tactic:
rw [two_mul, fastGrowing_zero]

Premises used: two_mul, ONote.fastGrowing_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
i : ℕ
⊢ Nat.succ^[i] i = i + i

Tactic:
Nat.succ_iterate _ _

Premises used: Nat.succ_iterate
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
i : ℕ
⊢ Nat.succ^[i] i = i + i

Tactic:
exact Nat.succ_iterate _ _

Premises used: Nat.succ_iterate
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
rw : Eq (α := ℕ → ℕ) (fun (i : ℕ) ↦ (fastGrowing 1)^[i] i) fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n * n
⊢ fastGrowing 2 = fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n * n

Tactic:
rw [@fastGrowing_succ 2 1 rfl]

Premises used: ONote.fastGrowing_succ, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ Eq (α := ℕ → ℕ) (fun (i : ℕ) ↦ (fastGrowing 1)^[i] i) fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n * n

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ fastGrowingε₀ 0 = 1

Tactic:
simp [fastGrowingε₀]

Premises used: ONote.fastGrowingε₀
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ fastGrowingε₀ 1 = 2

Tactic:
simp [fastGrowingε₀, show oadd 0 1 0 = 1 from rfl]

Premises used: ONote.fastGrowingε₀, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ fastGrowingε₀ 2 = 2048

Tactic:
norm_num [fastGrowingε₀, show oadd 0 1 0 = 1 from rfl, @fastGrowing_limit (oadd 1 1 0) _ rfl,
    show oadd 0 (2 : Nat).succPNat 0 = 3 from rfl, @fastGrowing_succ 3 2 rfl]

Premises used: ONote.fastGrowing_limit, ONote.oadd, ONote.fastGrowing_succ, ONote.fastGrowingε₀, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : NONote
⊢ (↑o : ONote).NF

Tactic:
o.2

Premises used: Subtype.property
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ WellFounded fun (x1 x2 : NONote) ↦ x1 < x2

Tactic:
InvImage.wf repr Ordinal.lt_wf

Premises used: InvImage, NONote.repr, Ordinal.lt_wf, InvImage.wf
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ WellFoundedLT NONote

Tactic:
⟨lt_wf⟩

Premises used: IsWellFounded.mk, NONote.lt_wf
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
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)
⊢ (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)

Tactic:
dsimp [cmp]

Premises used: NONote.cmp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (a.cmp b).Compares a b

Tactic:
have := ONote.cmp_compares a b
-- Module: Mathlib.SetTheory.Ordinal.Notation
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)
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)
⊢ (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:
cases h : ONote.cmp a b

Premises used: ONote.cmp
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 a b

Tactic:
simp only [h] at this
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 a b

Tactic:
simp only [h] at this
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 a b

Tactic:
simp only [h] at this
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.lt
this : Ordering.lt.Compares a b
⊢ Ordering.lt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)

Tactic:
this

Premises used: NONote.repr, Ordering.Compares
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.lt
this : Ordering.lt.Compares a b
⊢ Ordering.lt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)

Tactic:
exact this
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.lt
this : Ordering.lt.Compares a b
⊢ Ordering.lt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)

Tactic:
try exact this
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)

Tactic:
this
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.gt
this : Ordering.gt.Compares a b
⊢ Ordering.gt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)

Tactic:
this

Premises used: NONote.repr, Ordering.Compares
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.gt
this : Ordering.gt.Compares a b
⊢ Ordering.gt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)

Tactic:
exact this
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.gt
this : Ordering.gt.Compares a b
⊢ Ordering.gt.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)

Tactic:
try exact this
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)

Tactic:
Subtype.mk_eq_mk.2 this

Premises used: Iff.mpr, Ordering.Compares, Subtype.mk_eq_mk, NONote