-- 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')
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
⊢ 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₁ : ∀ (m' : ℕ) (e' : m.natPred = m' + 1),
  match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) Sum.inl (some a'), m' + 1 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'