f✝ : Ordinal → Ordinal
f : Ordinal → Ordinal
a : Ordinal
n : ℕ
⊢ (f^[n]) a ≤ (fun a => sup fun n => (f^[n]) a) a
f✝ : Ordinal → Ordinal
f : Ordinal → Ordinal
a : Ordinal
n : ℕ
⊢ (f^[n]) a ≤ nfp f a
rw [← sup_iterate_eq_nfp]
no goals
f✝ : Ordinal → Ordinal
f : Ordinal → Ordinal
a : Ordinal
n : ℕ
⊢ (f^[n]) a ≤ (fun a => sup fun n => (f^[n]) a) a
exact le_sup _ n