ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
this : ∀ (o : Ordinal), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
⊢ ∃ o, derivFamily f o = a

case this
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
⊢ ∀ (o : Ordinal), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
⊢ ∃ o, derivFamily f o = a
suffices : ∀ (o) (_ : a ≤ derivFamily.{u, v} f o), ∃ o, derivFamily.{u, v} f o = a
case this
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
⊢ ∀ (o : Ordinal), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
this : ∀ (o : Ordinal), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
⊢ ∃ o, derivFamily f o = a

case this
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
⊢ ∀ (o : Ordinal), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
exact this a ((derivFamily_isNormal _).self_le _)
case this
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = a
case this
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
⊢ ∀ (o : Ordinal), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
intro o
case this.H₁
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
⊢ a ≤ derivFamily f 0 → ∃ o, derivFamily f o = a

case this.H₂
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
⊢ a ≤ derivFamily f (succ o) → ∃ o, derivFamily f o = a

case this.H₃
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = a
case this
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = a
induction' o using limitRecOn with o IH o l IH
case this.H₁
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ ∃ o, derivFamily f o = a
case this.H₁
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
⊢ a ≤ derivFamily f 0 → ∃ o, derivFamily f o = a
intro h₁
case this.H₁
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ derivFamily f 0 ≤ a
case this.H₁
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ ∃ o, derivFamily f o = a
refine' ⟨0, le_antisymm _ h₁⟩
case this.H₁
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ nfpFamily f 0 ≤ a
case this.H₁
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ derivFamily f 0 ≤ a
rw [derivFamily_zero]
no goals
case this.H₁
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ nfpFamily f 0 ≤ a
exact nfpFamily_le_fp (fun i => (H i).monotone) (Ordinal.zero_le _) ha
case this.H₂
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
⊢ ∃ o, derivFamily f o = a
case this.H₂
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
⊢ a ≤ derivFamily f (succ o) → ∃ o, derivFamily f o = a
intro h₁
case this.H₂.inl
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
h : a ≤ derivFamily f o
⊢ ∃ o, derivFamily f o = a

case this.H₂.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
h : derivFamily f o < a
⊢ ∃ o, derivFamily f o = a
case this.H₂
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
⊢ ∃ o, derivFamily f o = a
cases' le_or_lt a (derivFamily.{u, v} f o) with h h
case this.H₂.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
h : derivFamily f o < a
⊢ derivFamily f (succ o) ≤ a
case this.H₂.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
h : derivFamily f o < a
⊢ ∃ o, derivFamily f o = a
refine' ⟨succ o, le_antisymm _ h₁⟩
case this.H₂.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
h : derivFamily f o < a
⊢ nfpFamily f (succ (derivFamily f o)) ≤ a
case this.H₂.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
h : derivFamily f o < a
⊢ derivFamily f (succ o) ≤ a
rw [derivFamily_succ]
no goals
case this.H₂.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
h : derivFamily f o < a
⊢ nfpFamily f (succ (derivFamily f o)) ≤ a
exact nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha
no goals
case this.H₂.inl
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
h : a ≤ derivFamily f o
⊢ ∃ o, derivFamily f o = a
exact IH h
case this.H₃
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
⊢ ∃ o, derivFamily f o = a
case this.H₃
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = a
intro h₁
case this.H₃.inl
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a = derivFamily f o
⊢ ∃ o, derivFamily f o = a

case this.H₃.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a < derivFamily f o
⊢ ∃ o, derivFamily f o = a
case this.H₃
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
⊢ ∃ o, derivFamily f o = a
cases' eq_or_lt_of_le h₁ with h h
case this.H₃.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : ∃ x h, ¬derivFamily f x ≤ a
⊢ ∃ o, derivFamily f o = a
case this.H₃.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a < derivFamily f o
⊢ ∃ o, derivFamily f o = a
rw [derivFamily_limit _ l, ← not_le, bsup_le_iff, not_ball] at h
no goals
case this.H₃.inr
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : ∃ x h, ¬derivFamily f x ≤ a
⊢ ∃ o, derivFamily f o = a
exact
  let ⟨o', h, hl⟩ := h
  IH o' h (le_of_not_le hl)
no goals
case this.H₃.inl
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal
l : IsLimit o
IH : ∀ (o' : Ordinal), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a = derivFamily f o
⊢ ∃ o, derivFamily f o = a
exact ⟨_, h.symm⟩