no goals
M : Type u_1
N : Type ?u.4624
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p in antidiagonal n, f (Prod.swap p) = ∏ p in antidiagonal n, f p
conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]