Summing equalities over a Fintype

Stream: Is there code for X?

[Snir Broshi]

Hello, is there a theorem similar to the following:

import Mathlib.Algebra.BigOperators.Group.Finset.Defs

theorem sum_eq_sum
    {ι : Type*} [Fintype ι]
    {A : Type*} [AddCommMonoid A]
    {lhs rhs : ι → A} (h : ∀ i, lhs i = rhs i) :
    ∑ i, lhs i = ∑ i, rhs i := by
  sorry

I found the inductive case in a weird corner of mathlib:

import Mathlib.Algebra.BigOperators.Group.Finset.Defs

#check Mathlib.Tactic.LinearCombination.add_eq_eq

Thanks

[Aaron Liu]

import Mathlib.Algebra.BigOperators.Group.Finset.Defs

theorem sum_eq_sum
    {ι : Type*} [Fintype ι]
    {A : Type*} [AddCommMonoid A]
    {lhs rhs : ι → A} (h : ∀ i, lhs i = rhs i) :
    ∑ i, lhs i = ∑ i, rhs i :=
  congrArg Finset.univ.sum (funext h)

[Aaron Liu]

oh it's docs#Fintype.sum_congr

[Aaron Liu]

import Mathlib.Data.Fintype.BigOperators

theorem sum_eq_sum
    {ι : Type*} [Fintype ι]
    {A : Type*} [AddCommMonoid A]
    {lhs rhs : ι → A} (h : ∀ i, lhs i = rhs i) :
    ∑ i, lhs i = ∑ i, rhs i :=
  Fintype.sum_congr lhs rhs h

[Snir Broshi]

Woah, thanks! Can I ask how did you find those? My search-fu is still weak

[Aaron Liu]

I'll reproduce my search here

[Aaron Liu]

@loogle Finset.univ, Finset.sum, "congr"

[loogle]

:search: Finset.sum_congr_set, Fintype.sum_congr, and 1 more

[Aaron Liu]

It's the second result

[Aaron Liu]

For the other one, is just a simple congruence

[Aaron Liu]

you can also use the congr() syntax like this:

import Mathlib.Algebra.BigOperators.Group.Finset.Defs

theorem sum_eq_sum
    {ι : Type*} [Fintype ι]
    {A : Type*} [AddCommMonoid A]
    {lhs rhs : ι → A} (h : ∀ i, lhs i = rhs i) :
    ∑ i, lhs i = ∑ i, rhs i :=
  congr(∑ i, $(h i))

[Aaron Liu]

I think it actually produces almost the exact same term

[Snir Broshi]

In what sense is it a congruence? I thought the proof would use induction

[Aaron Liu]

well since lhs = rhs

[Aaron Liu]

then ∑ i, lhs i = ∑ i, rhs i just by substituting

[Ruben Van de Velde]

It's simpler because you're summing over the whole type; docs#Fintype.sum_congr is slightly more involved because it only requires equality on the set you're summing over