case refine'_1
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
⊢ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a

case refine'_2
o : Ordinal
⊢ (o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a) → Principal (fun x x_1 => x * x_1) o
o : Ordinal
⊢ Principal (fun x x_1 => x * x_1) o ↔ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a
refine' ⟨fun ho => _, _⟩
case refine'_1.inl
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a

case refine'_1.inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a
case refine'_1
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
⊢ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a
cases' le_or_lt o 2 with ho₂ ho₂
case refine'_1.inr.inl
ho : Principal (fun x x_1 => x * x_1) 0
ho₂ : 2 < 0
⊢ 0 ≤ 2 ∨ ∃ a, 0 = ω ^ ω ^ a

case refine'_1.inr.inr.intro
a : Ordinal
ho : Principal (fun x x_1 => x * x_1) (ω ^ a)
ho₂ : 2 < ω ^ a
⊢ ω ^ a ≤ 2 ∨ ∃ a_1, ω ^ a = ω ^ ω ^ a_1
case refine'_1.inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a
rcases principal_add_iff_zero_or_omega_opow.1 (principal_add_of_principal_mul ho ho₂.ne') with
  (rfl | ⟨a, rfl⟩)
case refine'_1.inr.inr.intro.inl
ho : Principal (fun x x_1 => x * x_1) (ω ^ 0)
ho₂ : 2 < ω ^ 0
⊢ ω ^ 0 ≤ 2 ∨ ∃ a, ω ^ 0 = ω ^ ω ^ a

case refine'_1.inr.inr.intro.inr.intro
b : Ordinal
ho : Principal (fun x x_1 => x * x_1) (ω ^ ω ^ b)
ho₂ : 2 < ω ^ ω ^ b
⊢ ω ^ ω ^ b ≤ 2 ∨ ∃ a, ω ^ ω ^ b = ω ^ ω ^ a
case refine'_1.inr.inr.intro
a : Ordinal
ho : Principal (fun x x_1 => x * x_1) (ω ^ a)
ho₂ : 2 < ω ^ a
⊢ ω ^ a ≤ 2 ∨ ∃ a_1, ω ^ a = ω ^ ω ^ a_1
rcases principal_add_iff_zero_or_omega_opow.1
    (principal_add_of_principal_mul_opow one_lt_omega ho) with
  (rfl | ⟨b, rfl⟩)
no goals
case refine'_1.inr.inr.intro.inr.intro
b : Ordinal
ho : Principal (fun x x_1 => x * x_1) (ω ^ ω ^ b)
ho₂ : 2 < ω ^ ω ^ b
⊢ ω ^ ω ^ b ≤ 2 ∨ ∃ a, ω ^ ω ^ b = ω ^ ω ^ a
exact Or.inr ⟨b, rfl⟩
no goals
case refine'_1.inl
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a
exact Or.inl ho₂
no goals
case refine'_1.inr.inl
ho : Principal (fun x x_1 => x * x_1) 0
ho₂ : 2 < 0
⊢ 0 ≤ 2 ∨ ∃ a, 0 = ω ^ ω ^ a
exact (Ordinal.not_lt_zero 2 ho₂).elim
case refine'_1.inr.inr.intro.inl.h
ho : Principal (fun x x_1 => x * x_1) (ω ^ 0)
ho₂ : 2 < ω ^ 0
⊢ ω ^ 0 ≤ 2
case refine'_1.inr.inr.intro.inl
ho : Principal (fun x x_1 => x * x_1) (ω ^ 0)
ho₂ : 2 < ω ^ 0
⊢ ω ^ 0 ≤ 2 ∨ ∃ a, ω ^ 0 = ω ^ ω ^ a
left
no goals
case refine'_1.inr.inr.intro.inl.h
ho : Principal (fun x x_1 => x * x_1) (ω ^ 0)
ho₂ : 2 < ω ^ 0
⊢ ω ^ 0 ≤ 2
simpa using one_le_two
case refine'_2.inl
o : Ordinal
ho₂ : o ≤ 2
⊢ Principal (fun x x_1 => x * x_1) o

case refine'_2.inr.intro
a : Ordinal
⊢ Principal (fun x x_1 => x * x_1) (ω ^ ω ^ a)
case refine'_2
o : Ordinal
⊢ (o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a) → Principal (fun x x_1 => x * x_1) o
rintro (ho₂ | ⟨a, rfl⟩)
no goals
case refine'_2.inl
o : Ordinal
ho₂ : o ≤ 2
⊢ Principal (fun x x_1 => x * x_1) o
exact principal_mul_of_le_two ho₂
no goals
case refine'_2.inr.intro
a : Ordinal
⊢ Principal (fun x x_1 => x * x_1) (ω ^ ω ^ a)
exact principal_mul_omega_opow_opow a