a b : Cardinal
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = max b a
a b : Cardinal
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ a * b = max a b
rw [mul_comm, max_comm]
no goals
a b : Cardinal
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = max b a
exact mul_eq_max_of_aleph0_le_left h h'