Use proof in ∑ big operator

Stream: general

[Niels Voss]

Is there a way to fill in this sorry?

example : ℕ :=
∑ x in (divisors_antidiagonal 10),
  (have x.1 * x.2 = 10 := sorry, 5)

I'm basically looking for a way to use the proof that x ∈ (divisors_antidiagonal 10) within the body of the big ∑. This situation occurred in a more complicated situation where I was trying to prove that a recursive function terminates, when I was doing a recursive call with the second element of each pair in (divisors_antidiagonal n).erase ⟨1, n⟩