case h.e'_3.h.e'_1
f : Ordinal → Ordinal
H : IsNormal f
⊢ fixedPoints f = ⋂ (i : Unit), fixedPoints f
f : Ordinal → Ordinal
H : IsNormal f
⊢ deriv f = enumOrd (fixedPoints f)
convert derivFamily_eq_enumOrd fun _ : Unit => H
no goals
case h.e'_3.h.e'_1
f : Ordinal → Ordinal
H : IsNormal f
⊢ fixedPoints f = ⋂ (i : Unit), fixedPoints f
exact (Set.iInter_const _).symm