no goals
M : Type u_1
N : Type ?u.9475
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → ℕ → M
p : ℕ × ℕ
hp : p ∈ antidiagonal n
⊢ f p n = f p (p.fst + p.snd)
rw [Nat.mem_antidiagonal.1 hp]