case inl

⊢ (sup fun n => 0 * ↑n) = 0 * ω

case inr
o : Ordinal
ho : 0 < o
⊢ (sup fun n => o * ↑n) = o * ω
o : Ordinal
⊢ (sup fun n => o * ↑n) = o * ω
rcases eq_zero_or_pos o with (rfl | ho)
case inl

⊢ (sup fun n => 0 * ↑n) = 0
case inl

⊢ (sup fun n => 0 * ↑n) = 0 * ω
rw [zero_mul]
no goals
case inl

⊢ (sup fun n => 0 * ↑n) = 0
exact sup_eq_zero_iff.2 fun n => zero_mul (n : Ordinal)
no goals
case inr
o : Ordinal
ho : 0 < o
⊢ (sup fun n => o * ↑n) = o * ω
exact (mul_isNormal ho).apply_omega