Sum over fintype to sum over Finset.univ rw

Stream: Is there code for X?

[David Ledvinka]

Is there a lemma that can do this rw?

import Mathlib

example {α β : Type*} [Fintype α] [AddCommMonoid β] {f : α → β} :
    ∑ i : α, f i  = ∑ i ∈ Finset.univ, f i := by rfl

I can't seem to find one.

[Markus Himmel]

I believe these are literally the same term? Could you show an example where you need this lemma?

[Ruben Van de Velde]

Yeah, these are notation for the same thing

[Ruben Van de Velde]

You'll see in the infoview the goal shows as

⊢ ∑ i, f i = ∑ i, f i

[Martin Dvořák]

I thought we want to have rfl lemmas because we don't like to rely on definitional equality.

[Markus Himmel]

This is not a definitional equality, it's a syntactic equality.

[Martin Dvořák]

Ah, thanks a lot for correction!

[David Ledvinka]

Hmm I see, I wasn't able to apply a rw lemma until I changed to the rhs but something else must be going on then, ill try to reduce to a MWE

[David Ledvinka]

Ok its a pain to reduce to a MWE but I figured it out and my change was indeed doing more than I thought, thanks for the help!