[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
inst✝ : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{max u v}
⊢ (∃ i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
inst✝ : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{max u v}
⊢ (¬∃ i, nfpFamily f a ≤ f i b) ↔ ¬nfpFamily f a ≤ b
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
inst✝ : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{max u v}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a
[PROOFSTEP]
exact apply_lt_nfpFamily_iff H
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{max u v}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
⊢ List.foldr f a l ≤ b
[PROOFSTEP]
by_cases hι : IsEmpty ι
[GOAL]
case pos
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{max u v}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
hι : IsEmpty ι
⊢ List.foldr f a l ≤ b
[PROOFSTEP]
rwa [Unique.eq_default l]
[GOAL]
case neg
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{max u v}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
hι : ¬IsEmpty ι
⊢ List.foldr f a l ≤ b
[PROOFSTEP]
induction' l with i l IH generalizing a
[GOAL]
case neg.nil
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), Monotone (f i)
a✝ b : Ordinal.{max u v}
ab✝ : a✝ ≤ b
h : ∀ (i : ι), f i b ≤ b
hι : ¬IsEmpty ι
a : Ordinal.{max u v}
ab : a ≤ b
⊢ List.foldr f a [] ≤ b
[PROOFSTEP]
exact ab
[GOAL]
case neg.cons
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), Monotone (f i)
a✝ b : Ordinal.{max u v}
ab✝ : a✝ ≤ b
h : ∀ (i : ι), f i b ≤ b
hι : ¬IsEmpty ι
i : ι
l : List ι
IH : ∀ {a : Ordinal.{max u v}}, a ≤ b → List.foldr f a l ≤ b
a : Ordinal.{max u v}
ab : a ≤ b
⊢ List.foldr f a (i :: l) ≤ b
[PROOFSTEP]
exact (H i (IH ab)).trans (h i)
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
a : Ordinal.{max u v}
⊢ f i (nfpFamily f a) = nfpFamily f a
[PROOFSTEP]
unfold nfpFamily
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
a : Ordinal.{max u v}
⊢ f i (sup (List.foldr f a)) = sup (List.foldr f a)
[PROOFSTEP]
rw [@IsNormal.sup.{u, v, v} _ H _ _ ⟨[]⟩]
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
a : Ordinal.{max u v}
⊢ sup (f i ∘ List.foldr f a) = sup (List.foldr f a)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
a : Ordinal.{max u v}
⊢ sup (f i ∘ List.foldr f a) ≤ sup (List.foldr f a)
[PROOFSTEP]
refine' Ordinal.sup_le fun l => _
[GOAL]
case a
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
a : Ordinal.{max u v}
⊢ sup (List.foldr f a) ≤ sup (f i ∘ List.foldr f a)
[PROOFSTEP]
refine' Ordinal.sup_le fun l => _
[GOAL]
case a
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
a : Ordinal.{max u v}
l : List ι
⊢ (f i ∘ List.foldr f a) l ≤ sup (List.foldr f a)
[PROOFSTEP]
exact le_sup _ (i :: l)
[GOAL]
case a
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
a : Ordinal.{max u v}
l : List ι
⊢ List.foldr f a l ≤ sup (f i ∘ List.foldr f a)
[PROOFSTEP]
exact (H.self_le _).trans (le_sup _ _)
[GOAL]
ι : Type u
f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}
hι : Nonempty ι
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{max u v}
⊢ (∀ (i : ι), f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a
[PROOFSTEP]
refine' ⟨fun h => _, fun h i => _⟩
[GOAL]
case refine'_1
ι : Type u
f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}
hι : Nonempty ι
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{max u v}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a
[PROOFSTEP]
cases' hι with i
[GOAL]
case refine'_1.intro
ι : Type u
f✝ f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{max u v}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
i : ι
⊢ b ≤ nfpFamily f a
[PROOFSTEP]
exact ((H i).self_le b).trans (h i)
[GOAL]
case refine'_2
ι : Type u
f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}
hι : Nonempty ι
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{max u v}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a
[PROOFSTEP]
rw [← nfpFamily_fp (H i)]
[GOAL]
case refine'_2
ι : Type u
f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}
hι : Nonempty ι
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{max u v}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ f i (nfpFamily f a)
[PROOFSTEP]
exact (H i).monotone h
[GOAL]
ι : Type u
f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}
f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}
a : Ordinal.{max u u_1}
h : ∀ (i : ι), f i a = a
l : List ι
⊢ List.foldr f a l ≤ a
[PROOFSTEP]
rw [List.foldr_fixed' h l]
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
s : Set Ordinal.{max u v}
x✝ : s ∈ Set.range fun i => fixedPoints (f i)
i : ι
hi : (fun i => fixedPoints (f i)) i = s
⊢ nfpFamily f a ∈ s
[PROOFSTEP]
rw [← hi, mem_fixedPoints_iff]
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
s : Set Ordinal.{max u v}
x✝ : s ∈ Set.range fun i => fixedPoints (f i)
i : ι
hi : (fun i => fixedPoints (f i)) i = s
⊢ f i (nfpFamily f a) = nfpFamily f a
[PROOFSTEP]
exact nfpFamily_fp.{u, v} (H i) a
[GOAL]
ι : Type u
f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}
f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}
o : Ordinal.{max u_1 u}
⊢ derivFamily f o < derivFamily f (succ o)
[PROOFSTEP]
rw [derivFamily_succ, ← succ_le_iff]
[GOAL]
ι : Type u
f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}
f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}
o : Ordinal.{max u_1 u}
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))
[PROOFSTEP]
apply le_nfpFamily
[GOAL]
ι : Type u
f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}
f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}
o : Ordinal.{max u_1 u}
l : IsLimit o
a : Ordinal.{max u_1 u}
⊢ derivFamily f o ≤ a ↔ ∀ (b : Ordinal.{max u_1 u}), b < o → derivFamily f b ≤ a
[PROOFSTEP]
rw [derivFamily_limit _ l, bsup_le_iff]
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
o : Ordinal.{max u v}
⊢ f i (derivFamily f o) = derivFamily f o
[PROOFSTEP]
induction' o using limitRecOn with o _ o l IH
[GOAL]
case H₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
⊢ f i (derivFamily f 0) = derivFamily f 0
[PROOFSTEP]
rw [derivFamily_zero]
[GOAL]
case H₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0
[PROOFSTEP]
exact nfpFamily_fp H 0
[GOAL]
case H₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
o : Ordinal.{max u v}
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (derivFamily f (succ o)) = derivFamily f (succ o)
[PROOFSTEP]
rw [derivFamily_succ]
[GOAL]
case H₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
o : Ordinal.{max u v}
a✝ : f i (derivFamily f o) = derivFamily f o
⊢ f i (nfpFamily f (succ (derivFamily f o))) = nfpFamily f (succ (derivFamily f o))
[PROOFSTEP]
exact nfpFamily_fp H _
[GOAL]
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
o : Ordinal.{max u v}
l : IsLimit o
IH : ∀ (o' : Ordinal.{max u v}), o' < o → f i (derivFamily f o') = derivFamily f o'
⊢ f i (derivFamily f o) = derivFamily f o
[PROOFSTEP]
rw [derivFamily_limit _ l, IsNormal.bsup.{max u v, u, max u v} H (fun a _ => derivFamily f a) l.1]
[GOAL]
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
o : Ordinal.{max u v}
l : IsLimit o
IH : ∀ (o' : Ordinal.{max u v}), 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
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun c => _
[GOAL]
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
i : ι
H : IsNormal (f i)
o : Ordinal.{max u v}
l : IsLimit o
IH : ∀ (o' : Ordinal.{max u v}), o' < o → f i (derivFamily f o') = derivFamily f o'
c : Ordinal.{max u v}
⊢ (bsup o fun a h => f i (derivFamily f a)) ≤ c ↔ (bsup o fun a x => derivFamily f a) ≤ c
[PROOFSTEP]
simp (config := { contextual := true }) only [bsup_le_iff, IH]
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
⊢ ∃ o, derivFamily f o = a
[PROOFSTEP]
suffices : ∀ (o) (_ : a ≤ derivFamily.{u, v} f o), ∃ o, derivFamily.{u, v} f o = a
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
this : ∀ (o : Ordinal.{max u v}), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
⊢ ∃ o, derivFamily f o = a
case this
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
⊢ ∀ (o : Ordinal.{max u v}), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
[PROOFSTEP]
exact this a ((derivFamily_isNormal _).self_le _)
[GOAL]
case this
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
⊢ ∀ (o : Ordinal.{max u v}), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
[PROOFSTEP]
intro o
[GOAL]
case this
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = a
[PROOFSTEP]
induction' o using limitRecOn with o IH o l IH
[GOAL]
case this.H₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
⊢ a ≤ derivFamily f 0 → ∃ o, derivFamily f o = a
[PROOFSTEP]
intro h₁
[GOAL]
case this.H₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ ∃ o, derivFamily f o = a
[PROOFSTEP]
refine' ⟨0, le_antisymm _ h₁⟩
[GOAL]
case this.H₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ derivFamily f 0 ≤ a
[PROOFSTEP]
rw [derivFamily_zero]
[GOAL]
case this.H₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ nfpFamily f 0 ≤ a
[PROOFSTEP]
exact nfpFamily_le_fp (fun i => (H i).monotone) (Ordinal.zero_le _) ha
[GOAL]
case this.H₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
⊢ a ≤ derivFamily f (succ o) → ∃ o, derivFamily f o = a
[PROOFSTEP]
intro h₁
[GOAL]
case this.H₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (succ o)
⊢ ∃ o, derivFamily f o = a
[PROOFSTEP]
cases' le_or_lt a (derivFamily.{u, v} f o) with h h
[GOAL]
case this.H₂.inl
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
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
[PROOFSTEP]
exact IH h
[GOAL]
case this.H₂.inr
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
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
[PROOFSTEP]
refine' ⟨succ o, le_antisymm _ h₁⟩
[GOAL]
case this.H₂.inr
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
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
[PROOFSTEP]
rw [derivFamily_succ]
[GOAL]
case this.H₂.inr
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
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
[PROOFSTEP]
exact nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha
[GOAL]
case this.H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
l : IsLimit o
IH : ∀ (o' : Ordinal.{max u v}), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = a
[PROOFSTEP]
intro h₁
[GOAL]
case this.H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
l : IsLimit o
IH : ∀ (o' : Ordinal.{max u v}), o' < o → a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
⊢ ∃ o, derivFamily f o = a
[PROOFSTEP]
cases' eq_or_lt_of_le h₁ with h h
[GOAL]
case this.H₃.inl
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
l : IsLimit o
IH : ∀ (o' : Ordinal.{max u v}), 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
[PROOFSTEP]
exact ⟨_, h.symm⟩
[GOAL]
case this.H₃.inr
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
l : IsLimit o
IH : ∀ (o' : Ordinal.{max u v}), 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
[PROOFSTEP]
rw [derivFamily_limit _ l, ← not_le, bsup_le_iff, not_ball] at h 
[GOAL]
case this.H₃.inr
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{max u v}
l : IsLimit o
IH : ∀ (o' : Ordinal.{max u v}), 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
[PROOFSTEP]
exact
  let ⟨o', h, hl⟩ := h
  IH o' h (le_of_not_le hl)
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
⊢ derivFamily f = enumOrd (⋂ (i : ι), fixedPoints (f i))
[PROOFSTEP]
rw [← eq_enumOrd _ (fp_family_unbounded.{u, v} H)]
[GOAL]
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
[PROOFSTEP]
use(derivFamily_isNormal f).strictMono
[GOAL]
case right
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
⊢ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
[PROOFSTEP]
rw [Set.range_eq_iff]
[GOAL]
case right
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal.{max u v}), derivFamily f a ∈ ⋂ (i : ι), fixedPoints (f i)) ∧
    ∀ (b : Ordinal.{max u v}), b ∈ ⋂ (i : ι), fixedPoints (f i) → ∃ a, derivFamily f a = b
[PROOFSTEP]
refine' ⟨_, fun a ha => _⟩
[GOAL]
case right.refine'_1
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (a : Ordinal.{max u v}), derivFamily f a ∈ ⋂ (i : ι), fixedPoints (f i)
[PROOFSTEP]
rintro a S ⟨i, hi⟩
[GOAL]
case right.refine'_1.intro
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
S : Set Ordinal.{max u v}
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ S
[PROOFSTEP]
rw [← hi]
[GOAL]
case right.refine'_1.intro
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
S : Set Ordinal.{max u v}
i : ι
hi : (fun i => fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ (fun i => fixedPoints (f i)) i
[PROOFSTEP]
exact derivFamily_fp (H i) a
[GOAL]
case right.refine'_2
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : a ∈ ⋂ (i : ι), fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a
[PROOFSTEP]
rw [Set.mem_iInter] at ha 
[GOAL]
case right.refine'_2
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{max u v}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a
[PROOFSTEP]
rwa [← fp_iff_derivFamily H]
[GOAL]
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 b : Ordinal.{max v u}
hb : b < nfpBFamily o f a
i : Ordinal.{u}
hi : i < o
⊢ f i hi b < nfpBFamily o f a
[PROOFSTEP]
rw [← familyOfBFamily_enum o f]
[GOAL]
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 b : Ordinal.{max v u}
hb : b < nfpBFamily o f a
i : Ordinal.{u}
hi : i < o
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) b < nfpBFamily o f a
[PROOFSTEP]
apply apply_lt_nfpFamily (fun _ => H _ _) hb
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < nfpBFamily o f a
⊢ b < nfpBFamily o f a
[PROOFSTEP]
haveI := out_nonempty_iff_ne_zero.2 ho
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < nfpBFamily o f a
this : Nonempty (Quotient.out o).α
⊢ b < nfpBFamily o f a
[PROOFSTEP]
refine' (apply_lt_nfpFamily_iff.{u, v} _).1 fun _ => h _ _
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < nfpBFamily o f a
this : Nonempty (Quotient.out o).α
⊢ ∀ (i : (Quotient.out o).α), IsNormal (familyOfBFamily o f i)
[PROOFSTEP]
exact fun _ => H _ _
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
⊢ (∃ i hi, nfpBFamily o f a ≤ f i hi b) ↔ nfpBFamily o f a ≤ b
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
⊢ (¬∃ i hi, nfpBFamily o f a ≤ f i hi b) ↔ ¬nfpBFamily o f a ≤ b
[PROOFSTEP]
push_neg
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < nfpBFamily o f a) ↔ b < nfpBFamily o f a
[PROOFSTEP]
exact apply_lt_nfpBFamily_iff.{u, v} ho H
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max v u}
⊢ f i hi (nfpBFamily o f a) = nfpBFamily o f a
[PROOFSTEP]
rw [← familyOfBFamily_enum o f]
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max v u}
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) (nfpBFamily o f a) =
    nfpBFamily o f a
[PROOFSTEP]
apply nfpFamily_fp
[GOAL]
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max v u}
⊢ IsNormal (familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)))
[PROOFSTEP]
rw [familyOfBFamily_enum]
[GOAL]
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max v u}
⊢ IsNormal (f i ?H.hi)
case H.hi
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max v u}
⊢ i < o
[PROOFSTEP]
exact H
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ nfpBFamily o f a) ↔ b ≤ nfpBFamily o f a
[PROOFSTEP]
refine' ⟨fun h => _, fun h i hi => _⟩
[GOAL]
case refine'_1
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ nfpBFamily o f a
⊢ b ≤ nfpBFamily o f a
[PROOFSTEP]
have ho' : 0 < o := Ordinal.pos_iff_ne_zero.2 ho
[GOAL]
case refine'_1
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ nfpBFamily o f a
ho' : 0 < o
⊢ b ≤ nfpBFamily o f a
[PROOFSTEP]
exact ((H 0 ho').self_le b).trans (h 0 ho')
[GOAL]
case refine'_2
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
h : b ≤ nfpBFamily o f a
i : Ordinal.{u}
hi : i < o
⊢ f i hi b ≤ nfpBFamily o f a
[PROOFSTEP]
rw [← nfpBFamily_fp (H i hi)]
[GOAL]
case refine'_2
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max v u}
b : Ordinal.{max u v}
h : b ≤ nfpBFamily o f a
i : Ordinal.{u}
hi : i < o
⊢ f i hi b ≤ f i hi (nfpBFamily o f a)
[PROOFSTEP]
exact (H i hi).monotone h
[GOAL]
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 u v}
⊢ nfpBFamily o f a ∈ ⋂ (i : Ordinal.{u}) (hi : i < o), fixedPoints (f i hi)
[PROOFSTEP]
rw [Set.mem_iInter₂]
[GOAL]
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 u v}
⊢ ∀ (i : Ordinal.{u}) (j : i < o), nfpBFamily o f a ∈ fixedPoints (f i j)
[PROOFSTEP]
exact fun i hi => nfpBFamily_fp (H i hi) _
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ f i hi (derivBFamily o f a) = derivBFamily o f a
[PROOFSTEP]
rw [← familyOfBFamily_enum o f]
[GOAL]
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) (derivBFamily o f a) =
    derivBFamily o f a
[PROOFSTEP]
apply derivFamily_fp
[GOAL]
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)))
[PROOFSTEP]
rw [familyOfBFamily_enum]
[GOAL]
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (f i ?H.hi)
case H.hi
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ i < o
[PROOFSTEP]
exact H
[GOAL]
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 u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∃ b, derivBFamily o f b = a
[PROOFSTEP]
unfold derivBFamily
[GOAL]
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 u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∃ b, derivFamily (familyOfBFamily o f) b = a
[PROOFSTEP]
rw [← le_iff_derivFamily]
[GOAL]
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 u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∀ (i : (Quotient.out o).α), familyOfBFamily o f i a ≤ a
[PROOFSTEP]
refine' ⟨fun h i => h _ _, fun h i hi => _⟩
[GOAL]
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 u v}
h : ∀ (i : (Quotient.out o).α), familyOfBFamily o f i a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi a ≤ a
[PROOFSTEP]
rw [← familyOfBFamily_enum o f]
[GOAL]
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 u v}
h : ∀ (i : (Quotient.out o).α), familyOfBFamily o f i a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) a ≤ a
[PROOFSTEP]
apply h
[GOAL]
case H
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 u v}
⊢ ∀ (i : (Quotient.out o).α), IsNormal (familyOfBFamily o f i)
[PROOFSTEP]
exact fun _ => H _ _
[GOAL]
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 u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ↔ ∃ b, derivBFamily o f b = a
[PROOFSTEP]
rw [← le_iff_derivBFamily H]
[GOAL]
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 u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ↔ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a
[PROOFSTEP]
refine' ⟨fun h i hi => le_of_eq (h i hi), fun h i hi => _⟩
[GOAL]
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 u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi a = a
[PROOFSTEP]
rw [← (H i hi).le_iff_eq]
[GOAL]
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 u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi a ≤ a
[PROOFSTEP]
exact h i hi
[GOAL]
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)
⊢ derivBFamily o f = enumOrd (⋂ (i : Ordinal.{u}) (hi : i < o), fixedPoints (f i hi))
[PROOFSTEP]
rw [← eq_enumOrd _ (fp_bfamily_unbounded.{u, v} H)]
[GOAL]
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 (derivBFamily o f) ∧ Set.range (derivBFamily o f) = ⋂ (i : Ordinal.{u}) (hi : i < o), fixedPoints (f i hi)
[PROOFSTEP]
use(derivBFamily_isNormal f).strictMono
[GOAL]
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 (derivBFamily o f) = ⋂ (i : Ordinal.{u}) (hi : i < o), fixedPoints (f i hi)
[PROOFSTEP]
rw [Set.range_eq_iff]
[GOAL]
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 u v}), derivBFamily o f a ∈ ⋂ (i : Ordinal.{u}) (hi : i < o), fixedPoints (f i hi)) ∧
    ∀ (b : Ordinal.{max u v}), b ∈ ⋂ (i : Ordinal.{u}) (hi : i < o), fixedPoints (f i hi) → ∃ a, derivBFamily o f a = b
[PROOFSTEP]
refine' ⟨fun a => Set.mem_iInter₂.2 fun i hi => derivBFamily_fp (H i hi) a, fun a ha => _⟩
[GOAL]
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 u v}
ha : a ∈ ⋂ (i : Ordinal.{u}) (hi : i < o), fixedPoints (f i hi)
⊢ ∃ a_1, derivBFamily o f a_1 = a
[PROOFSTEP]
rw [Set.mem_iInter₂] at ha 
[GOAL]
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 u v}
ha : ∀ (i : Ordinal.{u}) (j : i < o), a ∈ fixedPoints (f i j)
⊢ ∃ a_1, derivBFamily o f a_1 = a
[PROOFSTEP]
rwa [← fp_iff_derivBFamily H]
[GOAL]
f✝ f : Ordinal.{u} → Ordinal.{u}
⊢ (fun a => sup fun n => f^[n] a) = nfp f
[PROOFSTEP]
refine' funext fun a => le_antisymm _ (sup_le fun l => _)
[GOAL]
case refine'_1
f✝ f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ (sup fun n => f^[n] a) ≤ nfp f a
[PROOFSTEP]
rw [sup_le_iff]
[GOAL]
case refine'_1
f✝ f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a
[PROOFSTEP]
intro n
[GOAL]
case refine'_1
f✝ f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ f^[n] a ≤ nfp f a
[PROOFSTEP]
rw [← List.length_replicate n Unit.unit, ← List.foldr_const f a]
[GOAL]
case refine'_1
f✝ f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun x => f) a (List.replicate n ()) ≤ nfp f a
[PROOFSTEP]
apply le_sup
[GOAL]
case refine'_2
f✝ f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ List.foldr (fun x => f) a l ≤ sup fun n => f^[n] a
[PROOFSTEP]
rw [List.foldr_const f a l]
[GOAL]
case refine'_2
f✝ f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[List.length l] a ≤ sup fun n => f^[n] a
[PROOFSTEP]
exact le_sup _ _
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ nfp f a
[PROOFSTEP]
rw [← sup_iterate_eq_nfp]
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ (fun a => sup fun n => f^[n] a) a
[PROOFSTEP]
exact le_sup _ n
[GOAL]
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < nfp f b ↔ ∃ n, a < f^[n] b
[PROOFSTEP]
rw [← sup_iterate_eq_nfp]
[GOAL]
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < (fun a => sup fun n => f^[n] a) b ↔ ∃ n, a < f^[n] b
[PROOFSTEP]
exact lt_sup
[GOAL]
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
[PROOFSTEP]
rw [← sup_iterate_eq_nfp]
[GOAL]
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ (fun a => sup fun n => f^[n] a) a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
[PROOFSTEP]
exact sup_le_iff
[GOAL]
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u_1}
⊢ nfp id a = id a
[PROOFSTEP]
simp_rw [← sup_iterate_eq_nfp, iterate_id]
[GOAL]
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u_1}
⊢ (sup fun n => id a) = id a
[PROOFSTEP]
exact sup_const a
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
H : IsNormal f
a b : Ordinal.{u_1}
⊢ f b < nfp f a ↔ b < nfp f a
[PROOFSTEP]
unfold nfp
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
H : IsNormal f
a b : Ordinal.{u_1}
⊢ f b < nfpFamily (fun x => f) a ↔ b < nfpFamily (fun x => f) a
[PROOFSTEP]
rw [← @apply_lt_nfpFamily_iff Unit (fun _ => f) _ (fun _ => H) a b]
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
H : IsNormal f
a b : Ordinal.{u_1}
⊢ f b < nfpFamily (fun x => f) a ↔ Unit → f b < nfpFamily (fun x => f) a
[PROOFSTEP]
exact ⟨fun h _ => h, fun h => h Unit.unit⟩
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
H : IsNormal f
a b : Ordinal.{u_1}
h : b ≤ nfp f a
⊢ f b ≤ nfp f a
[PROOFSTEP]
simpa only [H.nfp_fp] using H.le_iff.2 h
[GOAL]
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ Set.Unbounded (fun x x_1 => x < x_1) (fixedPoints f)
[PROOFSTEP]
convert fp_family_unbounded fun _ : Unit => H
[GOAL]
case h.e'_3
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ (i : Unit), fixedPoints f
[PROOFSTEP]
exact (Set.iInter_const _).symm
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
h : nfp f = id
⊢ deriv f 0 = id 0 ∧ ∀ (a : Ordinal.{u_1}), deriv f a = id a → deriv f (succ a) = id (succ a)
[PROOFSTEP]
simp [h]
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
H : IsNormal f
a : Ordinal.{u_1}
⊢ f a ≤ a ↔ ∃ o, deriv f o = a
[PROOFSTEP]
unfold deriv
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
H : IsNormal f
a : Ordinal.{u_1}
⊢ f a ≤ a ↔ ∃ o, derivFamily (fun x => f) o = a
[PROOFSTEP]
rw [← le_iff_derivFamily fun _ : Unit => H]
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
H : IsNormal f
a : Ordinal.{u_1}
⊢ f a ≤ a ↔ Unit → f a ≤ a
[PROOFSTEP]
exact ⟨fun h _ => h, fun h => h Unit.unit⟩
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
H : IsNormal f
a : Ordinal.{u_1}
⊢ f a = a ↔ ∃ o, deriv f o = a
[PROOFSTEP]
rw [← H.le_iff_eq, H.le_iff_deriv]
[GOAL]
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ deriv f = enumOrd (fixedPoints f)
[PROOFSTEP]
convert derivFamily_eq_enumOrd fun _ : Unit => H
[GOAL]
case h.e'_3.h.e'_1
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ (i : Unit), fixedPoints f
[PROOFSTEP]
exact (Set.iInter_const _).symm
[GOAL]
f✝ : Ordinal.{u} → Ordinal.{u}
f : Ordinal.{u_1} → Ordinal.{u_1}
h : nfp f = id
⊢ deriv f 0 = id 0 ∧ ∀ (a : Ordinal.{u_1}), deriv f a = id a → deriv f (succ a) = id (succ a)
[PROOFSTEP]
simp [h]
[GOAL]
a : Ordinal.{u_1}
⊢ nfp (fun x => a + x) 0 = a * ω
[PROOFSTEP]
simp_rw [← sup_iterate_eq_nfp, ← sup_mul_nat]
[GOAL]
a : Ordinal.{u_1}
⊢ (sup fun n => (fun x => a + x)^[n] 0) = sup fun n => a * ↑n
[PROOFSTEP]
congr
[GOAL]
case e_f
a : Ordinal.{u_1}
⊢ (fun n => (fun x => a + x)^[n] 0) = fun n => a * ↑n
[PROOFSTEP]
funext n
[GOAL]
case e_f.h
a : Ordinal.{u_1}
n : ℕ
⊢ (fun x => a + x)^[n] 0 = a * ↑n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case e_f.h.zero
a : Ordinal.{u_1}
⊢ (fun x => a + x)^[Nat.zero] 0 = a * ↑Nat.zero
[PROOFSTEP]
rw [Nat.cast_zero, mul_zero, iterate_zero_apply]
[GOAL]
case e_f.h.succ
a : Ordinal.{u_1}
n : ℕ
hn : (fun x => a + x)^[n] 0 = a * ↑n
⊢ (fun x => a + x)^[Nat.succ n] 0 = a * ↑(Nat.succ n)
[PROOFSTEP]
nth_rw 2 [Nat.succ_eq_one_add]
[GOAL]
case e_f.h.succ
a : Ordinal.{u_1}
n : ℕ
hn : (fun x => a + x)^[n] 0 = a * ↑n
⊢ (fun x => a + x)^[Nat.succ n] 0 = a * ↑(1 + n)
[PROOFSTEP]
rw [Nat.cast_add, Nat.cast_one, mul_one_add, iterate_succ_apply', hn]
[GOAL]
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x => a + x) b = a * ω
[PROOFSTEP]
apply le_antisymm (nfp_le_fp (add_isNormal a).monotone hba _)
[GOAL]
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * ω ≤ nfp ((fun x x_1 => x + x_1) a) b
[PROOFSTEP]
rw [← nfp_add_zero]
[GOAL]
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x => a + x) 0 ≤ nfp ((fun x x_1 => x + x_1) a) b
[PROOFSTEP]
exact nfp_monotone (add_isNormal a).monotone (Ordinal.zero_le b)
[GOAL]
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ (fun x x_1 => x + x_1) a (a * ω) ≤ a * ω
[PROOFSTEP]
dsimp
[GOAL]
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω
[PROOFSTEP]
rw [← mul_one_add, one_add_omega]
[GOAL]
a b : Ordinal.{u_1}
⊢ a + b = b ↔ a * ω ≤ b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ a * ω ≤ b
[PROOFSTEP]
rw [← nfp_add_zero a, ← deriv_zero]
[GOAL]
case refine'_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ deriv (fun x => a + x) 0 ≤ b
[PROOFSTEP]
cases' (add_isNormal a).fp_iff_deriv.1 h with c hc
[GOAL]
case refine'_1.intro
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv ((fun x x_1 => x + x_1) a) c = b
⊢ deriv (fun x => a + x) 0 ≤ b
[PROOFSTEP]
rw [← hc]
[GOAL]
case refine'_1.intro
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv ((fun x x_1 => x + x_1) a) c = b
⊢ deriv (fun x => a + x) 0 ≤ deriv ((fun x x_1 => x + x_1) a) c
[PROOFSTEP]
exact (deriv_isNormal _).monotone (Ordinal.zero_le _)
[GOAL]
case refine'_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
⊢ a + b = b
[PROOFSTEP]
have := Ordinal.add_sub_cancel_of_le h
[GOAL]
case refine'_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + b = b
[PROOFSTEP]
nth_rw 1 [← this]
[GOAL]
case refine'_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b
[PROOFSTEP]
rwa [← add_assoc, ← mul_one_add, one_add_omega]
[GOAL]
a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a * ω ≤ b
[PROOFSTEP]
rw [← add_eq_right_iff_mul_omega_le]
[GOAL]
a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a + b = b
[PROOFSTEP]
exact (add_isNormal a).le_iff_eq
[GOAL]
a b : Ordinal.{u}
⊢ deriv (fun x => a + x) b = a * ω + b
[PROOFSTEP]
revert b
[GOAL]
a : Ordinal.{u}
⊢ ∀ (b : Ordinal.{u}), deriv (fun x => a + x) b = a * ω + b
[PROOFSTEP]
rw [← funext_iff, IsNormal.eq_iff_zero_and_succ (deriv_isNormal _) (add_isNormal _)]
[GOAL]
a : Ordinal.{u}
⊢ deriv (fun x => a + x) 0 = (fun x x_1 => x + x_1) (a * ω) 0 ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun x => a + x) a_1 = (fun x x_1 => x + x_1) (a * ω) a_1 →
        deriv (fun x => a + x) (succ a_1) = (fun x x_1 => x + x_1) (a * ω) (succ a_1)
[PROOFSTEP]
refine' ⟨_, fun a h => _⟩
[GOAL]
case refine'_1
a : Ordinal.{u}
⊢ deriv (fun x => a + x) 0 = (fun x x_1 => x + x_1) (a * ω) 0
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
a : Ordinal.{u}
⊢ deriv (fun x => a + x) 0 = a * ω + 0
[PROOFSTEP]
rw [deriv_zero, add_zero]
[GOAL]
case refine'_1
a : Ordinal.{u}
⊢ nfp (fun x => a + x) 0 = a * ω
[PROOFSTEP]
exact nfp_add_zero a
[GOAL]
case refine'_2
a✝ a : Ordinal.{u}
h : deriv (fun x => a✝ + x) a = (fun x x_1 => x + x_1) (a✝ * ω) a
⊢ deriv (fun x => a✝ + x) (succ a) = (fun x x_1 => x + x_1) (a✝ * ω) (succ a)
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
a✝ a : Ordinal.{u}
h : deriv (fun x => a✝ + x) a = (fun x x_1 => x + x_1) (a✝ * ω) a
⊢ deriv (fun x => a✝ + x) (succ a) = a✝ * ω + succ a
[PROOFSTEP]
rw [deriv_succ, h, add_succ]
[GOAL]
case refine'_2
a✝ a : Ordinal.{u}
h : deriv (fun x => a✝ + x) a = (fun x x_1 => x + x_1) (a✝ * ω) a
⊢ nfp (fun x => a✝ + x) (succ ((fun x x_1 => x + x_1) (a✝ * ω) a)) = succ (a✝ * ω + a)
[PROOFSTEP]
exact nfp_eq_self (add_eq_right_iff_mul_omega_le.2 ((le_add_right _ _).trans (le_succ _)))
[GOAL]
a : Ordinal.{u_1}
ha : 0 < a
⊢ nfp (fun x => a * x) 1 = a ^ ω
[PROOFSTEP]
rw [← sup_iterate_eq_nfp, ← sup_opow_nat]
[GOAL]
a : Ordinal.{u_1}
ha : 0 < a
⊢ (fun a_1 => sup fun n => (fun x => a * x)^[n] a_1) 1 = sup fun n => a ^ ↑n
[PROOFSTEP]
dsimp
[GOAL]
a : Ordinal.{u_1}
ha : 0 < a
⊢ (sup fun n => (fun x => a * x)^[n] 1) = sup fun n => a ^ ↑n
[PROOFSTEP]
congr
[GOAL]
case e_f
a : Ordinal.{u_1}
ha : 0 < a
⊢ (fun n => (fun x => a * x)^[n] 1) = fun n => a ^ ↑n
[PROOFSTEP]
funext n
[GOAL]
case e_f.h
a : Ordinal.{u_1}
ha : 0 < a
n : ℕ
⊢ (fun x => a * x)^[n] 1 = a ^ ↑n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case e_f.h.zero
a : Ordinal.{u_1}
ha : 0 < a
⊢ (fun x => a * x)^[Nat.zero] 1 = a ^ ↑Nat.zero
[PROOFSTEP]
rw [Nat.cast_zero, opow_zero, iterate_zero_apply]
[GOAL]
case e_f.h.succ
a : Ordinal.{u_1}
ha : 0 < a
n : ℕ
hn : (fun x => a * x)^[n] 1 = a ^ ↑n
⊢ (fun x => a * x)^[Nat.succ n] 1 = a ^ ↑(Nat.succ n)
[PROOFSTEP]
nth_rw 2 [Nat.succ_eq_one_add]
[GOAL]
case e_f.h.succ
a : Ordinal.{u_1}
ha : 0 < a
n : ℕ
hn : (fun x => a * x)^[n] 1 = a ^ ↑n
⊢ (fun x => a * x)^[Nat.succ n] 1 = a ^ ↑(1 + n)
[PROOFSTEP]
rw [Nat.cast_add, Nat.cast_one, opow_add, opow_one, iterate_succ_apply', hn]
[GOAL]
a : Ordinal.{u_1}
ha : 0 < a
⊢ 0 < a
[PROOFSTEP]
exact ha
[GOAL]
a : Ordinal.{u_1}
⊢ nfp (fun x => a * x) 0 = 0
[PROOFSTEP]
rw [← Ordinal.le_zero, nfp_le_iff]
[GOAL]
a : Ordinal.{u_1}
⊢ ∀ (n : ℕ), (fun x => a * x)^[n] 0 ≤ 0
[PROOFSTEP]
intro n
[GOAL]
a : Ordinal.{u_1}
n : ℕ
⊢ (fun x => a * x)^[n] 0 ≤ 0
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
a : Ordinal.{u_1}
⊢ (fun x => a * x)^[Nat.zero] 0 ≤ 0
[PROOFSTEP]
rfl
[GOAL]
case succ
a : Ordinal.{u_1}
n : ℕ
hn : (fun x => a * x)^[n] 0 ≤ 0
⊢ (fun x => a * x)^[Nat.succ n] 0 ≤ 0
[PROOFSTEP]
dsimp only
[GOAL]
case succ
a : Ordinal.{u_1}
n : ℕ
hn : (fun x => a * x)^[n] 0 ≤ 0
⊢ (fun x => a * x)^[Nat.succ n] 0 ≤ 0
[PROOFSTEP]
rwa [iterate_succ_apply, mul_zero]
[GOAL]
⊢ nfp (HMul.hMul 0) = id
[PROOFSTEP]
rw [← sup_iterate_eq_nfp]
[GOAL]
⊢ (fun a => sup fun n => (HMul.hMul 0)^[n] a) = id
[PROOFSTEP]
refine' funext fun a => (sup_le fun n => _).antisymm (le_sup (fun n => (0 * ·)^[n] a) 0)
[GOAL]
a : Ordinal.{u_1}
n : ℕ
⊢ (HMul.hMul 0)^[n] a ≤ id a
[PROOFSTEP]
induction' n with n _
[GOAL]
case zero
a : Ordinal.{u_1}
⊢ (HMul.hMul 0)^[Nat.zero] a ≤ id a
[PROOFSTEP]
rfl
[GOAL]
case succ
a : Ordinal.{u_1}
n : ℕ
n_ih✝ : (HMul.hMul 0)^[n] a ≤ id a
⊢ (HMul.hMul 0)^[Nat.succ n] a ≤ id a
[PROOFSTEP]
rw [Function.iterate_succ']
[GOAL]
case succ
a : Ordinal.{u_1}
n : ℕ
n_ih✝ : (HMul.hMul 0)^[n] a ≤ id a
⊢ (HMul.hMul 0 ∘ (HMul.hMul 0)^[n]) a ≤ id a
[PROOFSTEP]
change 0 * _ ≤ a
[GOAL]
case succ
a : Ordinal.{u_1}
n : ℕ
n_ih✝ : (HMul.hMul 0)^[n] a ≤ id a
⊢ 0 * (HMul.hMul 0)^[n] a ≤ a
[PROOFSTEP]
rw [zero_mul]
[GOAL]
case succ
a : Ordinal.{u_1}
n : ℕ
n_ih✝ : (HMul.hMul 0)^[n] a ≤ id a
⊢ 0 ≤ a
[PROOFSTEP]
exact Ordinal.zero_le a
[GOAL]
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ a ^ ω
⊢ nfp (fun x => a * x) b = a ^ ω
[PROOFSTEP]
cases' eq_zero_or_pos a with ha ha
[GOAL]
case inl
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ a ^ ω
ha : a = 0
⊢ nfp (fun x => a * x) b = a ^ ω
[PROOFSTEP]
rw [ha, zero_opow omega_ne_zero] at hba ⊢
[GOAL]
case inl
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ nfp (fun x => 0 * x) b = 0
[PROOFSTEP]
rw [Ordinal.le_zero.1 hba, nfp_zero_mul]
[GOAL]
case inl
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ id 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case inr
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b = a ^ ω
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.a
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b ≤ a ^ ω
[PROOFSTEP]
apply nfp_le_fp (mul_isNormal ha).monotone hba
[GOAL]
case inr.a
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ (fun x x_1 => x * x_1) a (a ^ ω) ≤ a ^ ω
[PROOFSTEP]
dsimp only
[GOAL]
case inr.a
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a * a ^ ω ≤ a ^ ω
[PROOFSTEP]
rw [← opow_one_add, one_add_omega]
[GOAL]
case inr.a
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ nfp (fun x => a * x) b
[PROOFSTEP]
rw [← nfp_mul_one ha]
[GOAL]
case inr.a
a b : Ordinal.{u}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) 1 ≤ nfp (fun x => a * x) b
[PROOFSTEP]
exact nfp_monotone (mul_isNormal ha).monotone (one_le_iff_pos.2 hb)
[GOAL]
a b : Ordinal.{u}
hab : a * b = b
⊢ b = 0 ∨ a ^ ω ≤ b
[PROOFSTEP]
cases' eq_zero_or_pos a with ha ha
[GOAL]
case inl
a b : Ordinal.{u}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b
[PROOFSTEP]
rw [ha, zero_opow omega_ne_zero]
[GOAL]
case inl
a b : Ordinal.{u}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b
[PROOFSTEP]
exact Or.inr (Ordinal.zero_le b)
[GOAL]
case inr
a b : Ordinal.{u}
hab : a * b = b
ha : 0 < a
⊢ b = 0 ∨ a ^ ω ≤ b
[PROOFSTEP]
rw [or_iff_not_imp_left]
[GOAL]
case inr
a b : Ordinal.{u}
hab : a * b = b
ha : 0 < a
⊢ ¬b = 0 → a ^ ω ≤ b
[PROOFSTEP]
intro hb
[GOAL]
case inr
a b : Ordinal.{u}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ a ^ ω ≤ b
[PROOFSTEP]
rw [← nfp_mul_one ha]
[GOAL]
case inr
a b : Ordinal.{u}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x => a * x) 1 ≤ b
[PROOFSTEP]
rw [← Ne.def, ← one_le_iff_ne_zero] at hb 
[GOAL]
case inr
a b : Ordinal.{u}
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun x => a * x) 1 ≤ b
[PROOFSTEP]
exact nfp_le_fp (mul_isNormal ha).monotone hb (le_of_eq hab)
[GOAL]
a b : Ordinal.{u_1}
⊢ a * b = b ↔ a ^ ω ∣ b
[PROOFSTEP]
cases' eq_zero_or_pos a with ha ha
[GOAL]
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ a * b = b ↔ a ^ ω ∣ b
[PROOFSTEP]
rw [ha, zero_mul, zero_opow omega_ne_zero, zero_dvd_iff]
[GOAL]
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 = b ↔ b = 0
[PROOFSTEP]
exact eq_comm
[GOAL]
case inr
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b = b ↔ a ^ ω ∣ b
[PROOFSTEP]
refine' ⟨fun hab => _, fun h => _⟩
[GOAL]
case inr.refine'_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ a ^ ω ∣ b
[PROOFSTEP]
rw [dvd_iff_mod_eq_zero]
[GOAL]
case inr.refine'_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0
[PROOFSTEP]
rw [← div_add_mod b (a ^ omega), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega, add_left_cancel] at hab 
[GOAL]
case inr.refine'_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0
[PROOFSTEP]
cases' eq_zero_or_opow_omega_le_of_mul_eq_right hab with hab hab
[GOAL]
case inr.refine'_1.inl
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : b % a ^ ω = 0
⊢ b % a ^ ω = 0
[PROOFSTEP]
exact hab
[GOAL]
case inr.refine'_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ b % a ^ ω = 0
[PROOFSTEP]
refine' (not_lt_of_le hab (mod_lt b (opow_ne_zero omega _))).elim
[GOAL]
case inr.refine'_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ a ≠ 0
[PROOFSTEP]
rwa [← Ordinal.pos_iff_ne_zero]
[GOAL]
case inr.refine'_2
a b : Ordinal.{u_1}
ha : 0 < a
h : a ^ ω ∣ b
⊢ a * b = b
[PROOFSTEP]
cases' h with c hc
[GOAL]
case inr.refine'_2.intro
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a * b = b
[PROOFSTEP]
rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega]
[GOAL]
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a ^ ω ∣ b
[PROOFSTEP]
rw [← mul_eq_right_iff_opow_omega_dvd]
[GOAL]
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b
[PROOFSTEP]
exact (mul_isNormal ha).le_iff_eq
[GOAL]
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * succ b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x => a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b
[PROOFSTEP]
apply nfp_le_fp (mul_isNormal ha).monotone
[GOAL]
case a.ab
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * succ b
[PROOFSTEP]
rw [mul_succ]
[GOAL]
case a.ab
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω
[PROOFSTEP]
apply add_le_add_left hca
[GOAL]
case a.h
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ (fun x x_1 => x * x_1) a (a ^ ω * succ b) ≤ a ^ ω * succ b
[PROOFSTEP]
dsimp only
[GOAL]
case a.h
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a * (a ^ ω * succ b) ≤ a ^ ω * succ b
[PROOFSTEP]
rw [← mul_assoc, ← opow_one_add, one_add_omega]
[GOAL]
case a
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)
[PROOFSTEP]
cases' mul_eq_right_iff_opow_omega_dvd.1 ((mul_isNormal ha).nfp_fp ((a ^ omega) * b + c)) with d hd
[GOAL]
case a.intro
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u}
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)
[PROOFSTEP]
rw [hd]
[GOAL]
case a.intro
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u}
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ a ^ ω * d
[PROOFSTEP]
apply mul_le_mul_left'
[GOAL]
case a.intro.bc
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u}
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
⊢ succ b ≤ d
[PROOFSTEP]
have := le_nfp (Mul.mul a) ((a ^ omega) * b + c)
[GOAL]
case a.intro.bc
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u}
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ nfp (Mul.mul a) (a ^ ω * b + c)
⊢ succ b ≤ d
[PROOFSTEP]
erw [hd] at this 
[GOAL]
case a.intro.bc
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u}
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ a ^ ω * d
⊢ succ b ≤ d
[PROOFSTEP]
have := (add_lt_add_left hc ((a ^ omega) * b)).trans_le this
[GOAL]
case a.intro.bc
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u}
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b + 0 < a ^ ω * d
⊢ succ b ≤ d
[PROOFSTEP]
rw [add_zero, mul_lt_mul_iff_left (opow_pos omega ha)] at this 
[GOAL]
case a.intro.bc
a c b : Ordinal.{u}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u}
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ succ b ≤ d
[PROOFSTEP]
rwa [succ_le_iff]
[GOAL]
a : Ordinal.{u}
ha : 0 < a
b : Ordinal.{u}
⊢ deriv (fun x => a * x) b = a ^ ω * b
[PROOFSTEP]
revert b
[GOAL]
a : Ordinal.{u}
ha : 0 < a
⊢ ∀ (b : Ordinal.{u}), deriv (fun x => a * x) b = a ^ ω * b
[PROOFSTEP]
rw [← funext_iff, IsNormal.eq_iff_zero_and_succ (deriv_isNormal _) (mul_isNormal (opow_pos omega ha))]
[GOAL]
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = (fun x x_1 => x * x_1) (a ^ ω) 0 ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun x => a * x) a_1 = (fun x x_1 => x * x_1) (a ^ ω) a_1 →
        deriv (fun x => a * x) (succ a_1) = (fun x x_1 => x * x_1) (a ^ ω) (succ a_1)
[PROOFSTEP]
refine' ⟨_, fun c h => _⟩
[GOAL]
case refine'_1
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = (fun x x_1 => x * x_1) (a ^ ω) 0
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_1
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = a ^ ω * 0
[PROOFSTEP]
rw [deriv_zero, nfp_mul_zero, mul_zero]
[GOAL]
case refine'_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x => a * x) c = (fun x x_1 => x * x_1) (a ^ ω) c
⊢ deriv (fun x => a * x) (succ c) = (fun x x_1 => x * x_1) (a ^ ω) (succ c)
[PROOFSTEP]
rw [deriv_succ, h]
[GOAL]
case refine'_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x => a * x) c = (fun x x_1 => x * x_1) (a ^ ω) c
⊢ nfp (fun x => a * x) (succ ((fun x x_1 => x * x_1) (a ^ ω) c)) = (fun x x_1 => x * x_1) (a ^ ω) (succ c)
[PROOFSTEP]
exact nfp_mul_opow_omega_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))
