Sum over bijection

Stream: new members

[Bernardo Anibal Subercaseaux Roa]

Hi,
I'm struggling to prove a very simple fact.
My goal looks like:

∑ x : V, G.dist (bm x) v = ∑ u : V, G.dist u v

and I have

bm : V ≃ V

At this point I'd expect a standard theorem to solve the goal; something that says that summing over x : V, with the sum being of the form (g (f x)) and f being a bijective function from V to V, is equal to the sum having been of the form (g x). The closest I found was https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Finprod.html#finsum_eq_of_bijective, if I'm parsing it correctly, but I don't quite know how to use something like this. Any help would be appreciated!

[Aaron Liu]

@loogle Finset.sum, Equiv, Eq

[loogle]

:search: Equiv.sum_comp, Fintype.sum_equiv, and 32 more

[Aaron Liu]

Try docs#Equiv.sum_comp (here ι = κ = V)

[Kevin Buzzard]

(deleted)