M : Type u_1
N : Type ?u.4907
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ f (Prod.swap (0, n + 1)) * ∏ p in antidiagonal n, f (Prod.swap ((Prod.swap p).fst + 1, (Prod.swap p).snd)) =
    f (n + 1, 0) * ∏ p in antidiagonal n, f (p.fst, p.snd + 1)
M : Type u_1
N : Type ?u.4907
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p in antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p in antidiagonal n, f (p.fst, p.snd + 1)
rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap]
no goals
M : Type u_1
N : Type ?u.4907
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ f (Prod.swap (0, n + 1)) * ∏ p in antidiagonal n, f (Prod.swap ((Prod.swap p).fst + 1, (Prod.swap p).snd)) =
    f (n + 1, 0) * ∏ p in antidiagonal n, f (p.fst, p.snd + 1)
rfl