## Stream: new members

### Topic: Splitting sum with dite

#### Yakov Pechersky (Jul 29 2020 at 17:16):

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 (Jul 29 2020 at 17:18):

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 (Jul 29 2020 at 17:33):

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 (Jul 29 2020 at 17:33):

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

#### Yury G. Kudryashov (Jul 30 2020 at 03:50):

Last updated: Dec 20 2023 at 11:08 UTC