-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem add_nfBelow {b} : ∀ {o₁ o₂}, NFBelow o₁ b → NFBelow o₂ b → NFBelow (o₁ + o₂) b
  | 0, _, _, h₂ => h₂
  | oadd e n a, o, h₁, h₂ => by
    have h' := add_nfBelow (h₁.snd.mono <| le_of_lt h₁.lt) h₂
    simp only [oadd_add]; revert h'; obtain - | ⟨e', n', a'⟩ := a + o <;> intro h'
    · exact NFBelow.oadd h₁.fst NFBelow.zero h₁.lt
    have : ((e.cmp e').Compares e e') := @cmp_compares _ _ h₁.fst h'.fst
    cases h : cmp e e' <;> dsimp [addAux] <;> simp only [h]
    · exact h'
    · simp only [h] at this
      subst e'
      exact NFBelow.oadd h'.fst h'.snd h'.lt
    · simp only [h] at this
      exact NFBelow.oadd h₁.fst (NF.below_of_lt this ⟨⟨_, h'⟩⟩) h₁.lt

Proof state:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.addAux n (a + o)).NFBelow b

Tactic:
revert h'

Result:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (a + o).NFBelow b → (e.addAux n (a + o)).NFBelow b

Proof state:
case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
n' : ℕ+
a' : ONote
h' : (e.oadd n' a').NFBelow b
h : e.cmp e = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

Tactic:
exact NFBelow.oadd h'.fst h'.snd h'.lt

Result:
no goals

Proof state:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.oadd n a + o).NFBelow b

Tactic:
simp only [oadd_add]

Result:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.addAux n (a + o)).NFBelow b

Proof state:
case oadd.lt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (e'.oadd n' a').NFBelow b

Tactic:
exact h'

Result:
no goals

Proof state:
case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.eq
this : Ordering.eq.Compares e e'
⊢ (e.oadd (n + n') a').NFBelow b

Tactic:
subst e'

Result:
case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
n' : ℕ+
a' : ONote
h' : (e.oadd n' a').NFBelow b
h : e.cmp e = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

Proof state:
case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

Tactic:
simp only [h] at this

Result:
case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.eq
this : Ordering.eq.Compares e e'
⊢ (e.oadd (n + n') a').NFBelow b

Proof state:
case zero
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : zero.NFBelow b
⊢ (e.addAux n zero).NFBelow b

Tactic:
exact NFBelow.oadd h₁.fst NFBelow.zero h₁.lt

Result:
no goals

Proof state:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (a + o).NFBelow b → (e.addAux n (a + o)).NFBelow b

Tactic:
obtain - | ⟨e', n', a'⟩ := a + o <;> intro h'

Result:
case zero
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : zero.NFBelow b
⊢ (e.addAux n zero).NFBelow b

case oadd
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Proof state:
case oadd
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
have : ((e.cmp e').Compares e e') := @cmp_compares _ _ h₁.fst h'.fst

Result:
case oadd
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Proof state:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (e.oadd n a + o).NFBelow b

Tactic:
have h' := add_nfBelow (h₁.snd.mono <| le_of_lt h₁.lt) h₂

Result:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.oadd n a + o).NFBelow b

Proof state:
case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.gt
this : Ordering.gt.Compares e e'
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b

Tactic:
exact NFBelow.oadd h₁.fst (NF.below_of_lt this ⟨⟨_, h'⟩⟩) h₁.lt

Result:
no goals

Proof state:
case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b

Tactic:
simp only [h] at this

Result:
case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.gt
this : Ordering.gt.Compares e e'
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b

Proof state:
case oadd
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
cases h : cmp e e' <;> dsimp [addAux] <;> simp only [h]

Result:
case oadd.lt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (e'.oadd n' a').NFBelow b

case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b