case inl
b : Ordinal
ha : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) (0 ^ b)

case inr.intro
b c : Ordinal
ha : Principal (fun x x_1 => x + x_1) (ω ^ c)
⊢ Principal (fun x x_1 => x + x_1) ((ω ^ c) ^ b)
a : Ordinal
ha : Principal (fun x x_1 => x + x_1) a
b : Ordinal
⊢ Principal (fun x x_1 => x + x_1) (a ^ b)
rcases principal_add_iff_zero_or_omega_opow.1 ha with (rfl | ⟨c, rfl⟩)
case inl.inl
ha : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) (0 ^ 0)

case inl.inr
b : Ordinal
ha : Principal (fun x x_1 => x + x_1) 0
hb : b ≠ 0
⊢ Principal (fun x x_1 => x + x_1) (0 ^ b)
case inl
b : Ordinal
ha : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) (0 ^ b)
rcases eq_or_ne b 0 with (rfl | hb)
case inl.inl
ha : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) 1
case inl.inl
ha : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) (0 ^ 0)
rw [opow_zero]
no goals
case inl.inl
ha : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) 1
exact principal_add_one
no goals
case inl.inr
b : Ordinal
ha : Principal (fun x x_1 => x + x_1) 0
hb : b ≠ 0
⊢ Principal (fun x x_1 => x + x_1) (0 ^ b)
rwa [zero_opow hb]
case inr.intro
b c : Ordinal
ha : Principal (fun x x_1 => x + x_1) (ω ^ c)
⊢ Principal (fun x x_1 => x + x_1) (ω ^ (c * b))
case inr.intro
b c : Ordinal
ha : Principal (fun x x_1 => x + x_1) (ω ^ c)
⊢ Principal (fun x x_1 => x + x_1) ((ω ^ c) ^ b)
rw [← opow_mul]
no goals
case inr.intro
b c : Ordinal
ha : Principal (fun x x_1 => x + x_1) (ω ^ c)
⊢ Principal (fun x x_1 => x + x_1) (ω ^ (c * b))
exact principal_add_omega_opow _