-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem derivFamily_eq_enumOrd [Small.{u} ι] (H : ∀ i, IsNormal (f i)) :
    derivFamily f = enumOrd (⋂ i, Function.fixedPoints (f i))

Proof state:
case right.refine_1.intro
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
S : Set Ordinal.{u}
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ S

Tactic:
rw [← hi]

Result:
case right.refine_1.intro
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
S : Set Ordinal.{u}
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ (fun i => fixedPoints (f i)) i

Proof state:
case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)

Tactic:
rw [Set.range_eq_iff]

Result:
case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)) ∧
    ∀ b ∈ ⋂ i, fixedPoints (f i), ∃ a, derivFamily f a = b

Proof state:
case right.refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)

Tactic:
rintro a S ⟨i, hi⟩

Result:
case right.refine_1.intro
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
S : Set Ordinal.{u}
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ S

Proof state:
case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a

Tactic:
rwa [← fp_iff_derivFamily H]

Result:
no goals

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ derivFamily f = enumOrd (⋂ i, fixedPoints (f i))

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

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)

Proof state:
case right.refine_1.intro
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
S : Set Ordinal.{u}
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ (fun i => fixedPoints (f i)) i

Tactic:
exact derivFamily_fp (H i) a

Result:
no goals

Proof state:
case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)) ∧
    ∀ b ∈ ⋂ i, fixedPoints (f i), ∃ a, derivFamily f a = b

Tactic:
refine ⟨?_, fun a ha => ?_⟩

Result:
case right.refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)

case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : a ∈ ⋂ i, fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a

Proof state:
case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : a ∈ ⋂ i, fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a

Tactic:
rw [Set.mem_iInter] at ha

Result:
case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)

Tactic:
use (isNormal_derivFamily f).strictMono

Result:
case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)