Theorem: sum_union_le (Bml/Setsimp.lean)

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

State before:
T : Type u_1
inst✝ : DecidableEq T
X Y : Finset T
F : T → ℕ
⊢ (X ∪ Y).sum F ≤ X.sum F + Y.sum F
Tactic:
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
State after:
no goals

State before:
T : Type u_1
inst✝ : DecidableEq T
X Y : Finset T
F : T → ℕ
⊢ (X ∪ Y).sum F ≤ (X ∪ Y).sum F + (X ∩ Y).sum F
Tactic:
simp
State after:
no goals