tsum over equivalent (equal) subtypes

Stream: mathlib4

[Peter Nelson]

The following proof isn't too bad, but the change feels awkward. Is there a better way to do this? Or does this indicate a missing API lemma?

import Mathlib.Topology.Algebra.InfiniteSum.Basic

example {α : Type} (P Q : α → Prop) (h_eqv : ∀ a, P a ↔ Q a) (f : α → ℕ) :
    ∑' x : {x // P x}, f x = ∑' x : {x // Q x}, f x := by
  change ∑' x : {x | P x}, _ = ∑' x : {x | Q x}, _
  rw [tsum_congr_subtype]
  simp [h_eqv]

[Eric Wieser]

docs#tsum_congr_subtype is mis-stated, it should be the version you wrote

[Eric Wieser]

(and then maybe the old statement can be moved to tsum_congr_set_coe or similar)

[Peter Nelson]

#9080