n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x in divisors n,
      f
        (↑{ toFun := fun d => (d, n / d),
                inj' :=
                  (_ :
                    ∀ (p₁ p₂ : ℕ),
                      (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                        ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
            x).fst
        (↑{ toFun := fun d => (d, n / d),
                inj' :=
                  (_ :
                    ∀ (p₁ p₂ : ℕ),
                      (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                        ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
            x).snd =
    ∏ i in divisors n, f i (n / i)
n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i in divisorsAntidiagonal n, f i.fst i.snd = ∏ i in divisors n, f i (n / i)
rw [← map_div_right_divisors, Finset.prod_map]
no goals
n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x in divisors n,
      f
        (↑{ toFun := fun d => (d, n / d),
                inj' :=
                  (_ :
                    ∀ (p₁ p₂ : ℕ),
                      (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                        ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
            x).fst
        (↑{ toFun := fun d => (d, n / d),
                inj' :=
                  (_ :
                    ∀ (p₁ p₂ : ℕ),
                      (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                        ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
            x).snd =
    ∏ i in divisors n, f i (n / i)
rfl