Split nested sum in cases

Stream: Is there code for X?

[Iván Renison]

Hi, do we have code for doing something like this?

lemma aux (n : ℕ) (f : Fin n → Fin n → ℝ) :
    ∑(i0 : Fin n), ∑(i1 : Fin n), f i0 i1 =
      (∑(i0 : Fin n), ∑(i1 : Fin n), (if i0 ≠ i1 then f i0 i1 else 0)) + (∑(i : Fin n), f i i) :=
  sorry

[Vasilii Nesterov]

You can use Fintype.sum_prod_type' for moving to sums over Fin n × Fin n, then with Finset.sum_add_sum_compl split the LHS into two sums: the diagonal and its completion. For if-then-else there is Finset.sum_ite. The API for Finset.sum is pretty extensive, I'm just using loogle to find relevant lemmas

[Jon Eugster]

my first hacky try resulted in the following. You might easily do better, but might be helpful to see which theorems were used.

import Mathlib

example (n : ℕ) (f : Fin n → Fin n → ℝ) :
    ∑(i₀ : Fin n), ∑(i₁ : Fin n), f i₀ i₁ =
      (∑(i₀ : Fin n), ∑(i₁ : Fin n), (if i₀ ≠ i₁ then f i₀ i₁ else 0)) + (∑(i : Fin n), f i i) := by
  rw [← Finset.sum_add_distrib]
  apply Finset.sum_congr rfl
  intro x hx
  rw [Finset.sum_ite]
  rw [← Finset.sum_add_sum_compl {y | x ≠ y}]
  simp
  conv => rhs; rw [← Finset.sum_singleton (f x ·) x]
  convert rfl
  -- remaining goal: `{x} = {x_1 | x = x_1}`
  -- might be easier than what follows
  ext i
  rw [Finset.mem_singleton]
  rw [Finset.mem_filter]
  exact ⟨(⟨Finset.mem_univ i, ·.symm⟩), (·.2.symm)⟩

[Iván Renison]

Thankyou very much