sum over bigger finset

Stream: Is there code for X?

[Kevin Buzzard]

Do we not have this? Am I making a meal of it? Should it be s ⊆ t or s \le t?

import tactic

open_locale big_operators

example (α : Type) (s : finset α) (f : α → ℤ) (h : ∀ a, a ∉ s → f a = 0) (t : finset α)
  (hst : s ⊆ t) : ∑ a in s, f a = ∑ b in t, f b :=
begin
  classical,
  rw [← finset.sum_inter_add_sum_diff t s, (finset.inter_eq_right_iff_subset s t).2 hst],
  suffices : ∀ x ∈ t \ s, f x = 0,
  { simp [finset.sum_eq_zero this], },
  -- `finish` now works but that's not allowed any more, right?
  intros x hx,
  apply h,
  rw finset.mem_sdiff at hx,
  exact hx.2,
end

[Yaël Dillies]

docs#finset.sum_subset

[Kevin Buzzard]

Thanks! Why didn't library_search find this?

[Kevin Buzzard]

Oh -- because I misguessed h :-/