dfinsupp sum ite

Stream: Is there code for X?

[Heather Macbeth]

I couldn't find a dfinsupp analogue of docs#finsupp.sum_ite_self_eq', would anyone like to find it for me or show me how to prove this quickly?

import data.dfinsupp.basic

variables {ι : Type*} [decidable_eq ι] {E : Type*}
  [add_comm_group E]
  {G : ι → Type*}
  [Π (i : ι), add_comm_group (G i)] [Π (i : ι) (x : G i), decidable (x ≠ 0)]

example (W : Π₀ i, G i) (i : ι) :
  W.sum (λ j v, if h : j = i then (eq.rec v h : G i) else 0) = W i :=
sorry

[Yakov Pechersky]

import data.dfinsupp.basic

variables {ι : Type*} [decidable_eq ι] {E : Type*}
  [add_comm_group E]
  {G : ι → Type*}
  [Π (i : ι), add_comm_group (G i)] [Π (i : ι) (x : G i), decidable (x ≠ 0)]

example (W : Π₀ i, G i) (i : ι) :
  W.sum (λ j v, if h : j = i then (eq.rec v h : G i) else 0) = W i :=
by simp [dfinsupp.sum] {contextual := tt}

[Yakov Pechersky]

When in doubt, unfold! (But actually unfolding is usually not the right thing to do. However, I looked at the other dfinsupp.prod proofs in the file, and they also all unfolded.)

[Heather Macbeth]

Ah, this explains a lot, I've had endless pain with dfinsupp in the past from trying to do everything through the API ... I never figured out how to unfold dfinsupp.sum!

[Eric Wieser]

It looks like you want to refold dfinsupp.single there?

[Eric Wieser]

Then the statement is docs#dfinsupp.sum_single

[Heather Macbeth]

I don't see what you mean, sorry? Mine has W i on the RHS, not W.

[Eric Wieser]

Ah you're right

[Eric Wieser]

You could probably get there by pulling the application at i outside the sum and ite, but that's certainly not a direct proof any more