case inl
b : Cardinal
⊢ 0 * b ≤ max (max 0 b) ℵ₀

case inr
a b : Cardinal
ha0 : a ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
a b : Cardinal
⊢ a * b ≤ max (max a b) ℵ₀
rcases eq_or_ne a 0 with (rfl | ha0)
case inr.inl
a : Cardinal
ha0 : a ≠ 0
⊢ a * 0 ≤ max (max a 0) ℵ₀

case inr.inr
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
case inr
a b : Cardinal
ha0 : a ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
rcases eq_or_ne b 0 with (rfl | hb0)
case inr.inr.inl
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a * b ≤ max (max a b) ℵ₀

case inr.inr.inr
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
case inr.inr
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
cases' le_or_lt ℵ₀ a with ha ha
no goals
case inl
b : Cardinal
⊢ 0 * b ≤ max (max 0 b) ℵ₀
simp
no goals
case inr.inl
a : Cardinal
ha0 : a ≠ 0
⊢ a * 0 ≤ max (max a 0) ℵ₀
simp
case inr.inr.inl
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
case inr.inr.inl
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a * b ≤ max (max a b) ℵ₀
rw [mul_eq_max_of_aleph0_le_left ha hb0]
no goals
case inr.inr.inl
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
exact le_max_left _ _
case inr.inr.inr.inl
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a * b ≤ max (max a b) ℵ₀

case inr.inr.inr.inr
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
case inr.inr.inr
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
cases' le_or_lt ℵ₀ b with hb hb
case inr.inr.inr.inl
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀
case inr.inr.inr.inl
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a * b ≤ max (max a b) ℵ₀
rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]
no goals
case inr.inr.inr.inl
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀
exact le_max_left _ _
no goals
case inr.inr.inr.inr
a b : Cardinal
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
exact le_max_of_le_right (mul_lt_aleph0 ha hb).le