case inl
a b : Ordinal
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b

case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
⊢ b = 0 ∨ a ^ ω ≤ b
a b : Ordinal
hab : a * b = b
⊢ b = 0 ∨ a ^ ω ≤ b
cases' eq_zero_or_pos a with ha ha
case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
⊢ ¬b = 0 → a ^ ω ≤ b
case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
⊢ b = 0 ∨ a ^ ω ≤ b
rw [or_iff_not_imp_left]
case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ a ^ ω ≤ b
case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
⊢ ¬b = 0 → a ^ ω ≤ b
intro hb
case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x => a * x) 1 ≤ b
case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ a ^ ω ≤ b
rw [← nfp_mul_one ha]
case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun x => a * x) 1 ≤ b
case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x => a * x) 1 ≤ b
rw [← Ne.def, ← one_le_iff_ne_zero] at hb
no goals
case inr
a b : Ordinal
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun x => a * x) 1 ≤ b
exact nfp_le_fp (mul_isNormal ha).monotone hb (le_of_eq hab)
case inl
a b : Ordinal
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b
case inl
a b : Ordinal
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b
rw [ha, zero_opow omega_ne_zero]
no goals
case inl
a b : Ordinal
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b
exact Or.inr (Ordinal.zero_le b)