Proof transfer from antidiagonal to divisors_antidiagonal

Stream: new members

[Sigma]

In the library we have docs#finset.nat.sum_antidiagonal_eq_sum_range_succ and I need to use the analogous statement

variables {M : Type*} [ring M]
lemma div_antidiagonal_eq_sum_divisors (X : ℕ) (func : ℕ × ℕ → M) :
  X.divisors_antidiagonal.sum func =
  finset.sum X.divisors (λ x, func ⟨x, X / x⟩)

I was hoping I could basically copy the proof over, swapping n-k for X / x, but the proof just looks like black magic. I tried printing it and looked to find the important bits, but it refused to typecheck even after I cleaned it up. I tried rewriting it in terms of a product instead of a sum like for the one we have, but it didn't do anything.
I was wondering what I should try next.

[Eric Rodriguez]

import algebra.big_operators.nat_antidiagonal
import number_theory.divisors

open_locale big_operators

variables {M : Type*} [ring M]
lemma div_antidiagonal_eq_sum_divisors (X : ℕ) (func : ℕ × ℕ → M) :
  X.divisors_antidiagonal.sum func =
  ∑ x in X.divisors, func (x, X / x) :=
begin
    convert finset.sum_map _ ⟨λ x, (x, X / x) , λ x y h, (prod.mk.inj h).1⟩ _,
    ext,
    simp,
end

seems to lead to a pretty sensible proof state, and the proof is basically copy-paste; what are you confused about? glad to try and explain if i get it myself ^^