case inl

⊢ Principal (fun x x_1 => x + x_1) 0 ↔ 0 = 0 ∨ ∃ a, 0 = ω ^ a

case inr
o : Ordinal
ho : o ≠ 0
⊢ Principal (fun x x_1 => x + x_1) o ↔ o = 0 ∨ ∃ a, o = ω ^ a
o : Ordinal
⊢ Principal (fun x x_1 => x + x_1) o ↔ o = 0 ∨ ∃ a, o = ω ^ a
rcases eq_or_ne o 0 with (rfl | ho)
no goals
case inl

⊢ Principal (fun x x_1 => x + x_1) 0 ↔ 0 = 0 ∨ ∃ a, 0 = ω ^ a
simp only [principal_zero, Or.inl]
case inr
o : Ordinal
ho : o ≠ 0
⊢ (∀ (a : Ordinal), a < o → a + o = o) ↔ o = 0 ∨ ∃ a, o = ω ^ a
case inr
o : Ordinal
ho : o ≠ 0
⊢ Principal (fun x x_1 => x + x_1) o ↔ o = 0 ∨ ∃ a, o = ω ^ a
rw [principal_add_iff_add_left_eq_self]
case inr
o : Ordinal
ho : o ≠ 0
⊢ (∀ (a : Ordinal), a < o → a + o = o) ↔ ∃ a, o = ω ^ a
case inr
o : Ordinal
ho : o ≠ 0
⊢ (∀ (a : Ordinal), a < o → a + o = o) ↔ o = 0 ∨ ∃ a, o = ω ^ a
simp only [ho, false_or_iff]
case inr
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
⊢ False
case inr
o : Ordinal
ho : o ≠ 0
⊢ (∀ (a : Ordinal), a < o → a + o = o) ↔ ∃ a, o = ω ^ a
refine'
  ⟨fun H => ⟨_, ((lt_or_eq_of_le (opow_log_le_self _ ho)).resolve_left fun h => _).symm⟩,
    fun ⟨b, e⟩ => e.symm ▸ fun a => add_omega_opow⟩
case inr
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ False
case inr
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
⊢ False
have := H _ h
case inr
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : o < ω ^ succ (log ω o)
⊢ False
case inr
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ False
have := lt_opow_succ_log_self one_lt_omega o
case inr
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : ∃ c', c' < ω ∧ o < ω ^ log ω o * c'
⊢ False
case inr
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : o < ω ^ succ (log ω o)
⊢ False
rw [opow_succ, lt_mul_of_limit omega_isLimit] at this
case inr.intro.intro
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
a : Ordinal
ao : a < ω
h' : o < ω ^ log ω o * a
⊢ False
case inr
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : ∃ c', c' < ω ∧ o < ω ^ log ω o * c'
⊢ False
rcases this with ⟨a, ao, h'⟩
case inr.intro.intro.intro
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
ao : ↑n < ω
h' : o < ω ^ log ω o * ↑n
⊢ False
case inr.intro.intro
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
a : Ordinal
ao : a < ω
h' : o < ω ^ log ω o * a
⊢ False
rcases lt_omega.1 ao with ⟨n, rfl⟩
case inr.intro.intro.intro
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
h' : o < ω ^ log ω o * ↑n
⊢ False
case inr.intro.intro.intro
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
ao : ↑n < ω
h' : o < ω ^ log ω o * ↑n
⊢ False
clear ao
case inr.intro.intro.intro
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ o < ω ^ log ω o * ↑n → False
case inr.intro.intro.intro
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
h' : o < ω ^ log ω o * ↑n
⊢ False
revert h'
case inr.intro.intro.intro.h
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n ≤ o
case inr.intro.intro.intro
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ o < ω ^ log ω o * ↑n → False
apply not_lt_of_le
case inr.intro.intro.intro.h
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
e : ω ^ log ω o * ↑n + o = o
⊢ ω ^ log ω o * ↑n ≤ o

case e
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n + o = o
case inr.intro.intro.intro.h
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n ≤ o
suffices e : (omega^log omega o) * ↑n + o = o
case e.zero
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ ω ^ log ω o * ↑Nat.zero + o = o

case e.succ
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
IH : ω ^ log ω o * ↑n + o = o
⊢ ω ^ log ω o * ↑(Nat.succ n) + o = o
case e
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n + o = o
induction' n with n IH
no goals
case e.succ
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
IH : ω ^ log ω o * ↑n + o = o
⊢ ω ^ log ω o * ↑(Nat.succ n) + o = o
simp only [Nat.cast_succ, mul_add_one, add_assoc, this, IH]
no goals
case inr.intro.intro.intro.h
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
e : ω ^ log ω o * ↑n + o = o
⊢ ω ^ log ω o * ↑n ≤ o
simpa only [e] using le_add_right ((omega^log omega o) * ↑n) o
no goals
case e.zero
o : Ordinal
ho : o ≠ 0
H : ∀ (a : Ordinal), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ ω ^ log ω o * ↑Nat.zero + o = o
simp [Nat.cast_zero, mul_zero, zero_add]