Splitting sum with dite

Stream: new members

[Yakov Pechersky]

What's the lemma/definition that can break a sum into the cases that are relevant to the internal ite or dite? My current goal state is:

R : Type u_1,
_inst_1 : field R,
n : ℕ,
i j : fin (n + 2),
h : i ≠ j,
A : matrix (fin (n + 2)) (fin (n + 2)) R,
ix jx : fin (n + 2),
hj : jx = j,
hi : ¬jx = i
⊢ ∑ (x : fin (n + 2)),
      dite (x = j) (λ (h : x = j), ite (ix = i) 1 0)
          (λ (h : ¬x = j), dite (x = i) (λ (h : x = i), ite (ix = j) 1 0) (λ (h : ¬x = i), ite (ix = x) 1 0)) *
        A x j =
    A ix i

[Yakov Pechersky]

The statement being proved is wrong in general (I was left-multiplying by the swap-column matrix instead of right-multiplying), but the question stands.

[Mario Carneiro]

You can usually use split_ifs if you have an ite in the goal, but here it won't work because it's under a binder

[Mario Carneiro]

first you have to figure out what you want to do about the sum

[Yury G. Kudryashov]

See docs#finset.prod_apply_dite