a : Ordinal
⊢ (sup fun n => ((fun x => a + x)^[n]) 0) = sup fun n => a * ↑n
a : Ordinal
⊢ nfp (fun x => a + x) 0 = a * ω
simp_rw [← sup_iterate_eq_nfp, ← sup_mul_nat]
case e_f
a : Ordinal
⊢ (fun n => ((fun x => a + x)^[n]) 0) = fun n => a * ↑n
a : Ordinal
⊢ (sup fun n => ((fun x => a + x)^[n]) 0) = sup fun n => a * ↑n
congr
case e_f.h
a : Ordinal
n : ℕ
⊢ ((fun x => a + x)^[n]) 0 = a * ↑n
case e_f
a : Ordinal
⊢ (fun n => ((fun x => a + x)^[n]) 0) = fun n => a * ↑n
funext n
case e_f.h.zero
a : Ordinal
⊢ ((fun x => a + x)^[Nat.zero]) 0 = a * ↑Nat.zero

case e_f.h.succ
a : Ordinal
n : ℕ
hn : ((fun x => a + x)^[n]) 0 = a * ↑n
⊢ ((fun x => a + x)^[Nat.succ n]) 0 = a * ↑(Nat.succ n)
case e_f.h
a : Ordinal
n : ℕ
⊢ ((fun x => a + x)^[n]) 0 = a * ↑n
induction' n with n hn
no goals
case e_f.h.zero
a : Ordinal
⊢ ((fun x => a + x)^[Nat.zero]) 0 = a * ↑Nat.zero
rw [Nat.cast_zero, mul_zero, iterate_zero_apply]
case e_f.h.succ
a : Ordinal
n : ℕ
hn : ((fun x => a + x)^[n]) 0 = a * ↑n
⊢ ((fun x => a + x)^[Nat.succ n]) 0 = a * ↑(1 + n)
case e_f.h.succ
a : Ordinal
n : ℕ
hn : ((fun x => a + x)^[n]) 0 = a * ↑n
⊢ ((fun x => a + x)^[Nat.succ n]) 0 = a * ↑(Nat.succ n)
nth_rw 2 [Nat.succ_eq_one_add]
no goals
case e_f.h.succ
a : Ordinal
n : ℕ
hn : ((fun x => a + x)^[n]) 0 = a * ↑n
⊢ ((fun x => a + x)^[Nat.succ n]) 0 = a * ↑(1 + n)
rw [Nat.cast_add, Nat.cast_one, mul_one_add, iterate_succ_apply', hn]