case inl
a b : Ordinal
ha : a = 0
⊢ a * b = b ↔ a ^ ω ∣ b

case inr
a b : Ordinal
ha : 0 < a
⊢ a * b = b ↔ a ^ ω ∣ b
a b : Ordinal
⊢ a * b = b ↔ a ^ ω ∣ b
cases' eq_zero_or_pos a with ha ha
case inr.refine'_1
a b : Ordinal
ha : 0 < a
hab : a * b = b
⊢ a ^ ω ∣ b

case inr.refine'_2
a b : Ordinal
ha : 0 < a
h : a ^ ω ∣ b
⊢ a * b = b
case inr
a b : Ordinal
ha : 0 < a
⊢ a * b = b ↔ a ^ ω ∣ b
refine' ⟨fun hab => _, fun h => _⟩
case inr.refine'_2.intro
a b : Ordinal
ha : 0 < a
c : Ordinal
hc : b = a ^ ω * c
⊢ a * b = b
case inr.refine'_2
a b : Ordinal
ha : 0 < a
h : a ^ ω ∣ b
⊢ a * b = b
cases' h with c hc
no goals
case inr.refine'_2.intro
a b : Ordinal
ha : 0 < a
c : Ordinal
hc : b = a ^ ω * c
⊢ a * b = b
rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega]
case inl
a b : Ordinal
ha : a = 0
⊢ 0 = b ↔ b = 0
case inl
a b : Ordinal
ha : a = 0
⊢ a * b = b ↔ a ^ ω ∣ b
rw [ha, zero_mul, zero_opow omega_ne_zero, zero_dvd_iff]
no goals
case inl
a b : Ordinal
ha : a = 0
⊢ 0 = b ↔ b = 0
exact eq_comm
case inr.refine'_1
a b : Ordinal
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0
case inr.refine'_1
a b : Ordinal
ha : 0 < a
hab : a * b = b
⊢ a ^ ω ∣ b
rw [dvd_iff_mod_eq_zero]
case inr.refine'_1
a b : Ordinal
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0
case inr.refine'_1
a b : Ordinal
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0
rw [← div_add_mod b (a^omega), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega,
  add_left_cancel] at hab
case inr.refine'_1.inl
a b : Ordinal
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : b % a ^ ω = 0
⊢ b % a ^ ω = 0

case inr.refine'_1.inr
a b : Ordinal
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ b % a ^ ω = 0
case inr.refine'_1
a b : Ordinal
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0
cases' eq_zero_or_opow_omega_le_of_mul_eq_right hab with hab hab
case inr.refine'_1.inr
a b : Ordinal
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ a ≠ 0
case inr.refine'_1.inr
a b : Ordinal
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ b % a ^ ω = 0
refine' (not_lt_of_le hab (mod_lt b (opow_ne_zero omega _))).elim
no goals
case inr.refine'_1.inr
a b : Ordinal
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ a ≠ 0
rwa [← Ordinal.pos_iff_ne_zero]
no goals
case inr.refine'_1.inl
a b : Ordinal
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : b % a ^ ω = 0
⊢ b % a ^ ω = 0
exact hab