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

case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ c ≤ b
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b = c
apply le_antisymm
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ ¬b < c
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ c ≤ b
rw [← not_lt]
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
⊢ False
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ ¬b < c
intro hb
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
this : a + b < c
⊢ False
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
⊢ False
have : a + b < c := add_lt_of_lt hc ha hb
no goals
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
this : a + b < c
⊢ False
simp [h, lt_irrefl] at this
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ a + b
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ c
rw [← h]
no goals
case a
a b c : Cardinal
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ a + b
apply self_le_add_left