case inl
a b : Cardinal
ha : ℵ₀ ≤ a
⊢ a + b ≤ max (max a b) ℵ₀

case inr
a b : Cardinal
ha : a < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀
a b : Cardinal
⊢ a + b ≤ max (max a b) ℵ₀
cases' le_or_lt ℵ₀ a with ha ha
case inl
a b : Cardinal
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
case inl
a b : Cardinal
ha : ℵ₀ ≤ a
⊢ a + b ≤ max (max a b) ℵ₀
rw [add_eq_max ha]
no goals
case inl
a b : Cardinal
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
exact le_max_left _ _
case inr.inl
a b : Cardinal
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a + b ≤ max (max a b) ℵ₀

case inr.inr
a b : Cardinal
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀
case inr
a b : Cardinal
ha : a < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀
cases' le_or_lt ℵ₀ b with hb hb
case inr.inl
a b : Cardinal
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀
case inr.inl
a b : Cardinal
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a + b ≤ max (max a b) ℵ₀
rw [add_comm, add_eq_max hb, max_comm]
no goals
case inr.inl
a b : Cardinal
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀
exact le_max_left _ _
no goals
case inr.inr
a b : Cardinal
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀
exact le_max_of_le_right (add_lt_aleph0 ha hb).le