no goals
α : Type u_1
β : Type ?u.129077
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s ≤ ncard t ↔ ncard (s \ t) ≤ ncard (t \ s)
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
  inter_comm, add_le_add_iff_left]