calc
  (X ∪ Y).sum F ≤ (X ∪ Y).sum F + (X ∩ Y).sum F := by simp
  _ = X.sum F + Y.sum F := Finset.sum_union_inter
T : Type u_1
inst✝ : DecidableEq T
X Y : Finset T
F : T → ℕ
⊢ (X ∪ Y).sum F ≤ X.sum F + Y.sum F
no goals