case inl
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ b = c

case inr
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ b = c
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
⊢ b = c
cases' le_or_lt ℵ₀ b with hb hb
case inl
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
case inl
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ b = c
have : a < b := ha.trans_le hb
case inl
a b c : Cardinal
h : a + c = b
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
case inl
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
rw [add_eq_right hb this.le, eq_comm] at h
no goals
case inl
a b c : Cardinal
h : a + c = b
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
rw [eq_of_add_eq_of_aleph0_le h this hb]
case inr
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ b = c
case inr
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ b = c
have hc : c < ℵ₀ := by
  rw [← not_le]
  intro hc
  apply lt_irrefl ℵ₀
  apply (hc.trans (self_le_add_left _ a)).trans_lt
  rw [← h]
  apply add_lt_aleph0 ha hb
case inr
a b c : Cardinal
h : a + b = a + c
ha : ∃ n, a = ↑n
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
⊢ b = c
case inr
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ b = c
rw [lt_aleph0] at *
case inr.intro
b c : Cardinal
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
n : ℕ
h : ↑n + b = ↑n + c
⊢ b = c
case inr
a b c : Cardinal
h : a + b = a + c
ha : ∃ n, a = ↑n
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
⊢ b = c
rcases ha with ⟨n, rfl⟩
case inr.intro.intro
c : Cardinal
hc : ∃ n, c = ↑n
n m : ℕ
h : ↑n + ↑m = ↑n + c
⊢ ↑m = c
case inr.intro
b c : Cardinal
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
n : ℕ
h : ↑n + b = ↑n + c
⊢ b = c
rcases hb with ⟨m, rfl⟩
case inr.intro.intro.intro
n m k : ℕ
h : ↑n + ↑m = ↑n + ↑k
⊢ ↑m = ↑k
case inr.intro.intro
c : Cardinal
hc : ∃ n, c = ↑n
n m : ℕ
h : ↑n + ↑m = ↑n + c
⊢ ↑m = c
rcases hc with ⟨k, rfl⟩
case inr.intro.intro.intro
n m k : ℕ
h : n + m = n + k
⊢ m = k
case inr.intro.intro.intro
n m k : ℕ
h : ↑n + ↑m = ↑n + ↑k
⊢ ↑m = ↑k
norm_cast  at h⊢
no goals
case inr.intro.intro.intro
n m k : ℕ
h : n + m = n + k
⊢ m = k
apply add_left_cancel h
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ ¬ℵ₀ ≤ c
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ c < ℵ₀
rw [← not_le]
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ False
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ ¬ℵ₀ ≤ c
intro hc
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ ℵ₀ < ℵ₀
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ False
apply lt_irrefl ℵ₀
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + c < ℵ₀
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ ℵ₀ < ℵ₀
apply (hc.trans (self_le_add_left _ a)).trans_lt
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + b < ℵ₀
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + c < ℵ₀
rw [← h]
no goals
a b c : Cardinal
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + b < ℵ₀
apply add_lt_aleph0 ha hb