finsupp equals sum of `finsupp.filter`

Stream: Is there code for X?

[Andrew Yang]

Is there a good way to prove the lemma below?

import data.finsupp.basic

example {α β γ : Type*} [add_comm_monoid β] (f : α → γ) (x : α →₀ β) {P : (α →₀ β) → Prop}
  (h₁ : ∀ b, P (x.filter (λ a, f a = b)))
  (h₂ : ∀ x y, P x → P y → P (x + y)) : P x :=
begin

end

[Andrew Yang]

I managed to state and proof the statement in the title :

lemma finsupp.sum_image_support_filter {α β γ : Type*}
  [add_comm_monoid β] (f : α → γ) (x : α →₀ β) [decidable_eq γ] :
  ∑ b in finset.image f x.support, x.filter (λ a, f a = b) = x :=
begin
  ext i,
  simp_rw [finsupp.finset_sum_apply, finsupp.filter_apply, finset.sum_ite, finset.sum_const_zero,
    add_zero, finset.filter_eq],
  split_ifs,
  { simp },
  { rw [finset.sum_empty, eq_comm, ← finsupp.not_mem_support_iff],
    exact λ h', h (finset.mem_image_of_mem f h') }
end

Is this not in mathlib? Is there any generalizations?