f : Ordinal → Ordinal
a : Ordinal
⊢ (sup fun n => id a) = id a
f : Ordinal → Ordinal
a : Ordinal
⊢ nfp id a = id a
simp_rw [← sup_iterate_eq_nfp, iterate_id]
no goals
f : Ordinal → Ordinal
a : Ordinal
⊢ (sup fun n => id a) = id a
exact sup_const a