sum ite over fin

Stream: general

[Johan Commelin]

How do I kill off this one?

lemma MWE (R : Type v) [ring R] (n : ℕ) :
finset.univ.sum (λ (k : fin (n + 2)), (-1) ^ k.val * ite (0 = k) (1 : R) (0 : R)) = 1 := sorry

[Chris Hughes]

finset.sum_eq_single

[Kenny Lau]

not found

[Kenny Lau]

import data.fintype

universe v

lemma MWE (R : Type v) [ring R] (n : ℕ) :
finset.univ.sum (λ (k : fin (n + 2)), (-1) ^ k.val * ite (0 = k) (1 : R) (0 : R)) = 1 :=
begin
  transitivity finset.sum (finset.singleton 0 : finset (fin (n+2))) _,
  { symmetry,
    apply finset.sum_subset,
    { intros i H, simp },
    { intros, simp at a, simp [ne.symm a] } },
  simp, refl
end

[Chris Hughes]

It's actually sum_eq_single due to a naming error.

[Kenny Lau]

that's the same thing, and still not found

[Johan Commelin]

@Chris Hughes My Lean still doesn't find it.

[Chris Hughes]

I think it might be new.