expand Finset.sum?

Stream: Is there code for X?

[Edison Xie]

If I have a sum of finset, for example ∑ x : Fin 3, ![a * a - b * b - c * c + 1, 2 * a * b, 2 * a * c] x • Fin.cons j ![1, ↑i] x, how do I expand it into (a * a - b * b - c * c + 1) • 1 + (2 * a * b) • ↑i + (2 * a * c) • j? The lemma I'm trying to prove is:

lemma expand' (D : Type*) (a b c : ℝ) [DivisionRing D] [Algebra ℝ D] (i j : D):
∑ x : Fin 3, ![a * a - b * b - c * c + 1, 2 * a * b, 2 * a * c] x • Fin.cons j ![1, i] x =
  (a * a - b * b - c * c + 1) • 1 + (2 * a * b) • i + (2 * a * c) • j := sorry

[Andrew Yang]

try simp [Fin.sum_univ_three, ← Fin.succ_one_eq_two, -Fin.succ_one_eq_two']

[Andrew Yang]

(and you will find that your lemma is wrong)

[Edison Xie]

thanks for help the lemma was just made up :joy: