a b : Cardinal
⊢ a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
a b : Cardinal
⊢ a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0
rw [max_le_iff]
case refine'_1
a b : Cardinal
h : a + b = a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

case refine'_2
a b : Cardinal
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a
a b : Cardinal
⊢ a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
refine' ⟨fun h => _, _⟩
case refine'_1.inl
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

case refine'_1.inr
a b : Cardinal
h : a + b = a
ha : a < ℵ₀
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
case refine'_1
a b : Cardinal
h : a + b = a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
cases' le_or_lt ℵ₀ a with ha ha
case refine'_1.inr.h
a b : Cardinal
h : a + b = a
ha : a < ℵ₀
⊢ b = 0
case refine'_1.inr
a b : Cardinal
h : a + b = a
ha : a < ℵ₀
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
right
case refine'_1.inr.h
a b : Cardinal
h : a + b = a
ha : (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
⊢ b = 0
case refine'_1.inr.h
a b : Cardinal
h : a + b = a
ha : a < ℵ₀
⊢ b = 0
rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
case refine'_1.inr.h.intro.intro.intro
n m : ℕ
h : ↑n + ↑m = ↑n
⊢ ↑m = 0
case refine'_1.inr.h
a b : Cardinal
h : a + b = a
ha : (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
⊢ b = 0
rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩
case refine'_1.inr.h.intro.intro.intro
n m : ℕ
h : n + m = n
⊢ m = 0
case refine'_1.inr.h.intro.intro.intro
n m : ℕ
h : ↑n + ↑m = ↑n
⊢ ↑m = 0
norm_cast  at h⊢
no goals
case refine'_1.inr.h.intro.intro.intro
n m : ℕ
h : n + m = n
⊢ m = 0
rw [← add_right_inj, h, add_zero]
case refine'_1.inl.h
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a
case refine'_1.inl
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
left
case refine'_1.inl.h
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ b ≤ a
case refine'_1.inl.h
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a
use ha
case refine'_1.inl.h
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ¬a < b
case refine'_1.inl.h
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ b ≤ a
rw [← not_lt]
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ a < b → a < a + b
case refine'_1.inl.h
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ¬a < b
apply fun hb => ne_of_gt _ h
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
hb : a < b
⊢ a < a + b
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
⊢ a < b → a < a + b
intro hb
no goals
a b : Cardinal
h : a + b = a
ha : ℵ₀ ≤ a
hb : a < b
⊢ a < a + b
exact hb.trans_le (self_le_add_left b a)
case refine'_2.inl.intro
a b : Cardinal
h1 : ℵ₀ ≤ a
h2 : b ≤ a
⊢ a + b = a

case refine'_2.inr
a b : Cardinal
h3 : b = 0
⊢ a + b = a
case refine'_2
a b : Cardinal
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a
rintro (⟨h1, h2⟩ | h3)
no goals
case refine'_2.inl.intro
a b : Cardinal
h1 : ℵ₀ ≤ a
h2 : b ≤ a
⊢ a + b = a
rw [add_eq_max h1, max_eq_left h2]
no goals
case refine'_2.inr
a b : Cardinal
h3 : b = 0
⊢ a + b = a
rw [h3, add_zero]