ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
⊢ derivFamily f = enumOrd (⋂ (i : ι), fixedPoints (f i))
rw [← eq_enumOrd _ (fp_family_unbounded.{u, v} H)]
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
⊢ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
use (derivFamily_isNormal f).strictMono
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal), derivFamily f a ∈ ⋂ (i : ι), fixedPoints (f i)) ∧
    ∀ (b : Ordinal), (b ∈ ⋂ (i : ι), fixedPoints (f i)) → ∃ a, derivFamily f a = b
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
⊢ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
rw [Set.range_eq_iff]
case refine'_1
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (a : Ordinal), derivFamily f a ∈ ⋂ (i : ι), fixedPoints (f i)

case refine'_2
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : a ∈ ⋂ (i : ι), fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal), derivFamily f a ∈ ⋂ (i : ι), fixedPoints (f i)) ∧
    ∀ (b : Ordinal), (b ∈ ⋂ (i : ι), fixedPoints (f i)) → ∃ a, derivFamily f a = b
refine' ⟨_, fun a ha => _⟩
case refine'_2
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a
case refine'_2
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : a ∈ ⋂ (i : ι), fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a
rw [Set.mem_iInter] at ha
no goals
case refine'_2
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a
rwa [← fp_iff_derivFamily H]
case refine'_1.intro
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
S : Set Ordinal
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ S
case refine'_1
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (a : Ordinal), derivFamily f a ∈ ⋂ (i : ι), fixedPoints (f i)
rintro a S ⟨i, hi⟩
case refine'_1.intro
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
S : Set Ordinal
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ (fun i => fixedPoints (f i)) i
case refine'_1.intro
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
S : Set Ordinal
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ S
rw [← hi]
no goals
case refine'_1.intro
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
S : Set Ordinal
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ (fun i => fixedPoints (f i)) i
exact derivFamily_fp (H i) a