a : Ordinal
⊢ ∀ (b : Ordinal), deriv (fun x => a + x) b = a * ω + b
a b : Ordinal
⊢ deriv (fun x => a + x) b = a * ω + b
revert b
a : Ordinal
⊢ deriv (fun x => a + x) 0 = (fun x x_1 => x + x_1) (a * ω) 0 ∧
    ∀ (a_1 : Ordinal),
      deriv (fun x => a + x) a_1 = (fun x x_1 => x + x_1) (a * ω) a_1 →
        deriv (fun x => a + x) (succ a_1) = (fun x x_1 => x + x_1) (a * ω) (succ a_1)
a : Ordinal
⊢ ∀ (b : Ordinal), deriv (fun x => a + x) b = a * ω + b
rw [← funext_iff, IsNormal.eq_iff_zero_and_succ (deriv_isNormal _) (add_isNormal _)]
case refine'_1
a : Ordinal
⊢ deriv (fun x => a + x) 0 = (fun x x_1 => x + x_1) (a * ω) 0

case refine'_2
a✝ a : Ordinal
h : deriv (fun x => a✝ + x) a = (fun x x_1 => x + x_1) (a✝ * ω) a
⊢ deriv (fun x => a✝ + x) (succ a) = (fun x x_1 => x + x_1) (a✝ * ω) (succ a)
a : Ordinal
⊢ deriv (fun x => a + x) 0 = (fun x x_1 => x + x_1) (a * ω) 0 ∧
    ∀ (a_1 : Ordinal),
      deriv (fun x => a + x) a_1 = (fun x x_1 => x + x_1) (a * ω) a_1 →
        deriv (fun x => a + x) (succ a_1) = (fun x x_1 => x + x_1) (a * ω) (succ a_1)
refine' ⟨_, fun a h => _⟩
case refine'_1
a : Ordinal
⊢ deriv (fun x => a + x) 0 = a * ω + 0
case refine'_1
a : Ordinal
⊢ deriv (fun x => a + x) 0 = (fun x x_1 => x + x_1) (a * ω) 0
dsimp
case refine'_1
a : Ordinal
⊢ nfp (fun x => a + x) 0 = a * ω
case refine'_1
a : Ordinal
⊢ deriv (fun x => a + x) 0 = a * ω + 0
rw [deriv_zero, add_zero]
no goals
case refine'_1
a : Ordinal
⊢ nfp (fun x => a + x) 0 = a * ω
exact nfp_add_zero a
case refine'_2
a✝ a : Ordinal
h : deriv (fun x => a✝ + x) a = (fun x x_1 => x + x_1) (a✝ * ω) a
⊢ deriv (fun x => a✝ + x) (succ a) = a✝ * ω + succ a
case refine'_2
a✝ a : Ordinal
h : deriv (fun x => a✝ + x) a = (fun x x_1 => x + x_1) (a✝ * ω) a
⊢ deriv (fun x => a✝ + x) (succ a) = (fun x x_1 => x + x_1) (a✝ * ω) (succ a)
dsimp
case refine'_2
a✝ a : Ordinal
h : deriv (fun x => a✝ + x) a = (fun x x_1 => x + x_1) (a✝ * ω) a
⊢ nfp (fun x => a✝ + x) (succ ((fun x x_1 => x + x_1) (a✝ * ω) a)) = succ (a✝ * ω + a)
case refine'_2
a✝ a : Ordinal
h : deriv (fun x => a✝ + x) a = (fun x x_1 => x + x_1) (a✝ * ω) a
⊢ deriv (fun x => a✝ + x) (succ a) = a✝ * ω + succ a
rw [deriv_succ, h, add_succ]
no goals
case refine'_2
a✝ a : Ordinal
h : deriv (fun x => a✝ + x) a = (fun x x_1 => x + x_1) (a✝ * ω) a
⊢ nfp (fun x => a✝ + x) (succ ((fun x x_1 => x + x_1) (a✝ * ω) a)) = succ (a✝ * ω + a)
exact nfp_eq_self (add_eq_right_iff_mul_omega_le.2 ((le_add_right _ _).trans (le_succ _)))