o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
⊢ StrictMono (derivBFamily o f) ∧ Set.range (derivBFamily o f) = ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
⊢ derivBFamily o f = enumOrd (⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi))
rw [← eq_enumOrd _ (fp_bfamily_unbounded.{u, v} H)]
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
⊢ Set.range (derivBFamily o f) = ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
⊢ StrictMono (derivBFamily o f) ∧ Set.range (derivBFamily o f) = ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)
use (derivBFamily_isNormal f).strictMono
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
⊢ (∀ (a : Ordinal), derivBFamily o f a ∈ ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)) ∧
    ∀ (b : Ordinal), (b ∈ ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)) → ∃ a, derivBFamily o f a = b
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
⊢ Set.range (derivBFamily o f) = ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)
rw [Set.range_eq_iff]
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
ha : a ∈ ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)
⊢ ∃ a_1, derivBFamily o f a_1 = a
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
⊢ (∀ (a : Ordinal), derivBFamily o f a ∈ ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)) ∧
    ∀ (b : Ordinal), (b ∈ ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)) → ∃ a, derivBFamily o f a = b
refine' ⟨fun a => Set.mem_iInter₂.2 fun i hi => derivBFamily_fp (H i hi) a, fun a ha => _⟩
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
ha : ∀ (i : Ordinal) (j : i < o), a ∈ fixedPoints (f i j)
⊢ ∃ a_1, derivBFamily o f a_1 = a
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
ha : a ∈ ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)
⊢ ∃ a_1, derivBFamily o f a_1 = a
rw [Set.mem_iInter₂] at ha
no goals
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
ha : ∀ (i : Ordinal) (j : i < o), a ∈ fixedPoints (f i j)
⊢ ∃ a_1, derivBFamily o f a_1 = a
rwa [← fp_iff_derivBFamily H]