sum over single element

Stream: Is there code for X?

[Jenkin]

I am trying to prove the following but I am not sure how

import Mathlib

variable {m : Type} [Fintype m] [Nonempty m] [DecidableEq m] (N : Matrix m m ℂ)

example {i : m × m} :
∑ x ∈ { x : m × m | x.1 = x.2 } with i.2 = x.2, N i.1 x.1 = N i.1 i.2 := by
  sorry

any pointers welcome!

[Kenny Lau]

import Mathlib

variable {m : Type} [Fintype m] [Nonempty m] [DecidableEq m] (N : Matrix m m ℂ)

example {i : m × m} :
    ∑ x ∈ { x : m × m | x.1 = x.2 } with i.2 = x.2, N i.1 x.1 = N i.1 i.2 := by
  convert Finset.sum_singleton _ _ using 2

[Jenkin]

I tried viewing this in the LEAN4 playground but there were unsolved goals

⊢ {x ∈ {x | x.1 = x.2} | i.2 = x.2} = {?convert_5}

[Aaron Liu]

import Mathlib

variable {m : Type} [Fintype m] [Nonempty m] [DecidableEq m] (N : Matrix m m ℂ)

example {i : m × m} :
    ∑ x ∈ { x : m × m | x.1 = x.2 } with i.2 = x.2, N i.1 x.1 = N i.1 i.2 := by
  rw [Finset.sum_filter, Finset.sum_filter]
  conv =>
    enter [1, 2, a]
    equals if (i.2, i.2) = a then N i.1 i.2 else 0 =>
      grind
  simp

[Kenny Lau]

Jenkin said:

there were unsolved goals

you said pointers