-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_add_iff_zero_or_omega0_opow :
    Principal (· + ·) o ↔ o = 0 ∨ o ∈ Set.range (ω ^ · : Ordinal → Ordinal)

Proof state:
case inr
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
⊢ False

Tactic:
have := H _ h

Result:
case inr
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ False

Proof state:
case inr
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ False

Tactic:
have := lt_opow_succ_log_self one_lt_omega0 o

Result:
case inr
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : o < ω ^ succ (log ω o)
⊢ False

Proof state:
case inr
o : Ordinal.{u}
ho : o ≠ 0
⊢ (∀ a < o, a + o = o) ↔ o ∈ Set.range fun x => ω ^ x

Tactic:
refine
  ⟨fun H => ⟨_, ((lt_or_eq_of_le (opow_log_le_self _ ho)).resolve_left fun h => ?_)⟩,
    fun ⟨b, e⟩ => e.symm ▸ fun a => add_omega0_opow⟩

Result:
case inr
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
⊢ False

Proof state:
case inr
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : o < ω ^ succ (log ω o)
⊢ False

Tactic:
rw [opow_succ, lt_mul_of_limit isLimit_omega0] at this

Result:
case inr
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : ∃ c' < ω, o < ω ^ log ω o * c'
⊢ False

Proof state:
case inr
o : Ordinal.{u}
ho : o ≠ 0
⊢ Principal (fun x1 x2 => x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun x => ω ^ x

Tactic:
rw [principal_add_iff_add_left_eq_self]

Result:
case inr
o : Ordinal.{u}
ho : o ≠ 0
⊢ (∀ a < o, a + o = o) ↔ o = 0 ∨ o ∈ Set.range fun x => ω ^ x

Proof state:
case inr.intro.intro.intro
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
ao : ↑n < ω
h' : o < ω ^ log ω o * ↑n
⊢ False

Tactic:
clear ao

Result:
case inr.intro.intro.intro
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
h' : o < ω ^ log ω o * ↑n
⊢ False

Proof state:
case inr.intro.intro.intro.hab
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n + o = o

Tactic:
induction' n with n IH

Result:
case inr.intro.intro.intro.hab.zero
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ ω ^ log ω o * ↑0 + o = o

case inr.intro.intro.intro.hab.succ
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
IH : ω ^ log ω o * ↑n + o = o
⊢ ω ^ log ω o * ↑(n + 1) + o = o

Proof state:
case inr.intro.intro.intro
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
h' : o < ω ^ log ω o * ↑n
⊢ False

Tactic:
revert h'

Result:
case inr.intro.intro.intro
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ o < ω ^ log ω o * ↑n → False

Proof state:
case inr.intro.intro.intro.hab.succ
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
IH : ω ^ log ω o * ↑n + o = o
⊢ ω ^ log ω o * ↑(n + 1) + o = o

Tactic:
simp only [Nat.cast_succ, mul_add_one, add_assoc, this, IH]

Result:
no goals

Proof state:
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ 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

Tactic:
simpa only [e] using le_add_right (ω ^ log ω o * ↑n) o

Result:
no goals

Proof state:
case inr.intro.intro.intro.hab
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n ≤ o

Tactic:
suffices e : ω ^ log ω o * n + o = o by
  simpa only [e] using le_add_right (ω ^ log ω o * ↑n) o

Result:
case inr.intro.intro.intro.hab
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n + o = o

Proof state:
case inr.intro.intro.intro.hab.zero
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ ω ^ log ω o * ↑0 + o = o

Tactic:
simp [Nat.cast_zero, mul_zero, zero_add]

Result:
no goals

Proof state:
case inr
o : Ordinal.{u}
ho : o ≠ 0
⊢ (∀ a < o, a + o = o) ↔ o = 0 ∨ o ∈ Set.range fun x => ω ^ x

Tactic:
simp only [ho, false_or]

Result:
case inr
o : Ordinal.{u}
ho : o ≠ 0
⊢ (∀ a < o, a + o = o) ↔ o ∈ Set.range fun x => ω ^ x

Proof state:
case inr.intro.intro
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
a : Ordinal.{u}
ao : a < ω
h' : o < ω ^ log ω o * a
⊢ False

Tactic:
rcases lt_omega0.1 ao with ⟨n, rfl⟩

Result:
case inr.intro.intro.intro
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
ao : ↑n < ω
h' : o < ω ^ log ω o * ↑n
⊢ False

Proof state:
case inl

⊢ Principal (fun x1 x2 => x1 + x2) 0 ↔ 0 = 0 ∨ 0 ∈ Set.range fun x => ω ^ x

Tactic:
simp only [principal_zero, Or.inl]

Result:
no goals

Proof state:
case inr
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : ∃ c' < ω, o < ω ^ log ω o * c'
⊢ False

Tactic:
rcases this with ⟨a, ao, h'⟩

Result:
case inr.intro.intro
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
a : Ordinal.{u}
ao : a < ω
h' : o < ω ^ log ω o * a
⊢ False

Proof state:
case inr.intro.intro.intro
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ o < ω ^ log ω o * ↑n → False

Tactic:
apply not_lt_of_le

Result:
case inr.intro.intro.intro.hab
o : Ordinal.{u}
ho : o ≠ 0
H : ∀ a < o, a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n ≤ o

Proof state:
o : Ordinal.{u}
⊢ Principal (fun x1 x2 => x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun x => ω ^ x

Tactic:
rcases eq_or_ne o 0 with (rfl | ho)

Result:
case inl

⊢ Principal (fun x1 x2 => x1 + x2) 0 ↔ 0 = 0 ∨ 0 ∈ Set.range fun x => ω ^ x

case inr
o : Ordinal.{u}
ho : o ≠ 0
⊢ Principal (fun x1 x2 => x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun x => ω ^ x