awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
e : b.fundamentalSequence = Sum.inl none
⊢ match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) a.fundamentalSequence, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
have ihb₁ : b = 0
Tactic: rw [e, FundamentalSequenceProp] at ihb
Cleared hypotheses: ihb, e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
b' : ONote
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 ihb₁ : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
Tactic: rw [e, FundamentalSequenceProp] at ihb
Cleared hypotheses: ihb, e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m (f i)).repr
have 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
Tactic: rw [e, FundamentalSequenceProp] at ihb
Cleared hypotheses: ihb, e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e : b.fundamentalSequence = Sum.inl none
⊢ match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) a.fundamentalSequence, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
have oadd : ∀ (e : a.fundamentalSequence = Sum.inl none),
  match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) Sum.inl none, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
Tactic: rcases e : a.fundamentalSequence with (⟨_ | a'⟩ | f)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
⊢ match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) Sum.inl none, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
have oadd : ∀ (e' : m.natPred = 0),
  match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) Sum.inl none, 0 with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
Tactic: rcases e' : m.natPred with - | m'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
e : a.fundamentalSequence = Sum.inl (some a')
⊢ match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) Sum.inl (some a'), m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
have oadd : ∀ (e' : m.natPred = 0),
  match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) Sum.inl (some a'), 0 with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
Tactic: rcases e' : m.natPred with - | m'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) Sum.inr f, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
have oadd : ∀ (e' : m.natPred = 0),
  match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) Sum.inr f, 0 with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
Tactic: rcases e' : m.natPred with - | m'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ (a.oadd m b).repr = succ zero.repr ∧ ((a.oadd m b).NF → zero.NF)
have iha₁ : a = 0
Tactic: rw [e, FundamentalSequenceProp] at iha
Cleared hypotheses: iha, ihb, e_1, e, e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ (a.oadd m b).repr = succ (zero.oadd m'.succPNat zero).repr ∧ ((a.oadd m b).NF → (zero.oadd m'.succPNat zero).NF)
have oadd : ∀ (iha : a = 0) (ihb : b = 0) (e : b.fundamentalSequence = Sum.inl none) (e : a.fundamentalSequence = Sum.inl none)
  (m' : ℕ) (e' : m.natPred = m' + 1),
  (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 [e, FundamentalSequenceProp] at iha
Cleared hypotheses: iha, ihb, e_1, e, m', e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
⊢ 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
have iha₁ : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
Tactic: rw [e, FundamentalSequenceProp] at iha
Cleared hypotheses: iha, e, e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ 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
have oadd : ∀ (iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)) (e : a.fundamentalSequence = Sum.inl (some a')) (m' : ℕ)
  (e' : m.natPred = m' + 1),
  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 [e, FundamentalSequenceProp] at iha
Cleared hypotheses: iha, e, m', e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
e' : m.natPred = 0
⊢ 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
have 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
Tactic: rw [e, FundamentalSequenceProp] at iha
Cleared hypotheses: iha, e, e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ 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
have 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
Tactic: rw [e, FundamentalSequenceProp] at iha
Cleared hypotheses: iha, e, m', e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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 = 1
have this : m.natPred + 1 = (↑m : ℕ)
Tactic: have := PNat.natPred_add_one m
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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 : ℕ)
⊢ m = 1
have this₁ : HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)
Tactic: rw [e'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ (a.oadd m b).repr = succ zero.repr ∧ ((a.oadd m b).NF → zero.NF)
have oadd : (a.oadd 1 b).repr = succ zero.repr ∧ ((a.oadd 1 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]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ (a.oadd m b).repr = succ zero.repr ∧ ((a.oadd m b).NF → zero.NF)
have oadd : (a.oadd 1 b).repr = succ zero.repr ∧ ((a.oadd 1 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]
-- 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
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
⊢ m = 1
have this : m.natPred + 1 = (↑m : ℕ)
Tactic: have := PNat.natPred_add_one m
-- 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
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 : ℕ)
⊢ m = 1
have this₁ : HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)
Tactic: rw [e'] at this
Cleared hypotheses: this
-- 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')
e' : m.natPred = 0
⊢ 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
have 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
Tactic: rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]
-- 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')
e' : m.natPred = 0
⊢ 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
have 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
Tactic: try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]
-- 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
⊢ m = 1
have this : m.natPred + 1 = (↑m : ℕ)
Tactic: have := PNat.natPred_add_one m
-- 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
this : m.natPred + 1 = (↑m : ℕ)
⊢ m = 1
have this₁ : HAdd.hAdd (α := ℕ) 0 1 = (↑m : ℕ)
Tactic: rw [e'] at this
Cleared hypotheses: this
-- 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
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.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
have 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
Tactic: rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]
-- 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
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.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
have 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
Tactic: try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]