-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_mul_iff_le_two_or_omega0_opow_opow :
    Principal (· * ·) o ↔ o ≤ 2 ∨ o ∈ Set.range (ω ^ ω ^ · : Ordinal → Ordinal)

Proof state:
case refine_1.inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x => ω ^ ω ^ x

Tactic:
rcases principal_add_iff_zero_or_omega0_opow.1 (principal_add_of_principal_mul ho ho₂.ne')
  with (rfl | ⟨a, rfl⟩)

Result:
case refine_1.inr.inl
ho : Principal (fun x1 x2 => x1 * x2) 0
ho₂ : 2 < 0
⊢ 0 ≤ 2 ∨ 0 ∈ Set.range fun x => ω ^ ω ^ x

case refine_1.inr.inr.intro
a : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) ((fun x => ω ^ x) a)
ho₂ : 2 < (fun x => ω ^ x) a
⊢ (fun x => ω ^ x) a ≤ 2 ∨ (fun x => ω ^ x) a ∈ Set.range fun x => ω ^ ω ^ x

Proof state:
case refine_1.inr.inr.intro
a : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) ((fun x => ω ^ x) a)
ho₂ : 2 < (fun x => ω ^ x) a
⊢ (fun x => ω ^ x) a ≤ 2 ∨ (fun x => ω ^ x) a ∈ Set.range fun x => ω ^ ω ^ x

Tactic:
rcases principal_add_iff_zero_or_omega0_opow.1
  (principal_add_of_principal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)

Result:
case refine_1.inr.inr.intro.inl
ho : Principal (fun x1 x2 => x1 * x2) ((fun x => ω ^ x) 0)
ho₂ : 2 < (fun x => ω ^ x) 0
⊢ (fun x => ω ^ x) 0 ≤ 2 ∨ (fun x => ω ^ x) 0 ∈ Set.range fun x => ω ^ ω ^ x

case refine_1.inr.inr.intro.inr.intro
b : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) ((fun x => ω ^ x) ((fun x => ω ^ x) b))
ho₂ : 2 < (fun x => ω ^ x) ((fun x => ω ^ x) b)
⊢ (fun x => ω ^ x) ((fun x => ω ^ x) b) ≤ 2 ∨ (fun x => ω ^ x) ((fun x => ω ^ x) b) ∈ Set.range fun x => ω ^ ω ^ x

Proof state:
case refine_2.inr.intro
a : Ordinal.{u}
⊢ Principal (fun x1 x2 => x1 * x2) ((fun x => ω ^ ω ^ x) a)

Tactic:
exact principal_mul_omega0_opow_opow a

Result:
no goals

Proof state:
case refine_2.inl
o : Ordinal.{u}
ho₂ : o ≤ 2
⊢ Principal (fun x1 x2 => x1 * x2) o

Tactic:
exact principal_mul_of_le_two ho₂

Result:
no goals

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

Tactic:
refine ⟨fun ho => ?_, ?_⟩

Result:
case refine_1
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x => ω ^ ω ^ x

case refine_2
o : Ordinal.{u}
⊢ (o ≤ 2 ∨ o ∈ Set.range fun x => ω ^ ω ^ x) → Principal (fun x1 x2 => x1 * x2) o

Proof state:
case refine_1.inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ o ∈ Set.range fun x => ω ^ ω ^ x

Tactic:
exact Or.inl ho₂

Result:
no goals

Proof state:
case refine_1.inr.inr.intro.inl
ho : Principal (fun x1 x2 => x1 * x2) ((fun x => ω ^ x) 0)
ho₂ : 2 < (fun x => ω ^ x) 0
⊢ (fun x => ω ^ x) 0 ≤ 2 ∨ (fun x => ω ^ x) 0 ∈ Set.range fun x => ω ^ ω ^ x

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x => ω ^ ω ^ x

Tactic:
rcases le_or_lt o 2 with ho₂ | ho₂

Result:
case refine_1.inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ o ∈ Set.range fun x => ω ^ ω ^ x

case refine_1.inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x => ω ^ ω ^ x

Proof state:
case refine_2
o : Ordinal.{u}
⊢ (o ≤ 2 ∨ o ∈ Set.range fun x => ω ^ ω ^ x) → Principal (fun x1 x2 => x1 * x2) o

Tactic:
rintro (ho₂ | ⟨a, rfl⟩)

Result:
case refine_2.inl
o : Ordinal.{u}
ho₂ : o ≤ 2
⊢ Principal (fun x1 x2 => x1 * x2) o

case refine_2.inr.intro
a : Ordinal.{u}
⊢ Principal (fun x1 x2 => x1 * x2) ((fun x => ω ^ ω ^ x) a)

Proof state:
case refine_1.inr.inr.intro.inr.intro
b : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) ((fun x => ω ^ x) ((fun x => ω ^ x) b))
ho₂ : 2 < (fun x => ω ^ x) ((fun x => ω ^ x) b)
⊢ (fun x => ω ^ x) ((fun x => ω ^ x) b) ≤ 2 ∨ (fun x => ω ^ x) ((fun x => ω ^ x) b) ∈ Set.range fun x => ω ^ ω ^ x

Tactic:
exact Or.inr ⟨b, rfl⟩

Result:
no goals

Proof state:
case refine_1.inr.inl
ho : Principal (fun x1 x2 => x1 * x2) 0
ho₂ : 2 < 0
⊢ 0 ≤ 2 ∨ 0 ∈ Set.range fun x => ω ^ ω ^ x

Tactic:
exact (Ordinal.not_lt_zero 2 ho₂).elim

Result:
no goals