case h.e'_4
a b : Cardinal
h : ℵ₀ ≤ a
⊢ max a b = max a b * max a b
a b : Cardinal
h : ℵ₀ ≤ a
⊢ a * b ≤ max a b
convert mul_le_mul' (le_max_left a b) (le_max_right a b) using 1
case h.e'_4
a b : Cardinal
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ max a b
case h.e'_4
a b : Cardinal
h : ℵ₀ ≤ a
⊢ max a b = max a b * max a b
rw [mul_eq_self]
no goals
case h.e'_4
a b : Cardinal
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ max a b
refine' h.trans (le_max_left a b)