case H₁
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
⊢ f i (derivFamily f 0) = derivFamily f 0

case H₂
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (derivFamily f (succ o)) = derivFamily f (succ o)

case H₃
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → f i (derivFamily f o') = derivFamily f o'
⊢ f i (derivFamily f o) = derivFamily f o
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
⊢ f i (derivFamily f o) = derivFamily f o
induction' o using limitRecOn with o _  o l IH
case H₁
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0
case H₁
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
⊢ f i (derivFamily f 0) = derivFamily f 0
rw [derivFamily_zero]
no goals
case H₁
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0
exact nfpFamily_fp H 0
case H₂
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (nfpFamily f (succ (derivFamily f o))) = nfpFamily f (succ (derivFamily f o))
case H₂
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (derivFamily f (succ o)) = derivFamily f (succ o)
rw [derivFamily_succ]
no goals
case H₂
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (nfpFamily f (succ (derivFamily f o))) = nfpFamily f (succ (derivFamily f o))
exact nfpFamily_fp H _
case H₃
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → f i (derivFamily f o') = derivFamily f o'
⊢ (bsup o fun a h => f i (derivFamily f a)) = bsup o fun a x => derivFamily f a
case H₃
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → f i (derivFamily f o') = derivFamily f o'
⊢ f i (derivFamily f o) = derivFamily f o
rw [derivFamily_limit _ l,
  IsNormal.bsup.{max u v, u, max u v} H (fun a _ => derivFamily f a) l.1]
case H₃
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → f i (derivFamily f o') = derivFamily f o'
c : Ordinal
⊢ (bsup o fun a h => f i (derivFamily f a)) ≤ c ↔ (bsup o fun a x => derivFamily f a) ≤ c
case H₃
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → f i (derivFamily f o') = derivFamily f o'
⊢ (bsup o fun a h => f i (derivFamily f a)) = bsup o fun a x => derivFamily f a
refine' eq_of_forall_ge_iff fun c => _
no goals
case H₃
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → f i (derivFamily f o') = derivFamily f o'
c : Ordinal
⊢ (bsup o fun a h => f i (derivFamily f a)) ≤ c ↔ (bsup o fun a x => derivFamily f a) ≤ c
simp (config := { contextual := true }) only [bsup_le_iff, IH]