-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem derivFamily_fp [Small.{u} ι] {i} (H : IsNormal (f i)) (o : Ordinal) :
    f i (derivFamily f o) = derivFamily f o

Proof state:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
⊢ f i (derivFamily f o) = derivFamily f o

Tactic:
have : Nonempty (Set.Iio o) := ⟨0, l.pos⟩

Result:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ f i (derivFamily f o) = derivFamily f o

Proof state:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
a : ↑(Set.Iio o)
⊢ f i (derivFamily f ↑a) ≤ c ↔ derivFamily f ↑a ≤ c

Tactic:
rw [IH _ a.2]

Result:
no goals

Proof state:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) ≤ c ↔ ⨆ b, derivFamily f ↑b ≤ c

Tactic:
rw [Ordinal.iSup_le_iff, Ordinal.iSup_le_iff]

Result:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ (∀ (i_1 : ↑(Set.Iio o)), f i (derivFamily f ↑i_1) ≤ c) ↔ ∀ (i : ↑(Set.Iio o)), derivFamily f ↑i ≤ c

Proof state:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) = ⨆ b, derivFamily f ↑b

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Result:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) ≤ c ↔ ⨆ b, derivFamily f ↑b ≤ c

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

Tactic:
induction' o using limitRecOn with o _ o l IH

Result:
case H₁
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (derivFamily f 0) = derivFamily f 0

case H₂
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (derivFamily f (succ o)) = derivFamily f (succ o)

case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
⊢ f i (derivFamily f o) = derivFamily f o

Proof state:
case H₁
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0

Tactic:
exact nfpFamily_fp H 0

Result:
no goals

Proof state:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ (∀ (i_1 : ↑(Set.Iio o)), f i (derivFamily f ↑i_1) ≤ c) ↔ ∀ (i : ↑(Set.Iio o)), derivFamily f ↑i ≤ c

Tactic:
refine forall_congr' fun a ↦ ?_

Result:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
a : ↑(Set.Iio o)
⊢ f i (derivFamily f ↑a) ≤ c ↔ derivFamily f ↑a ≤ c

Proof state:
case H₂
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (derivFamily f (succ o)) = derivFamily f (succ o)

Tactic:
rw [derivFamily_succ]

Result:
case H₂
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (nfpFamily f (succ (derivFamily f o))) = nfpFamily f (succ (derivFamily f o))

Proof state:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ f i (derivFamily f o) = derivFamily f o

Tactic:
rw [derivFamily_limit _ l, H.map_iSup]

Result:
case H₃
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : o.IsLimit
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) = ⨆ b, derivFamily f ↑b

Proof state:
case H₂
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (nfpFamily f (succ (derivFamily f o))) = nfpFamily f (succ (derivFamily f o))

Tactic:
exact nfpFamily_fp H _

Result:
no goals

Proof state:
case H₁
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (derivFamily f 0) = derivFamily f 0

Tactic:
rw [derivFamily_zero]

Result:
case H₁
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0