a : Ordinal
ha : 0 < a
⊢ (fun a_1 => sup fun n => ((fun x => a * x)^[n]) a_1) 1 = sup fun n => a ^ ↑n

a : Ordinal
ha : 0 < a
⊢ 0 < a
a : Ordinal
ha : 0 < a
⊢ nfp (fun x => a * x) 1 = a ^ ω
rw [← sup_iterate_eq_nfp, ← sup_opow_nat]
a : Ordinal
ha : 0 < a
⊢ (sup fun n => ((fun x => a * x)^[n]) 1) = sup fun n => a ^ ↑n
a : Ordinal
ha : 0 < a
⊢ (fun a_1 => sup fun n => ((fun x => a * x)^[n]) a_1) 1 = sup fun n => a ^ ↑n
dsimp
case e_f
a : Ordinal
ha : 0 < a
⊢ (fun n => ((fun x => a * x)^[n]) 1) = fun n => a ^ ↑n
a : Ordinal
ha : 0 < a
⊢ (sup fun n => ((fun x => a * x)^[n]) 1) = sup fun n => a ^ ↑n
congr
case e_f.h
a : Ordinal
ha : 0 < a
n : ℕ
⊢ ((fun x => a * x)^[n]) 1 = a ^ ↑n
case e_f
a : Ordinal
ha : 0 < a
⊢ (fun n => ((fun x => a * x)^[n]) 1) = fun n => a ^ ↑n
funext n
case e_f.h.zero
a : Ordinal
ha : 0 < a
⊢ ((fun x => a * x)^[Nat.zero]) 1 = a ^ ↑Nat.zero

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