a b c : Cardinal
h : b + a = b + c
hb : b < ℵ₀
⊢ a = c
a b c : Cardinal
h : a + b = c + b
hb : b < ℵ₀
⊢ a = c
rw [add_comm a b, add_comm c b] at h
no goals
a b c : Cardinal
h : b + a = b + c
hb : b < ℵ₀
⊢ a = c
exact Cardinal.eq_of_add_eq_add_left h hb