case refine'_1
f✝ f : Ordinal → Ordinal
a : Ordinal
⊢ (sup fun n => (f^[n]) a) ≤ nfp f a

case refine'_2
f✝ f : Ordinal → Ordinal
a : Ordinal
l : List Unit
⊢ List.foldr (fun x => f) a l ≤ sup fun n => (f^[n]) a
f✝ f : Ordinal → Ordinal
⊢ (fun a => sup fun n => (f^[n]) a) = nfp f
refine' funext fun a => le_antisymm _ (sup_le fun l => _)
case refine'_1
f✝ f : Ordinal → Ordinal
a : Ordinal
⊢ ∀ (i : ℕ), (f^[i]) a ≤ nfp f a
case refine'_1
f✝ f : Ordinal → Ordinal
a : Ordinal
⊢ (sup fun n => (f^[n]) a) ≤ nfp f a
rw [sup_le_iff]
case refine'_1
f✝ f : Ordinal → Ordinal
a : Ordinal
n : ℕ
⊢ (f^[n]) a ≤ nfp f a
case refine'_1
f✝ f : Ordinal → Ordinal
a : Ordinal
⊢ ∀ (i : ℕ), (f^[i]) a ≤ nfp f a
intro n
case refine'_1
f✝ f : Ordinal → Ordinal
a : Ordinal
n : ℕ
⊢ List.foldr (fun x => f) a (List.replicate n ()) ≤ nfp f a
case refine'_1
f✝ f : Ordinal → Ordinal
a : Ordinal
n : ℕ
⊢ (f^[n]) a ≤ nfp f a
rw [← List.length_replicate n Unit.unit, ← List.foldr_const f a]
no goals
case refine'_1
f✝ f : Ordinal → Ordinal
a : Ordinal
n : ℕ
⊢ List.foldr (fun x => f) a (List.replicate n ()) ≤ nfp f a
apply le_sup
case refine'_2
f✝ f : Ordinal → Ordinal
a : Ordinal
l : List Unit
⊢ (f^[List.length l]) a ≤ sup fun n => (f^[n]) a
case refine'_2
f✝ f : Ordinal → Ordinal
a : Ordinal
l : List Unit
⊢ List.foldr (fun x => f) a l ≤ sup fun n => (f^[n]) a
rw [List.foldr_const f a l]
no goals
case refine'_2
f✝ f : Ordinal → Ordinal
a : Ordinal
l : List Unit
⊢ (f^[List.length l]) a ≤ sup fun n => (f^[n]) a
exact le_sup _ _