a : Ordinal
ha : 0 < a
⊢ ∀ (b : Ordinal), deriv (fun x => a * x) b = a ^ ω * b
a : Ordinal
ha : 0 < a
b : Ordinal
⊢ deriv (fun x => a * x) b = a ^ ω * b
revert b
a : Ordinal
ha : 0 < a
⊢ 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
ha : 0 < a
⊢ ∀ (b : Ordinal), deriv (fun x => a * x) b = a ^ ω * b
rw [← funext_iff,
  IsNormal.eq_iff_zero_and_succ (deriv_isNormal _) (mul_isNormal (opow_pos omega ha))]
case refine'_1
a : Ordinal
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = (fun x x_1 => x * x_1) (a ^ ω) 0

case refine'_2
a : Ordinal
ha : 0 < a
c : Ordinal
h : deriv (fun x => a * x) c = (fun x x_1 => x * x_1) (a ^ ω) c
⊢ deriv (fun x => a * x) (succ c) = (fun x x_1 => x * x_1) (a ^ ω) (succ c)
a : Ordinal
ha : 0 < a
⊢ 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 c h => _⟩
case refine'_1
a : Ordinal
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = a ^ ω * 0
case refine'_1
a : Ordinal
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = (fun x x_1 => x * x_1) (a ^ ω) 0
dsimp only
no goals
case refine'_1
a : Ordinal
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = a ^ ω * 0
rw [deriv_zero, nfp_mul_zero, mul_zero]
case refine'_2
a : Ordinal
ha : 0 < a
c : Ordinal
h : deriv (fun x => a * x) c = (fun x x_1 => x * x_1) (a ^ ω) c
⊢ nfp (fun x => a * x) (succ ((fun x x_1 => x * x_1) (a ^ ω) c)) = (fun x x_1 => x * x_1) (a ^ ω) (succ c)
case refine'_2
a : Ordinal
ha : 0 < a
c : Ordinal
h : deriv (fun x => a * x) c = (fun x x_1 => x * x_1) (a ^ ω) c
⊢ deriv (fun x => a * x) (succ c) = (fun x x_1 => x * x_1) (a ^ ω) (succ c)
rw [deriv_succ, h]
no goals
case refine'_2
a : Ordinal
ha : 0 < a
c : Ordinal
h : deriv (fun x => a * x) c = (fun x x_1 => x * x_1) (a ^ ω) c
⊢ nfp (fun x => a * x) (succ ((fun x x_1 => x * x_1) (a ^ ω) c)) = (fun x x_1 => x * x_1) (a ^ ω) (succ c)
exact nfp_mul_opow_omega_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))