Subst in `Finset.attach` sum

Stream: new members

[Niklas Mohrin]

I am trying to prove the following example:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Combinatorics.SimpleGraph.Basic

open BigOperators

noncomputable section

variable {V : Type*} [Nonempty V] [Fintype V] [DecidableEq V]

def SimpleGraph.edges (G : SimpleGraph V) : Finset (V × V) := sorry

example
    (f : {u v : V} → (u ≠ v) → ℕ)
    (G G' : SimpleGraph V)
    (e₀ : V × V)
    (hG' : G'.edges = G.edges ∪ {e₀})
    (he₀ : e₀ ∈ G'.edges)                       -- Already implied by other arguments, but passed explicitly to keep statement short
    (hne : ∀ {e}, e ∈ G.edges → e.fst ≠ e.snd)  -- Already implied by other arguments, but passed explicitly to keep statement short
    (hne' : ∀ {e}, e ∈ G'.edges → e.fst ≠ e.snd) :
    ∑ e : G'.edges, f (hne' e.prop) = f (hne' he₀) + ∑ e : G.edges, f (hne e.prop) := sorry

(Full context can be found at https://github.com/niklasmohrin/lean-seminar-2023/blob/b645cf3547e88de2d4dbc5c660d8c4e89e5cf000/FlowEquivalentForest/Matrix.lean#L120-L128)

Using rw[hG'] gives motive is not type correct, which makes sense, because the f argument of Finset.sum would change type. So I suppose I would have to use subst somehow, but I can't really get there, because generalize G.edges = G_edges at * somehow gives me hG' : G_edges = G_edges ∪ {e₀} and even if it worked, I also cannot figure out how to prove the reduced version:

example
    (f : {u v : V} → (u ≠ v) → ℕ)
    (s s' : Finset (V × V))
    (e₀ : V × V)
    (hs' : s' = s ∪ {e₀})
    (he₀ : e₀ ∈ s')
    (hne : ∀ {e}, e ∈ s → e.fst ≠ e.snd)  -- Already implied by other arguments, but passed explicitly to keep statement short
    (hne' : ∀ {e}, e ∈ s' → e.fst ≠ e.snd) :
    ∑ e : s', f (hne' e.prop) = f (hne' he₀) + ∑ e : s, f (hne e.prop) := by
  subst hs'
  sorry

I would want to use Finset.sum_insert somehow now, but the types that are being summed are still different. After simp, it is clear that Finset.sum_insert does not apply, because there still is a Finset.attach in there.

Does someone know what I can do?

[Yaël Dillies]

A very powerful tool in this kind of situation is docs#Finset.sum_nbij or docs#Finset.sum_nbij'

[Niklas Mohrin]

Oh interesting. So I would split the s' sum and biject the s part of the s' sum over into the s world?

[Niklas Mohrin]

Hm, it seems a bit tedious to prove bijectivity, maybe I am better off rephrasing everything so that I am not summing Finset (V \times V), but instead a Finset UnequalPair?

[Yaël Dillies]

Possibly. I'm lacking context to give you an informed opinion.