need help using `sum_erase_eq_sub`

Stream: new members

[Becker A.]

I extract_goal'd this from my work, and replaced the unimportant side of the equation with zero (i.e., this goal is not true, please ignore for now):

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Fin

open Finset BigOperators

theorem sum_sq_eq.extracted_1_1.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  {s : Finset ι}
  {f : ι → ℝ}
  : ∑ i ∈ s, f i * ∑ j ∈ s.erase i, f j = 0
  := by
  conv =>
    enter [1, 2, i]
    rw [sum_erase_eq_sub ?h1]
    case h1 => sorry -- error here
  sorry

I'm running into two issues:

1. conv doesn't seem to be letting me use a placeholder for the input (h : a ∈ s) in docs#Finset.sum_erase_eq_sub. how should I be trying to use sum_erase_eq_sub here?
2. it requires as an input an instance of i ∈ s. I know I should have this since the sum is written ∑ i ∈ s, ..., but I don't seem to have access to this assertion with conv. how do I get access to i ∈ s?

[Aaron Liu]

docs#Finset.sum_congr

[Becker A.]

Aaron Liu said:

docs#Finset.sum_congr

I don't understand, please explain

[Aaron Liu]

it gives you the hypothesis that the element is in the set

[Becker A.]

sorry, I also don't understand how it would do that for me. can you explain that as well?

specifically the result of docs#Finset.sum_congr isn't in the form i ∈ s, it just gives s₁.sum f = s₂.sum g, so idk how I get i ∈ s from it.

[Ruben Van de Velde]

I think you want something like

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Fin

open Finset BigOperators

theorem sum_sq_eq.extracted_1_1.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  {s : Finset ι}
  {f : ι → ℝ}
  : ∑ i ∈ s, f i * ∑ j ∈ s.erase i, f j = 0
  := by
  conv =>
    enter [1]
    apply_congr
    · rfl
    rw [sum_erase_eq_sub (by assumption)]
  sorry

[Ruben Van de Velde]

enter in conv loses the necessary information

[Ruben Van de Velde]

Alternatively, what Aaron was getting at (though not particularly helpfully):

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Fin

open Finset BigOperators

theorem sum_sq_eq.extracted_1_1.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  {s : Finset ι}
  {f : ι → ℝ}
  : ∑ i ∈ s, f i * ∑ j ∈ s.erase i, f j = 0
  := by
  trans ∑ i ∈ s, f i * (∑ j ∈ s, f j - f i)
  · refine Finset.sum_congr rfl fun i hi => ?_
    rw [sum_erase_eq_sub hi]
  sorry

[Aaron Liu]

Oh I didn't know about apply_congr

[Aaron Liu]

this is amazing

[Becker A.]

cool! so what does apply_congr do exactly? I'm trying to find documentation for it and only found something from mathlib3

[Chris Henson]

See docs#Lean.Elab.Tactic.applyCongr for documentation.

[Becker A.]

...okay, still not exactly sure what it does from the docs. basically I need it for docs#Finset.sum (and I guess also Finset.prod)?

[Ruben Van de Velde]

Let me try to explain without the notation- say you have the following goal:

Finset.sum s f = Finset.sum t g

for some sets s t and functions f g. Now without knowing anything about what Finset.sum does, we can make this observation: if s = t and f = g (that is, f x = g x for all x), then certainly Finset.sum s f = Finset.sum t g. This is what enter uses in conv.

Now if you do know what Finset.sum does, clearly this is more than what we need. We can already prove the goal if f x = g x only for those x in s (which must still be equal to t). This is expressed in the lemma docs#Finset.sum_congr , and this is also the fact that apply_congr uses.

There's other situations where the same situation occurs, such as docs#Set.image_congr , but Finset.sum is probably the most common example.

[Jovan Gerbscheid]

I ran into this exact same issue, not knowing about apply_congr. Is there a chance that we could make enter use @[congr] lemmas by default?

This also seems relevant for the new rewriting tactic. @Kyle Miller, do you think it is reasonable that the congruence algorithm used by the new rewrite tactic would use Finset.sum_congr, so that side conditions generated by rewrites under sums will have the extra hypothesis of set membership given by Finset.sum_congr?