[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))


[GOAL]
a : Ordinal.{u_1}
⊢ 0 ^ a = 1 - a
[PROOFSTEP]
simp only [opow_def, if_true]
[GOAL]
a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ 0 ^ a = 0
[PROOFSTEP]
rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero]
[GOAL]
a : Ordinal.{u_1}
⊢ a ^ 0 = 1
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
a : Ordinal.{u_1}
h : a = 0
⊢ a ^ 0 = 1
[PROOFSTEP]
simp only [opow_def, if_pos h, sub_zero]
[GOAL]
case neg
a : Ordinal.{u_1}
h : ¬a = 0
⊢ a ^ 0 = 1
[PROOFSTEP]
simp only [opow_def, if_neg h, limitRecOn_zero]
[GOAL]
a b : Ordinal.{u_1}
h : a = 0
⊢ a ^ succ b = a ^ b * a
[PROOFSTEP]
subst a
[GOAL]
b : Ordinal.{u_1}
⊢ 0 ^ succ b = 0 ^ b * 0
[PROOFSTEP]
simp only [zero_opow (succ_ne_zero _), mul_zero]
[GOAL]
a b : Ordinal.{u_1}
h : ¬a = 0
⊢ a ^ succ b = a ^ b * a
[PROOFSTEP]
simp only [opow_def, limitRecOn_succ, if_neg h]
[GOAL]
a b : Ordinal.{u}
a0 : a ≠ 0
h : IsLimit b
⊢ a ^ b = bsup b fun c x => a ^ c
[PROOFSTEP]
simp only [opow_def, if_neg a0]
[GOAL]
a b : Ordinal.{u}
a0 : a ≠ 0
h : IsLimit b
⊢ (limitRecOn b 1 (fun x IH => IH * a) fun b x => bsup b) =
    bsup b fun c x => limitRecOn c 1 (fun x IH => IH * a) fun b x => bsup b
[PROOFSTEP]
rw [limitRecOn_limit _ _ _ _ h]
[GOAL]
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsLimit b
⊢ a ^ b ≤ c ↔ ∀ (b' : Ordinal.{u_1}), b' < b → a ^ b' ≤ c
[PROOFSTEP]
rw [opow_limit a0 h, bsup_le_iff]
[GOAL]
a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : IsLimit c
⊢ a < b ^ c ↔ ∃ c', c' < c ∧ a < b ^ c'
[PROOFSTEP]
rw [← not_iff_not, not_exists]
[GOAL]
a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : IsLimit c
⊢ ¬a < b ^ c ↔ ∀ (x : Ordinal.{u_1}), ¬(x < c ∧ a < b ^ x)
[PROOFSTEP]
simp only [not_lt, opow_le_of_limit b0 h, exists_prop, not_and]
[GOAL]
a : Ordinal.{u_1}
⊢ a ^ 1 = a
[PROOFSTEP]
rw [← succ_zero, opow_succ]
[GOAL]
a : Ordinal.{u_1}
⊢ a ^ 0 * a = a
[PROOFSTEP]
simp only [opow_zero, one_mul]
[GOAL]
a : Ordinal.{u_1}
⊢ 1 ^ a = 1
[PROOFSTEP]
induction a using limitRecOn with
| H₁ => simp only [opow_zero]
| H₂ _ ih => simp only [opow_succ, ih, mul_one]
| H₃ b l IH =>
  refine' eq_of_forall_ge_iff fun c => _
  rw [opow_le_of_limit Ordinal.one_ne_zero l]
  exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩
[GOAL]
a : Ordinal.{u_1}
⊢ 1 ^ a = 1
[PROOFSTEP]
induction a using limitRecOn with
| H₁ => simp only [opow_zero]
| H₂ _ ih => simp only [opow_succ, ih, mul_one]
| H₃ b l IH =>
  refine' eq_of_forall_ge_iff fun c => _
  rw [opow_le_of_limit Ordinal.one_ne_zero l]
  exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩
[GOAL]
case H₁
⊢ 1 ^ 0 = 1
[PROOFSTEP]

| H₁ => simp only [opow_zero]
[GOAL]
case H₁
⊢ 1 ^ 0 = 1
[PROOFSTEP]
simp only [opow_zero]
[GOAL]
case H₂
o✝ : Ordinal.{u_1}
ih : 1 ^ o✝ = 1
⊢ 1 ^ succ o✝ = 1
[PROOFSTEP]

| H₂ _ ih => simp only [opow_succ, ih, mul_one]
[GOAL]
case H₂
o✝ : Ordinal.{u_1}
ih : 1 ^ o✝ = 1
⊢ 1 ^ succ o✝ = 1
[PROOFSTEP]
simp only [opow_succ, ih, mul_one]
[GOAL]
case H₃
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
⊢ 1 ^ b = 1
[PROOFSTEP]

| H₃ b l IH =>
  refine' eq_of_forall_ge_iff fun c => _
  rw [opow_le_of_limit Ordinal.one_ne_zero l]
  exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩
[GOAL]
case H₃
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
⊢ 1 ^ b = 1
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun c => _
[GOAL]
case H₃
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ 1 ^ b ≤ c ↔ 1 ≤ c
[PROOFSTEP]
rw [opow_le_of_limit Ordinal.one_ne_zero l]
[GOAL]
case H₃
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ (∀ (b' : Ordinal.{u_1}), b' < b → 1 ^ b' ≤ c) ↔ 1 ≤ c
[PROOFSTEP]
exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩
[GOAL]
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
c : Ordinal.{u_1}
H : ∀ (b' : Ordinal.{u_1}), b' < b → 1 ^ b' ≤ c
⊢ 1 ≤ c
[PROOFSTEP]
simpa only [opow_zero] using H 0 l.pos
[GOAL]
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
c : Ordinal.{u_1}
H : 1 ≤ c
b' : Ordinal.{u_1}
h : b' < b
⊢ 1 ^ b' ≤ c
[PROOFSTEP]
rwa [IH _ h]
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ b
[PROOFSTEP]
have h0 : 0 < (a ^ 0) := by simp only [opow_zero, zero_lt_one]
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ 0
[PROOFSTEP]
simp only [opow_zero, zero_lt_one]
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ b
[PROOFSTEP]
induction b using limitRecOn with
| H₁ => exact h0
| H₂ b IH =>
  rw [opow_succ]
  exact mul_pos IH a0
| H₃ b l _ => exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ b
[PROOFSTEP]
induction b using limitRecOn with
| H₁ => exact h0
| H₂ b IH =>
  rw [opow_succ]
  exact mul_pos IH a0
| H₃ b l _ => exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
[GOAL]
case H₁
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ 0
[PROOFSTEP]

| H₁ => exact h0
[GOAL]
case H₁
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ 0
[PROOFSTEP]
exact h0
[GOAL]
case H₂
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ succ b
[PROOFSTEP]

| H₂ b IH =>
  rw [opow_succ]
  exact mul_pos IH a0
[GOAL]
case H₂
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ succ b
[PROOFSTEP]
rw [opow_succ]
[GOAL]
case H₂
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ b * a
[PROOFSTEP]
exact mul_pos IH a0
[GOAL]
case H₃
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
l : IsLimit b
a✝ : ∀ (o' : Ordinal.{u_1}), o' < b → 0 < a ^ o'
⊢ 0 < a ^ b
[PROOFSTEP]

| H₃ b l _ => exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
[GOAL]
case H₃
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
l : IsLimit b
a✝ : ∀ (o' : Ordinal.{u_1}), o' < b → 0 < a ^ o'
⊢ 0 < a ^ b
[PROOFSTEP]
exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
[GOAL]
a : Ordinal.{u_1}
h : 1 < a
a0 : 0 < a
b : Ordinal.{u_1}
⊢ (fun x x_1 => x ^ x_1) a b < (fun x x_1 => x ^ x_1) a (succ b)
[PROOFSTEP]
simpa only [mul_one, opow_succ] using (mul_lt_mul_iff_left (opow_pos b a0)).2 h
[GOAL]
a b : Ordinal.{u_1}
l : IsLimit a
hb : b ≠ 0
⊢ IsLimit (a ^ b)
[PROOFSTEP]
rcases zero_or_succ_or_limit b with (e | ⟨b, rfl⟩ | l')
[GOAL]
case inl
a b : Ordinal.{u_1}
l : IsLimit a
hb : b ≠ 0
e : b = 0
⊢ IsLimit (a ^ b)
[PROOFSTEP]
exact absurd e hb
[GOAL]
case inr.inl.intro
a : Ordinal.{u_1}
l : IsLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsLimit (a ^ succ b)
[PROOFSTEP]
rw [opow_succ]
[GOAL]
case inr.inl.intro
a : Ordinal.{u_1}
l : IsLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsLimit (a ^ b * a)
[PROOFSTEP]
exact mul_isLimit (opow_pos _ l.pos) l
[GOAL]
case inr.inr
a b : Ordinal.{u_1}
l : IsLimit a
hb : b ≠ 0
l' : IsLimit b
⊢ IsLimit (a ^ b)
[PROOFSTEP]
exact opow_isLimit l.one_lt l'
[GOAL]
a b c : Ordinal.{u_1}
h₁ : 0 < a
h₂ : b ≤ c
⊢ a ^ b ≤ a ^ c
[PROOFSTEP]
cases' lt_or_eq_of_le (one_le_iff_pos.2 h₁) with h₁ h₁
[GOAL]
case inl
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c
[PROOFSTEP]
exact (opow_le_opow_iff_right h₁).2 h₂
[GOAL]
case inr
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 = a
⊢ a ^ b ≤ a ^ c
[PROOFSTEP]
subst a
[GOAL]
case inr
b c : Ordinal.{u_1}
h₂ : b ≤ c
h₁ : 0 < 1
⊢ 1 ^ b ≤ 1 ^ c
[PROOFSTEP]
simp only [one_opow, le_refl]
[GOAL]
a b c : Ordinal.{u_1}
ab : a ≤ b
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
by_cases a0 :
  a =
    0
      -- Porting note: `le_refl` is required.
[GOAL]
case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : a = 0
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
subst a
[GOAL]
case pos
b c : Ordinal.{u_1}
ab : 0 ≤ b
⊢ 0 ^ c ≤ b ^ c
[PROOFSTEP]
by_cases c0 : c = 0
[GOAL]
case pos
b c : Ordinal.{u_1}
ab : 0 ≤ b
c0 : c = 0
⊢ 0 ^ c ≤ b ^ c
[PROOFSTEP]
subst c
[GOAL]
case pos
b : Ordinal.{u_1}
ab : 0 ≤ b
⊢ 0 ^ 0 ≤ b ^ 0
[PROOFSTEP]
simp only [opow_zero, le_refl]
[GOAL]
case neg
b c : Ordinal.{u_1}
ab : 0 ≤ b
c0 : ¬c = 0
⊢ 0 ^ c ≤ b ^ c
[PROOFSTEP]
simp only [zero_opow c0, Ordinal.zero_le]
[GOAL]
case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
induction c using limitRecOn with
| H₁ => simp only [opow_zero, le_refl]
| H₂ c IH => simpa only [opow_succ] using mul_le_mul' IH ab
| H₃ c l IH =>
  exact
    (opow_le_of_limit a0 l).2 fun b' h =>
      (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le)
[GOAL]
case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
induction c using limitRecOn with
| H₁ => simp only [opow_zero, le_refl]
| H₂ c IH => simpa only [opow_succ] using mul_le_mul' IH ab
| H₃ c l IH =>
  exact
    (opow_le_of_limit a0 l).2 fun b' h =>
      (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le)
[GOAL]
case neg.H₁
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ 0 ≤ b ^ 0
[PROOFSTEP]

| H₁ => simp only [opow_zero, le_refl]
[GOAL]
case neg.H₁
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ 0 ≤ b ^ 0
[PROOFSTEP]
simp only [opow_zero, le_refl]
[GOAL]
case neg.H₂
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
IH : a ^ c ≤ b ^ c
⊢ a ^ succ c ≤ b ^ succ c
[PROOFSTEP]

| H₂ c IH => simpa only [opow_succ] using mul_le_mul' IH ab
[GOAL]
case neg.H₂
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
IH : a ^ c ≤ b ^ c
⊢ a ^ succ c ≤ b ^ succ c
[PROOFSTEP]
simpa only [opow_succ] using mul_le_mul' IH ab
[GOAL]
case neg.H₃
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ o' ≤ b ^ o'
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]

| H₃ c l IH =>
  exact
    (opow_le_of_limit a0 l).2 fun b' h =>
      (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le)
[GOAL]
case neg.H₃
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ o' ≤ b ^ o'
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
exact
  (opow_le_of_limit a0 l).2 fun b' h =>
    (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le)
[GOAL]
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ≤ a ^ b
[PROOFSTEP]
nth_rw 1 [← opow_one a]
[GOAL]
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
cases' le_or_gt a 1 with a1 a1
[GOAL]
case inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
cases' lt_or_eq_of_le a1 with a0 a1
[GOAL]
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
rw [lt_one_iff_zero] at a0
[GOAL]
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
rw [a0, zero_opow Ordinal.one_ne_zero]
[GOAL]
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b
[PROOFSTEP]
exact Ordinal.zero_le _
[GOAL]
case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
rw [a1, one_opow, one_opow]
[GOAL]
case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a > 1
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
rwa [opow_le_opow_iff_right a1, one_le_iff_pos]
[GOAL]
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ succ c < b ^ succ c
[PROOFSTEP]
rw [opow_succ, opow_succ]
[GOAL]
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c * a < b ^ c * b
[PROOFSTEP]
exact
  (mul_le_mul_right' (opow_le_opow_left c ab.le) a).trans_lt
    (mul_lt_mul_of_pos_left ab (opow_pos c ((Ordinal.zero_le a).trans_lt ab)))
[GOAL]
a b c : Ordinal.{u_1}
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | a0)
[GOAL]
case inl
b c : Ordinal.{u_1}
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | c0)
[GOAL]
case inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0
[PROOFSTEP]
simp
[GOAL]
case inl.inr
b c : Ordinal.{u_1}
c0 : c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
[PROOFSTEP]
have : b + c ≠ 0 := ((Ordinal.pos_iff_ne_zero.2 c0).trans_le (le_add_left _ _)).ne'
[GOAL]
case inl.inr
b c : Ordinal.{u_1}
c0 : c ≠ 0
this : b + c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
[PROOFSTEP]
simp only [zero_opow c0, zero_opow this, mul_zero]
[GOAL]
case inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
rcases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with (rfl | a1)
[GOAL]
case inr.inl
b c : Ordinal.{u_1}
a0 : 1 ≠ 0
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c
[PROOFSTEP]
simp only [one_opow, mul_one]
[GOAL]
case inr.inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
induction c using limitRecOn with
| H₁ => simp
| H₂ c IH => rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
|
  H₃ c l IH =>
  refine' eq_of_forall_ge_iff fun d => (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans (opow_isNormal a1)).limit_le l).symm
[GOAL]
case inr.inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
induction c using limitRecOn with
| H₁ => simp
| H₂ c IH => rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
|
  H₃ c l IH =>
  refine' eq_of_forall_ge_iff fun d => (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans (opow_isNormal a1)).limit_le l).symm
[GOAL]
case inr.inr.H₁
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + 0) = a ^ b * a ^ 0
[PROOFSTEP]

| H₁ => simp
[GOAL]
case inr.inr.H₁
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + 0) = a ^ b * a ^ 0
[PROOFSTEP]
simp
[GOAL]
case inr.inr.H₂
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + succ c) = a ^ b * a ^ succ c
[PROOFSTEP]

| H₂ c IH => rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
[GOAL]
case inr.inr.H₂
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + succ c) = a ^ b * a ^ succ c
[PROOFSTEP]
rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]

|
  H₃ c l IH =>
  refine' eq_of_forall_ge_iff fun d => (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans (opow_isNormal a1)).limit_le l).symm
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun d => (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → ((fun x x_1 => x ^ x_1) a ∘ (fun x x_1 => x + x_1) b) b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → a ^ (b + b_1) ≤ d) ↔ a ^ b * a ^ c ≤ d
[PROOFSTEP]
simp (config := { contextual := true }) only [IH]
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → a ^ b * a ^ b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d
[PROOFSTEP]
exact (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans (opow_isNormal a1)).limit_le l).symm
[GOAL]
a b : Ordinal.{u_1}
⊢ a ^ (1 + b) = a * a ^ b
[PROOFSTEP]
rw [opow_add, opow_one]
[GOAL]
a b c : Ordinal.{u_1}
h : b ≤ c
⊢ a ^ c = a ^ b * a ^ (c - b)
[PROOFSTEP]
rw [← opow_add, Ordinal.add_sub_cancel_of_le h]
[GOAL]
a b c : Ordinal.{u_1}
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
by_cases b0 : b = 0
[GOAL]
case pos
a b c : Ordinal.{u_1}
b0 : b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
simp only [b0, zero_mul, opow_zero, one_opow]
[GOAL]
case neg
a b c : Ordinal.{u_1}
b0 : ¬b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
by_cases a0 : a = 0
[GOAL]
case pos
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
subst a
[GOAL]
case pos
b c : Ordinal.{u_1}
b0 : ¬b = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
[PROOFSTEP]
by_cases c0 : c = 0
[GOAL]
case pos
b c : Ordinal.{u_1}
b0 : ¬b = 0
c0 : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
[PROOFSTEP]
simp only [c0, mul_zero, opow_zero]
[GOAL]
case neg
b c : Ordinal.{u_1}
b0 : ¬b = 0
c0 : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
[PROOFSTEP]
simp only [zero_opow b0, zero_opow c0, zero_opow (mul_ne_zero b0 c0)]
[GOAL]
case neg
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
cases' eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with a1 a1
[GOAL]
case neg.inl
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 = a
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
subst a1
[GOAL]
case neg.inl
b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬1 = 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c
[PROOFSTEP]
simp only [one_opow]
[GOAL]
case neg.inr
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
induction c using limitRecOn with
| H₁ => simp only [mul_zero, opow_zero]
| H₂ c IH => rw [mul_succ, opow_add, IH, opow_succ]
|
  H₃ c l IH =>
  refine'
    eq_of_forall_ge_iff fun d =>
      (((opow_isNormal a1).trans (mul_isNormal (Ordinal.pos_iff_ne_zero.2 b0))).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm
[GOAL]
case neg.inr
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
induction c using limitRecOn with
| H₁ => simp only [mul_zero, opow_zero]
| H₂ c IH => rw [mul_succ, opow_add, IH, opow_succ]
|
  H₃ c l IH =>
  refine'
    eq_of_forall_ge_iff fun d =>
      (((opow_isNormal a1).trans (mul_isNormal (Ordinal.pos_iff_ne_zero.2 b0))).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm
[GOAL]
case neg.inr.H₁
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * 0) = (a ^ b) ^ 0
[PROOFSTEP]

| H₁ => simp only [mul_zero, opow_zero]
[GOAL]
case neg.inr.H₁
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * 0) = (a ^ b) ^ 0
[PROOFSTEP]
simp only [mul_zero, opow_zero]
[GOAL]
case neg.inr.H₂
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * succ c) = (a ^ b) ^ succ c
[PROOFSTEP]

| H₂ c IH => rw [mul_succ, opow_add, IH, opow_succ]
[GOAL]
case neg.inr.H₂
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * succ c) = (a ^ b) ^ succ c
[PROOFSTEP]
rw [mul_succ, opow_add, IH, opow_succ]
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]

|
  H₃ c l IH =>
  refine'
    eq_of_forall_ge_iff fun d =>
      (((opow_isNormal a1).trans (mul_isNormal (Ordinal.pos_iff_ne_zero.2 b0))).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
refine'
  eq_of_forall_ge_iff fun d =>
    (((opow_isNormal a1).trans (mul_isNormal (Ordinal.pos_iff_ne_zero.2 b0))).limit_le l).trans _
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → ((fun x x_1 => x ^ x_1) a ∘ (fun x x_1 => x * x_1) b) b_1 ≤ d) ↔ (a ^ b) ^ c ≤ d
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → a ^ (b * b_1) ≤ d) ↔ (a ^ b) ^ c ≤ d
[PROOFSTEP]
simp (config := { contextual := true }) only [IH]
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → (a ^ b) ^ b_1 ≤ d) ↔ (a ^ b) ^ c ≤ d
[PROOFSTEP]
exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm
[GOAL]
b : Ordinal.{u_1}
h : 1 < b
x : Ordinal.{u_1}
⊢ log b x = pred (sInf {o | x < b ^ o})
[PROOFSTEP]
simp only [log, dif_pos h]
[GOAL]
b : Ordinal.{u_1}
h : ¬1 < b
x : Ordinal.{u_1}
⊢ log b x = 0
[PROOFSTEP]
simp only [log, dif_neg h]
[GOAL]
b : Ordinal.{u_1}
b1 : 1 < b
⊢ log b 0 = 0
[PROOFSTEP]
rw [log_def b1, ← Ordinal.le_zero, pred_le]
[GOAL]
b : Ordinal.{u_1}
b1 : 1 < b
⊢ sInf {o | 0 < b ^ o} ≤ succ 0
[PROOFSTEP]
apply csInf_le'
[GOAL]
case h
b : Ordinal.{u_1}
b1 : 1 < b
⊢ succ 0 ∈ {o | 0 < b ^ o}
[PROOFSTEP]
dsimp
[GOAL]
case h
b : Ordinal.{u_1}
b1 : 1 < b
⊢ 0 < b ^ succ 0
[PROOFSTEP]
rw [succ_zero, opow_one]
[GOAL]
case h
b : Ordinal.{u_1}
b1 : 1 < b
⊢ 0 < b
[PROOFSTEP]
exact zero_lt_one.trans b1
[GOAL]
b : Ordinal.{u_1}
b1 : ¬1 < b
⊢ log b 0 = 0
[PROOFSTEP]
simp only [log_of_not_one_lt_left b1]
[GOAL]
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
let t := sInf {o | x < (b ^ o)}
[GOAL]
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
have : x < (b ^ t) := csInf_mem (log_nonempty hb)
[GOAL]
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
rcases zero_or_succ_or_limit t with (h | h | h)
[GOAL]
case inl
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : t = 0
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
refine' ((one_le_iff_ne_zero.2 hx).not_lt _).elim
[GOAL]
case inl
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : t = 0
⊢ x < 1
[PROOFSTEP]
simpa only [h, opow_zero] using this
[GOAL]
case inr.inl
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : ∃ a, t = succ a
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
rw [show log b x = pred t from log_def hb x, succ_pred_iff_is_succ.2 h]
[GOAL]
case inr.inr
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : IsLimit t
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
rcases(lt_opow_of_limit (zero_lt_one.trans hb).ne' h).1 this with ⟨a, h₁, h₂⟩
[GOAL]
case inr.inr.intro.intro
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : IsLimit t
a : Ordinal.{u_1}
h₁ : a < t
h₂ : x < b ^ a
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
exact h₁.not_le.elim ((le_csInf_iff'' (log_nonempty hb)).1 le_rfl a h₂)
[GOAL]
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x < b ^ succ (log b x)
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)
[PROOFSTEP]
apply opow_pos _ (zero_lt_one.trans hb)
[GOAL]
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)
[PROOFSTEP]
rw [succ_log_def hb hx]
[GOAL]
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ sInf {o | x < b ^ o}
[PROOFSTEP]
exact csInf_mem (log_nonempty hb)
[GOAL]
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ b ^ log b x ≤ x
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | b0)
[GOAL]
case inl
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ 0 ^ log 0 x ≤ x
[PROOFSTEP]
rw [zero_opow']
[GOAL]
case inl
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ 1 - log 0 x ≤ x
[PROOFSTEP]
refine' (sub_le_self _ _).trans (one_le_iff_ne_zero.2 hx)
[GOAL]
case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
⊢ b ^ log b x ≤ x
[PROOFSTEP]
rcases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with (hb | rfl)
[GOAL]
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x
[PROOFSTEP]
refine' le_of_not_lt fun h => (lt_succ (log b x)).not_le _
[GOAL]
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
⊢ succ (log b x) ≤ log b x
[PROOFSTEP]
have := @csInf_le' _ _ {o | x < (b ^ o)} _ h
[GOAL]
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
this : sInf {o | x < b ^ o} ≤ log b x
⊢ succ (log b x) ≤ log b x
[PROOFSTEP]
rwa [← succ_log_def hb hx] at this
[GOAL]
case inr.inr
x : Ordinal.{u_1}
hx : x ≠ 0
b0 : 1 ≠ 0
⊢ 1 ^ log 1 x ≤ x
[PROOFSTEP]
rwa [one_opow, one_le_iff_ne_zero]
[GOAL]
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ 0 < log b o
[PROOFSTEP]
rwa [← succ_le_iff, succ_zero, ← opow_le_iff_le_log hb ho, opow_one]
[GOAL]
b o : Ordinal.{u_1}
hbo : o < b
⊢ log b o = 0
[PROOFSTEP]
rcases eq_or_ne o 0 with (rfl | ho)
[GOAL]
case inl
b : Ordinal.{u_1}
hbo : 0 < b
⊢ log b 0 = 0
[PROOFSTEP]
exact log_zero_right b
[GOAL]
case inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inr.inl
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : b ≤ 1
⊢ log b o = 0
[PROOFSTEP]
rcases le_one_iff.1 hb with (rfl | rfl)
[GOAL]
case inr.inl.inl
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 0
hb : 0 ≤ 1
⊢ log 0 o = 0
[PROOFSTEP]
exact log_zero_left o
[GOAL]
case inr.inl.inr
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0
[PROOFSTEP]
exact log_one_left o
[GOAL]
case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0
[PROOFSTEP]
rwa [← Ordinal.le_zero, ← lt_succ_iff, succ_zero, ← lt_opow_iff_log_lt hb ho, opow_one]
[GOAL]
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x = 0
⊢ log b x ≤ log b y
[PROOFSTEP]
simp only [hx, log_zero_right, Ordinal.zero_le]
[GOAL]
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : ¬x = 0
hb : ¬1 < b
⊢ log b x ≤ log b y
[PROOFSTEP]
simp only [log_of_not_one_lt_left hb, Ordinal.zero_le]
[GOAL]
b x : Ordinal.{u_1}
hx : x = 0
⊢ log b x ≤ x
[PROOFSTEP]
simp only [hx, log_zero_right, Ordinal.zero_le]
[GOAL]
b x : Ordinal.{u_1}
hx : ¬x = 0
hb : ¬1 < b
⊢ log b x ≤ x
[PROOFSTEP]
simp only [log_of_not_one_lt_left hb, Ordinal.zero_le]
[GOAL]
b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % b ^ log b o < o
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % 0 ^ log 0 o < o
[PROOFSTEP]
simpa using Ordinal.pos_iff_ne_zero.2 ho
[GOAL]
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o
[PROOFSTEP]
exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)
[GOAL]
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ log b (o % b ^ log b o) < log b o
[PROOFSTEP]
cases' eq_or_ne (o % (b ^ log b o)) 0 with h h
[GOAL]
case inl
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ log b (o % b ^ log b o) < log b o
[PROOFSTEP]
rw [h, log_zero_right]
[GOAL]
case inl
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o
[PROOFSTEP]
apply log_pos hb ho hbo
[GOAL]
case inr
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o
[PROOFSTEP]
rw [← succ_le_iff, succ_log_def hb h]
[GOAL]
case inr
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ sInf {o_1 | o % b ^ log b o < b ^ o_1} ≤ log b o
[PROOFSTEP]
apply csInf_le'
[GOAL]
case inr.h
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b o ∈ {o_1 | o % b ^ log b o < b ^ o_1}
[PROOFSTEP]
apply mod_lt
[GOAL]
case inr.h.h
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ b ^ log b o ≠ 0
[PROOFSTEP]
rw [← Ordinal.pos_iff_ne_zero]
[GOAL]
case inr.h.h
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ 0 < b ^ log b o
[PROOFSTEP]
exact opow_pos _ (zero_lt_one.trans hb)
[GOAL]
b u w v : Ordinal.{u_1}
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ u * succ v
[PROOFSTEP]
rwa [mul_succ, add_lt_add_iff_left]
[GOAL]
b u v w : Ordinal.{u_1}
hvb : v < b
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ succ u
[PROOFSTEP]
convert (opow_mul_add_lt_opow_mul_succ v hw).trans_le (mul_le_mul_left' (succ_le_of_lt hvb) _) using 1
[GOAL]
case h.e'_4
b u v w : Ordinal.{u_1}
hvb : v < b
hw : w < b ^ u
⊢ b ^ succ u = b ^ u * b
[PROOFSTEP]
exact opow_succ b u
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
⊢ log b (b ^ u * v + w) = u
[PROOFSTEP]
have hne' := (opow_mul_add_pos (zero_lt_one.trans hb).ne' u hv w).ne'
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
⊢ log b (b ^ u * v + w) = u
[PROOFSTEP]
by_contra' hne
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
⊢ False
[PROOFSTEP]
cases' lt_or_gt_of_ne hne with h h
[GOAL]
case inl
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) < u
⊢ False
[PROOFSTEP]
rw [← lt_opow_iff_log_lt hb hne'] at h
[GOAL]
case inl
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : b ^ u * v + w < b ^ u
⊢ False
[PROOFSTEP]
exact h.not_le ((le_mul_left _ (Ordinal.pos_iff_ne_zero.2 hv)).trans (le_add_right _ _))
[GOAL]
case inr
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) > u
⊢ False
[PROOFSTEP]
conv at h => change u < log b (b ^ u * v + w)
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) > u
| log b (b ^ u * v + w) > u
[PROOFSTEP]
change u < log b (b ^ u * v + w)
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) > u
| log b (b ^ u * v + w) > u
[PROOFSTEP]
change u < log b (b ^ u * v + w)
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) > u
| log b (b ^ u * v + w) > u
[PROOFSTEP]
change u < log b (b ^ u * v + w)
[GOAL]
case inr
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : u < log b (b ^ u * v + w)
⊢ False
[PROOFSTEP]
rw [← succ_le_iff, ← opow_le_iff_le_log hb hne'] at h
[GOAL]
case inr
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h✝ : u < log b (b ^ u * v + w)
h : b ^ succ u ≤ b ^ u * v + w
⊢ False
[PROOFSTEP]
exact (not_lt_of_le h) (opow_mul_add_lt_opow_succ hvb hw)
[GOAL]
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = x
[PROOFSTEP]
convert log_opow_mul_add hb zero_ne_one.symm hb (opow_pos x (zero_lt_one.trans hb)) using 1
[GOAL]
case h.e'_2
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = log b (b ^ x * 1 + 0)
[PROOFSTEP]
rw [add_zero, mul_one]
[GOAL]
b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / b ^ log b o
[PROOFSTEP]
rcases eq_zero_or_pos b with (rfl | hb)
[GOAL]
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / 0 ^ log 0 o
[PROOFSTEP]
simpa using Ordinal.pos_iff_ne_zero.2 ho
[GOAL]
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o
[PROOFSTEP]
rw [div_pos (opow_ne_zero _ hb.ne')]
[GOAL]
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o
[PROOFSTEP]
exact opow_log_le_self b ho
[GOAL]
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o / b ^ log b o < b
[PROOFSTEP]
rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]
[GOAL]
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ succ (log b o)
[PROOFSTEP]
exact lt_opow_succ_log_self hb o
[GOAL]
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
⊢ log b x + log b y ≤ log b (x * y)
[PROOFSTEP]
by_cases hb : 1 < b
[GOAL]
case pos
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)
[PROOFSTEP]
rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]
[GOAL]
case pos
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y
[PROOFSTEP]
exact
  mul_le_mul' (opow_log_le_self b hx)
    (opow_log_le_self b hy)
      -- Porting note: `le_refl` is required.
[GOAL]
case neg
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : ¬1 < b
⊢ log b x + log b y ≤ log b (x * y)
[PROOFSTEP]
simp only [log_of_not_one_lt_left hb, zero_add, le_refl]
[GOAL]
m : ℕ
⊢ ↑(m ^ 0) = ↑m ^ ↑0
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
⊢ ↑(m ^ (n + 1)) = ↑m ^ ↑(n + 1)
[PROOFSTEP]
rw [pow_succ', nat_cast_mul, nat_cast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ]
[GOAL]
o : Ordinal.{u_1}
ho : 0 < o
⊢ (sup fun n => o ^ ↑n) = o ^ ω
[PROOFSTEP]
rcases lt_or_eq_of_le (one_le_iff_pos.2 ho) with (ho₁ | rfl)
[GOAL]
case inl
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ (sup fun n => o ^ ↑n) = o ^ ω
[PROOFSTEP]
exact (opow_isNormal ho₁).apply_omega
[GOAL]
case inr
ho : 0 < 1
⊢ (sup fun n => 1 ^ ↑n) = 1 ^ ω
[PROOFSTEP]
rw [one_opow]
[GOAL]
case inr
ho : 0 < 1
⊢ (sup fun n => 1 ^ ↑n) = 1
[PROOFSTEP]
refine' le_antisymm (sup_le fun n => by rw [one_opow]) _
[GOAL]
ho : 0 < 1
n : ℕ
⊢ 1 ^ ↑n ≤ 1
[PROOFSTEP]
rw [one_opow]
[GOAL]
case inr
ho : 0 < 1
⊢ 1 ≤ sup fun n => 1 ^ ↑n
[PROOFSTEP]
convert le_sup (fun n : ℕ => 1 ^ n) 0
[GOAL]
case h.e'_3
ho : 0 < 1
⊢ 1 = 1 ^ ↑0
[PROOFSTEP]
rw [Nat.cast_zero, opow_zero]


[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  toPGame o = mk (Quotient.out o).α PEmpty (fun x => toPGame (typein (fun x x_1 => x < x_1) x)) PEmpty.elim
[PROOFSTEP]
rw [toPGame]
[GOAL]
o : Ordinal.{u_1}
⊢ LeftMoves (toPGame o) = (Quotient.out o).α
[PROOFSTEP]
rw [toPGame, LeftMoves]
[GOAL]
o : Ordinal.{u_1}
⊢ RightMoves (toPGame o) = PEmpty
[PROOFSTEP]
rw [toPGame, RightMoves]
[GOAL]
⊢ IsEmpty (LeftMoves (toPGame 0))
[PROOFSTEP]
rw [toPGame_leftMoves]
[GOAL]
⊢ IsEmpty (Quotient.out 0).α
[PROOFSTEP]
infer_instance
[GOAL]
o : Ordinal.{?u.8904}
⊢ IsEmpty (RightMoves (toPGame o))
[PROOFSTEP]
rw [toPGame_rightMoves]
[GOAL]
o : Ordinal.{?u.8904}
⊢ IsEmpty PEmpty
[PROOFSTEP]
infer_instance
[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  HEq (moveLeft (toPGame o)) fun x => toPGame (typein (fun x x_1 => x < x_1) x)
[PROOFSTEP]
rw [toPGame]
[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  HEq
    (moveLeft
      ((fun this =>
          mk (Quotient.out o).α PEmpty
            (fun x =>
              let_fun this_1 := (_ : typein (fun x x_1 => x < x_1) x < o);
              toPGame (typein (fun x x_1 => x < x_1) x))
            PEmpty.elim)
        (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1)))
    fun x => toPGame (typein (fun x x_1 => x < x_1) x)
[PROOFSTEP]
rfl
[GOAL]
o : Ordinal.{u_1}
i : ↑(Set.Iio o)
⊢ moveLeft (toPGame o) (↑toLeftMovesToPGame i) = toPGame ↑i
[PROOFSTEP]
simp
[GOAL]
i : LeftMoves (toPGame 1)
⊢ ↑toLeftMovesToPGame.symm i = { val := 0, property := (_ : 0 ∈ Set.Iio 1) }
[PROOFSTEP]
simp
[GOAL]
x : LeftMoves (toPGame 1)
⊢ moveLeft (toPGame 1) x = toPGame 0
[PROOFSTEP]
simp
[GOAL]
i : LeftMoves (toPGame 1)
⊢ moveLeft (toPGame 1) i ≡r moveLeft 1 (↑(Equiv.equivOfUnique (LeftMoves (toPGame 1)) (LeftMoves 1)) i)
[PROOFSTEP]
simpa using zeroToPgameRelabelling
[GOAL]
a b : Ordinal.{u_1}
h : a < b
⊢ toPGame a ⧏ toPGame b
[PROOFSTEP]
convert moveLeft_lf (toLeftMovesToPGame ⟨a, h⟩)
[GOAL]
case h.e'_1
a b : Ordinal.{u_1}
h : a < b
⊢ toPGame a = moveLeft (toPGame b) (↑toLeftMovesToPGame { val := a, property := h })
[PROOFSTEP]
rw [toPGame_moveLeft]
[GOAL]
a b : Ordinal.{u_1}
h : a ≤ b
⊢ toPGame a ≤ toPGame b
[PROOFSTEP]
refine' le_iff_forall_lf.2 ⟨fun i => _, isEmptyElim⟩
[GOAL]
a b : Ordinal.{u_1}
h : a ≤ b
i : LeftMoves (toPGame a)
⊢ moveLeft (toPGame a) i ⧏ toPGame b
[PROOFSTEP]
rw [toPGame_moveLeft']
[GOAL]
a b : Ordinal.{u_1}
h : a ≤ b
i : LeftMoves (toPGame a)
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame b
[PROOFSTEP]
exact toPGame_lf ((toLeftMovesToPGame_symm_lt i).trans_le h)
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a ⧏ toPGame b → a < b
[PROOFSTEP]
contrapose
[GOAL]
a b : Ordinal.{u_1}
⊢ ¬a < b → ¬toPGame a ⧏ toPGame b
[PROOFSTEP]
rw [not_lt, not_lf]
[GOAL]
a b : Ordinal.{u_1}
⊢ b ≤ a → toPGame b ≤ toPGame a
[PROOFSTEP]
exact toPGame_le
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a ≤ toPGame b → a ≤ b
[PROOFSTEP]
contrapose
[GOAL]
a b : Ordinal.{u_1}
⊢ ¬a ≤ b → ¬toPGame a ≤ toPGame b
[PROOFSTEP]
rw [not_le, PGame.not_le]
[GOAL]
a b : Ordinal.{u_1}
⊢ b < a → toPGame b ⧏ toPGame a
[PROOFSTEP]
exact toPGame_lf
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a < toPGame b → a < b
[PROOFSTEP]
contrapose
[GOAL]
a b : Ordinal.{u_1}
⊢ ¬a < b → ¬toPGame a < toPGame b
[PROOFSTEP]
rw [not_lt]
[GOAL]
a b : Ordinal.{u_1}
⊢ b ≤ a → ¬toPGame a < toPGame b
[PROOFSTEP]
exact fun h => not_lt_of_le (toPGame_le h)
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a ≈ toPGame b ↔ a = b
[PROOFSTEP]
change _ ≤ _ ∧ _ ≤ _ ↔ _
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a ≤ toPGame b ∧ toPGame b ≤ toPGame a ↔ a = b
[PROOFSTEP]
rw [le_antisymm_iff, toPGame_le_iff, toPGame_le_iff]
[GOAL]
a b : Ordinal.{u}
⊢ toPGame a + toPGame b ≈ toPGame (a ♯ b)
[PROOFSTEP]
refine' ⟨le_of_forall_lf (fun i => _) isEmptyElim, le_of_forall_lf (fun i => _) isEmptyElim⟩
[GOAL]
case refine'_1
a b : Ordinal.{u}
i : LeftMoves (toPGame a + toPGame b)
⊢ moveLeft (toPGame a + toPGame b) i ⧏ toPGame (a ♯ b)
[PROOFSTEP]
apply leftMoves_add_cases i
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i : LeftMoves (toPGame a + toPGame b)
⊢ ∀ (i : LeftMoves (toPGame a)), moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inl i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
intro i
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i : LeftMoves (toPGame a + toPGame b)
⊢ ∀ (i : LeftMoves (toPGame b)), moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
intro i
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inl i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
let wf := toLeftMovesToPGame_symm_lt i
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
let wf := toLeftMovesToPGame_symm_lt i
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inl i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
try rw [add_moveLeft_inl]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inl i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [add_moveLeft_inl]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
try rw [add_moveLeft_inl]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [add_moveLeft_inl]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a) i + toPGame b ⧏ toPGame (a ♯ b)
[PROOFSTEP]
try rw [add_moveLeft_inr]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a) i + toPGame b ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [add_moveLeft_inr]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
try rw [add_moveLeft_inr]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [add_moveLeft_inr]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a) i + toPGame b ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [toPGame_moveLeft', lf_congr_left (toPGame_add _ _), toPGame_lf_iff]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ toPGame a + moveLeft (toPGame b) i ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [toPGame_moveLeft', lf_congr_left (toPGame_add _ _), toPGame_lf_iff]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ ↑(↑toLeftMovesToPGame.symm i) ♯ b < a ♯ b
[PROOFSTEP]
exact nadd_lt_nadd_right wf _
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ a ♯ ↑(↑toLeftMovesToPGame.symm i) < a ♯ b
[PROOFSTEP]
exact nadd_lt_nadd_left wf _
[GOAL]
case refine'_2
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
⊢ moveLeft (toPGame (a ♯ b)) i ⧏ toPGame a + toPGame b
[PROOFSTEP]
rw [toPGame_moveLeft']
[GOAL]
case refine'_2
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
rcases lt_nadd_iff.1 (toLeftMovesToPGame_symm_lt i) with (⟨c, hc, hc'⟩ | ⟨c, hc, hc'⟩)
[GOAL]
case refine'_2.inl.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < a
hc' : ↑(↑toLeftMovesToPGame.symm i) ≤ c ♯ b
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
rw [← toPGame_le_iff, ← le_congr_right (toPGame_add _ _)] at hc'
[GOAL]
case refine'_2.inr.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < b
hc' : ↑(↑toLeftMovesToPGame.symm i) ≤ a ♯ c
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
rw [← toPGame_le_iff, ← le_congr_right (toPGame_add _ _)] at hc'
[GOAL]
case refine'_2.inl.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < a
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame c + toPGame b
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
apply lf_of_le_of_lf hc'
[GOAL]
case refine'_2.inr.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < b
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame a + toPGame c
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
apply lf_of_le_of_lf hc'
[GOAL]
case refine'_2.inl.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < a
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame c + toPGame b
⊢ toPGame c + toPGame b ⧏ toPGame a + toPGame b
[PROOFSTEP]
apply add_lf_add_right
[GOAL]
case refine'_2.inl.intro.intro.h
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < a
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame c + toPGame b
⊢ toPGame c ⧏ toPGame a
[PROOFSTEP]
rwa [toPGame_lf_iff]
[GOAL]
case refine'_2.inr.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < b
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame a + toPGame c
⊢ toPGame a + toPGame c ⧏ toPGame a + toPGame b
[PROOFSTEP]
apply add_lf_add_left
[GOAL]
case refine'_2.inr.intro.intro.h
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < b
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame a + toPGame c
⊢ toPGame c ⧏ toPGame b
[PROOFSTEP]
rwa [toPGame_lf_iff]