intro X Y F
T : Type u_1
inst✝ : DecidableEq T
⊢ ∀ {X Y : Finset T} {F : T → ℕ}, (X ∪ Y).sum F ≤ X.sum F + Y.sum F
T : Type u_1
inst✝ : DecidableEq T
X Y : Finset T
F : T → ℕ
⊢ (X ∪ Y).sum F ≤ X.sum F + Y.sum F