case refine'_1
a : Ordinal
l : IsLimit a
⊢ a ≤ ω * (a / ω)

case refine'_2
a : Ordinal
h : a ≠ 0 ∧ ω ∣ a
⊢ IsLimit a
a : Ordinal
⊢ IsLimit a ↔ a ≠ 0 ∧ ω ∣ a
refine' ⟨fun l => ⟨l.1, ⟨a / ω, le_antisymm _ (mul_div_le _ _)⟩⟩, fun h => _⟩
case refine'_1
a : Ordinal
l : IsLimit a
x : Ordinal
hx : x < a
⊢ x < ω * (a / ω)
case refine'_1
a : Ordinal
l : IsLimit a
⊢ a ≤ ω * (a / ω)
refine' (limit_le l).2 fun x hx => le_of_lt _
case refine'_1
a : Ordinal
l : IsLimit a
x : Ordinal
hx : x < a
⊢ ∀ (b' : Ordinal), b' < ω → ω * (x / ω) + b' ≤ a
case refine'_1
a : Ordinal
l : IsLimit a
x : Ordinal
hx : x < a
⊢ x < ω * (a / ω)
rw [← div_lt omega_ne_zero, ← succ_le_iff, le_div omega_ne_zero, mul_succ,
  add_le_of_limit omega_isLimit]
case refine'_1
a : Ordinal
l : IsLimit a
x : Ordinal
hx : x < a
b : Ordinal
hb : b < ω
⊢ ω * (x / ω) + b ≤ a
case refine'_1
a : Ordinal
l : IsLimit a
x : Ordinal
hx : x < a
⊢ ∀ (b' : Ordinal), b' < ω → ω * (x / ω) + b' ≤ a
intro b hb
case refine'_1.intro
a : Ordinal
l : IsLimit a
x : Ordinal
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ ω * (x / ω) + ↑n ≤ a
case refine'_1
a : Ordinal
l : IsLimit a
x : Ordinal
hx : x < a
b : Ordinal
hb : b < ω
⊢ ω * (x / ω) + b ≤ a
rcases lt_omega.1 hb with ⟨n, rfl⟩
no goals
case refine'_1.intro
a : Ordinal
l : IsLimit a
x : Ordinal
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ ω * (x / ω) + ↑n ≤ a
exact
  (add_le_add_right (mul_div_le _ _) _).trans
    (lt_sub.1 <| nat_lt_limit (sub_isLimit l hx) _).le
case refine'_2.intro.intro
b : Ordinal
a0 : ω * b ≠ 0
⊢ IsLimit (ω * b)
case refine'_2
a : Ordinal
h : a ≠ 0 ∧ ω ∣ a
⊢ IsLimit a
rcases h with ⟨a0, b, rfl⟩
case refine'_2.intro.intro
b : Ordinal
a0 : ω * b ≠ 0
⊢ b = 0 → ω * b = 0
case refine'_2.intro.intro
b : Ordinal
a0 : ω * b ≠ 0
⊢ IsLimit (ω * b)
refine' mul_isLimit_left omega_isLimit (Ordinal.pos_iff_ne_zero.2 <| mt _ a0)
case refine'_2.intro.intro
b : Ordinal
a0 : ω * b ≠ 0
e : b = 0
⊢ ω * b = 0
case refine'_2.intro.intro
b : Ordinal
a0 : ω * b ≠ 0
⊢ b = 0 → ω * b = 0
intro e
no goals
case refine'_2.intro.intro
b : Ordinal
a0 : ω * b ≠ 0
e : b = 0
⊢ ω * b = 0
simp only [e, mul_zero]