-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem derivBFamily_eq_enumOrd (H : ∀ i hi, IsNormal (f i hi)) :
    derivBFamily.{u, v} o f = enumOrd (⋂ (i) (hi), Function.fixedPoints (f i hi))

Proof state:
case right
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
ha : a ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)
⊢ ∃ a_1, o.derivBFamily f a_1 = a

Tactic:
rw [Set.mem_iInter₂] at ha

Result:
case right
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
ha : ∀ (i : Ordinal.{u}) (j : i < o), a ∈ fixedPoints (f i j)
⊢ ∃ a_1, o.derivBFamily f a_1 = a

Proof state:
case right
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ Set.range (o.derivBFamily f) = ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)

Tactic:
rw [Set.range_eq_iff]

Result:
case right
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ (∀ (a : Ordinal.{max v u}), o.derivBFamily f a ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)) ∧
    ∀ b ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi), ∃ a, o.derivBFamily f a = b

Proof state:
case right
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ (∀ (a : Ordinal.{max v u}), o.derivBFamily f a ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)) ∧
    ∀ b ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi), ∃ a, o.derivBFamily f a = b

Tactic:
refine ⟨fun a => Set.mem_iInter₂.2 fun i hi => derivBFamily_fp (H i hi) a, fun a ha => ?_⟩

Result:
case right
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
ha : a ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)
⊢ ∃ a_1, o.derivBFamily f a_1 = a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ o.derivBFamily f = enumOrd (⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi))

Tactic:
rw [eq_comm, eq_enumOrd _ (not_bddAbove_fp_bfamily H)]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ StrictMono (o.derivBFamily f) ∧ Set.range (o.derivBFamily f) = ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)

Proof state:
case right
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
ha : ∀ (i : Ordinal.{u}) (j : i < o), a ∈ fixedPoints (f i j)
⊢ ∃ a_1, o.derivBFamily f a_1 = a

Tactic:
rwa [← fp_iff_derivBFamily H]

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ StrictMono (o.derivBFamily f) ∧ Set.range (o.derivBFamily f) = ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)

Tactic:
use (isNormal_derivBFamily f).strictMono

Result:
case right
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ Set.range (o.derivBFamily f) = ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)