case intro.intro.inl
a b : Cardinal
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = max a b

case intro.intro.inr
a b : Cardinal
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = max a b
a b : Cardinal
h : ℵ₀ ≤ a * b
⊢ a * b = max a b
rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩
no goals
case intro.intro.inl
a b : Cardinal
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = max a b
exact mul_eq_max_of_aleph0_le_left ha' hb
no goals
case intro.intro.inr
a b : Cardinal
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = max a b
exact mul_eq_max_of_aleph0_le_right ha hb'