chore(Algebra/BigOperators): add to_additive for expectation and antidiagonal lemmas (#42763)

- Add `@[to_additive]` attributes to:
  - `Expect.expect_inv_index`
  - `Nat.prod_antidiagonal_succ`
  - `Nat.prod_antidiagonal_succ'`

- Remove the duplicated additive proofs:
  - `expect_neg_index`
  - `sum_antidiagonal_succ`
  - `sum_antidiagonal_succ'`

Used Aristotle AI to find the duplicates, and verify the change, and ChatGPT, AmazonQ to navigate VS Code, cli, running tests, making the PR, understanding the proof and so forth

Author: attilavjda

Mathlib/Algebra/BigOperators/Expect.lean

@@ -276,12 +276,10 @@ lemma expect_image [DecidableEq ι] {m : κ → ι} (hm : (t : Set κ).InjOn m)
 
 end bij
 
-@[simp] lemma expect_inv_index [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → M) :
+@[to_additive (attr := simp)]
+lemma expect_inv_index [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → M) :
     𝔼 i ∈ s⁻¹, f i = 𝔼 i ∈ s, f i⁻¹ := expect_image inv_injective.injOn
 
-@[simp] lemma expect_neg_index [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → M) :
-    𝔼 i ∈ -s, f i = 𝔼 i ∈ s, f (-i) := expect_image neg_injective.injOn
-
 lemma _root_.map_expect {F : Type*} [FunLike F M N] [LinearMapClass F ℚ≥0 M N]
     (g : F) (f : ι → M) (s : Finset ι) :
     g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i) := by simp only [expect, map_smul, map_sum]

Mathlib/Algebra/BigOperators/NatAntidiagonal.lean

@@ -24,30 +24,24 @@ open HasAntidiagonal
 
 namespace Nat
 
+@[to_additive]
 theorem prod_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → M} :
     (∏ p ∈ antidiagonal (n + 1), f p)
       = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2) := by
   rw [antidiagonal_succ, prod_cons, prod_map]; rfl
 
-theorem sum_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → N} :
-    (∑ p ∈ antidiagonal (n + 1), f p) = f (0, n + 1) + ∑ p ∈ antidiagonal n, f (p.1 + 1, p.2) :=
-  @prod_antidiagonal_succ (Multiplicative N) _ _ _
-
 @[to_additive]
 theorem prod_antidiagonal_swap {n : ℕ} {f : ℕ × ℕ → M} :
     ∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p := by
   conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]
   rfl
 
+@[to_additive]
 theorem prod_antidiagonal_succ' {n : ℕ} {f : ℕ × ℕ → M} : (∏ p ∈ antidiagonal (n + 1), f p) =
     f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1) := by
   rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap]
   rfl
 
-theorem sum_antidiagonal_succ' {n : ℕ} {f : ℕ × ℕ → N} :
-    (∑ p ∈ antidiagonal (n + 1), f p) = f (n + 1, 0) + ∑ p ∈ antidiagonal n, f (p.1, p.2 + 1) :=
-  @prod_antidiagonal_succ' (Multiplicative N) _ _ _
-
 @[to_additive]
 theorem prod_antidiagonal_subst {n : ℕ} {f : ℕ × ℕ → ℕ → M} :
     ∏ p ∈ antidiagonal n, f p n = ∏ p ∈ antidiagonal n, f p (p.1 + p.2) :=