awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
oadd :
  ∀
    (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.oadd m 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 b ∧
              ((a.oadd m b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr
⊢ IsSuccLimit (a.oadd m 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 b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- 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
⊢ m.natPred + 1 = (↑m : ℕ)

Tactic:
have := PNat.natPred_add_one m
-- 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
this : m.natPred + 1 = (↑m : ℕ)
⊢ HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)

Tactic:
rw [e'] at this
-- 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
this : HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)
⊢ m = 1

Tactic:
PNat.coe_inj.1 this.symm

Premises used: Iff.mp, Eq.symm, PNat.coe_inj
-- 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
this : HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)
⊢ m = 1

Tactic:
exact PNat.coe_inj.1 this.symm

Premises used: Iff.mp, PNat.coe_inj
-- 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 : (a.oadd 1 b).repr = succ zero.repr ∧ ((a.oadd 1 b).NF → zero.NF)
⊢ (a.oadd m b).repr = succ zero.repr ∧ ((a.oadd m b).NF → zero.NF)

Tactic:
rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]
-- 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 : (a.oadd 1 b).repr = succ zero.repr ∧ ((a.oadd 1 b).NF → zero.NF)
⊢ (a.oadd m b).repr = succ zero.repr ∧ ((a.oadd m b).NF → zero.NF)

Tactic:
try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]
-- 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
this : m' + 1 + 1 = (↑m : ℕ)
⊢ m = 1

Tactic:
PNat.coe_inj

Premises used: PNat.coe_inj
-- 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
⊢ m.natPred + 1 = (↑m : ℕ)

Tactic:
have := PNat.natPred_add_one m
-- 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 : m.natPred + 1 = (↑m : ℕ)
⊢ HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)

Tactic:
rw [e'] at this
-- 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 : HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)
⊢ m = 1

Tactic:
PNat.coe_inj.1 this.symm

Premises used: Iff.mp, Eq.symm, PNat.coe_inj
-- 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 : HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)
⊢ m = 1

Tactic:
exact PNat.coe_inj.1 this.symm

Premises used: Iff.mp, PNat.coe_inj
-- 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
oadd :
  IsSuccLimit (a.oadd 1 b).repr ∧
    (∀ (i : ℕ),
        a'.oadd i.succPNat zero < a'.oadd (i + 1).succPNat zero ∧
          a'.oadd i.succPNat zero < a.oadd 1 b ∧ ((a.oadd 1 b).NF → (a'.oadd i.succPNat zero).NF)) ∧
      ∀ a_1 < (a.oadd 1 b).repr, ∃ (i : ℕ), a_1 < (a'.oadd i.succPNat zero).repr
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a'.oadd i.succPNat zero < a'.oadd (i + 1).succPNat zero ∧
          a'.oadd i.succPNat zero < a.oadd m b ∧ ((a.oadd m b).NF → (a'.oadd i.succPNat zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a'.oadd i.succPNat zero).repr

Tactic:
rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]
-- 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
oadd :
  IsSuccLimit (a.oadd 1 b).repr ∧
    (∀ (i : ℕ),
        a'.oadd i.succPNat zero < a'.oadd (i + 1).succPNat zero ∧
          a'.oadd i.succPNat zero < a.oadd 1 b ∧ ((a.oadd 1 b).NF → (a'.oadd i.succPNat zero).NF)) ∧
      ∀ a_1 < (a.oadd 1 b).repr, ∃ (i : ℕ), a_1 < (a'.oadd i.succPNat zero).repr
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a'.oadd i.succPNat zero < a'.oadd (i + 1).succPNat zero ∧
          a'.oadd i.succPNat zero < a.oadd m b ∧ ((a.oadd m b).NF → (a'.oadd i.succPNat zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a'.oadd i.succPNat zero).repr

Tactic:
try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]
-- 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 : m' + 1 + 1 = (↑m : ℕ)
⊢ m = 1

Tactic:
PNat.coe_inj

Premises used: PNat.coe_inj
-- 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
⊢ m.natPred + 1 = (↑m : ℕ)

Tactic:
have := PNat.natPred_add_one m
-- 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
this : m.natPred + 1 = (↑m : ℕ)
⊢ HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)

Tactic:
rw [e'] at this
-- 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
this : HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)
⊢ m = 1

Tactic:
PNat.coe_inj.1 this.symm

Premises used: Iff.mp, Eq.symm, PNat.coe_inj
-- 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
this : HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)
⊢ m = 1

Tactic:
exact PNat.coe_inj.1 this.symm

Premises used: Iff.mp, PNat.coe_inj
-- 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.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
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        (f i).oadd 1 zero < (f (i + 1)).oadd 1 zero ∧
          (f i).oadd 1 zero < a.oadd m b ∧ ((a.oadd m b).NF → ((f i).oadd 1 zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < ((f i).oadd 1 zero).repr

Tactic:
rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]
-- 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.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
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        (f i).oadd 1 zero < (f (i + 1)).oadd 1 zero ∧
          (f i).oadd 1 zero < a.oadd m b ∧ ((a.oadd m b).NF → ((f i).oadd 1 zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < ((f i).oadd 1 zero).repr

Tactic:
try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]
-- 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
this : m' + 1 + 1 = (↑m : ℕ)
⊢ m = 1

Tactic:
PNat.coe_inj

Premises used: PNat.coe_inj
-- 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
rw : m = m.natPred.succPNat
rw₁ : (↑m : ℕ) = (↑m.natPred.succPNat : ℕ)
rw₂ : (↑m : ℕ) = m.natPred.succ
rw₃ : (↑m : ℕ) = m.natPred + 1
rw₄ rw₅ : (↑m : ℕ) = (↑m : ℕ)
⊢ m = (m' + 1).succPNat

Tactic:
rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]

Premises used: Nat.succPNat_coe, PNat.natPred_add_one, Nat.add_one, PNat.coe_inj
-- 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
oadd :
  (a.oadd (m' + 1).succPNat b).repr = succ (zero.oadd m'.succPNat zero).repr ∧
    ((a.oadd (m' + 1).succPNat b).NF → (zero.oadd m'.succPNat zero).NF)
⊢ (a.oadd m b).repr = succ (zero.oadd m'.succPNat zero).repr ∧ ((a.oadd m b).NF → (zero.oadd m'.succPNat zero).NF)

Tactic:
rw [show m = (m' + 1).succPNat by
              rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]]
-- 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
oadd :
  (a.oadd (m' + 1).succPNat b).repr = succ (zero.oadd m'.succPNat zero).repr ∧
    ((a.oadd (m' + 1).succPNat b).NF → (zero.oadd m'.succPNat zero).NF)
⊢ (a.oadd m b).repr = succ (zero.oadd m'.succPNat zero).repr ∧ ((a.oadd m b).NF → (zero.oadd m'.succPNat zero).NF)

Tactic:
try rw [show m = (m' + 1).succPNat by
              rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_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
rw : m = m.natPred.succPNat
rw₁ : (↑m : ℕ) = (↑m.natPred.succPNat : ℕ)
rw₂ : (↑m : ℕ) = m.natPred.succ
rw₃ : (↑m : ℕ) = m.natPred + 1
rw₄ rw₅ : (↑m : ℕ) = (↑m : ℕ)
⊢ m = (m' + 1).succPNat

Tactic:
rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]

Premises used: Nat.succPNat_coe, PNat.natPred_add_one, Nat.add_one, PNat.coe_inj
-- 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.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
⊢ IsSuccLimit (a.oadd m 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 b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr

Tactic:
rw [show m = (m' + 1).succPNat by
              rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_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
oadd :
  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
⊢ IsSuccLimit (a.oadd m 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 b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr

Tactic:
try rw [show m = (m' + 1).succPNat by
              rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]]
-- 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
rw : m = m.natPred.succPNat
rw₁ : (↑m : ℕ) = (↑m.natPred.succPNat : ℕ)
rw₂ : (↑m : ℕ) = m.natPred.succ
rw₃ : (↑m : ℕ) = m.natPred + 1
rw₄ rw₅ : (↑m : ℕ) = (↑m : ℕ)
⊢ m = (m' + 1).succPNat

Tactic:
rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]

Premises used: Nat.succPNat_coe, PNat.natPred_add_one, Nat.add_one, PNat.coe_inj
-- 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.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
⊢ IsSuccLimit (a.oadd m 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 b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr

Tactic:
rw [show m = (m' + 1).succPNat by
              rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]]
-- 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.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
⊢ IsSuccLimit (a.oadd m 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 b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr

Tactic:
try rw [show m = (m' + 1).succPNat by
              rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]]
-- 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) ∧ ((ONote.oadd 0 1 0).NF → NF 0)
⊢ (a.oadd 1 b).repr = succ zero.repr ∧ ((a.oadd 1 b).NF → zero.NF)

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
m' : ℕ
e' : m.natPred = m' + 1
oadd :
  HMul.hMul (α := Ordinal.{0}) 1 (↑m' : Ordinal.{0}) + 1 + 1 =
      succ (HMul.hMul (α := Ordinal.{0}) 1 (↑m' : Ordinal.{0}) + 1) ∧
    ((ONote.oadd 0 (m' + 1).succPNat 0).NF → (ONote.oadd 0 m'.succPNat 0).NF)
⊢ (a.oadd (m' + 1).succPNat b).repr = succ (zero.oadd m'.succPNat zero).repr ∧
    ((a.oadd (m' + 1).succPNat b).NF → (zero.oadd m'.succPNat zero).NF)

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
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
oadd :
  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
⊢ IsSuccLimit (a.oadd 1 b).repr ∧
    (∀ (i : ℕ),
        a'.oadd i.succPNat zero < a'.oadd (i + 1).succPNat zero ∧
          a'.oadd i.succPNat zero < a.oadd 1 b ∧ ((a.oadd 1 b).NF → (a'.oadd i.succPNat zero).NF)) ∧
      ∀ a_1 < (a.oadd 1 b).repr, ∃ (i : ℕ), a_1 < (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