[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p in antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p in antidiagonal n, f (p.fst + 1, p.snd)
[PROOFSTEP]
rw [antidiagonal_succ, prod_cons, prod_map]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x in antidiagonal n,
        f
          (↑(Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl ℕ))
            x) =
    f (0, n + 1) * ∏ p in antidiagonal n, f (p.fst + 1, p.snd)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p in antidiagonal n, f (Prod.swap p) = ∏ p in antidiagonal n, f p
[PROOFSTEP]
conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
| ∏ p in antidiagonal n, f (Prod.swap p)
[PROOFSTEP]
rw [← map_swap_antidiagonal, Finset.prod_map]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
| ∏ p in antidiagonal n, f (Prod.swap p)
[PROOFSTEP]
rw [← map_swap_antidiagonal, Finset.prod_map]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
| ∏ p in antidiagonal n, f (Prod.swap p)
[PROOFSTEP]
rw [← map_swap_antidiagonal, Finset.prod_map]
[GOAL]
M : Type u_1
N : Type u_2
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)
[PROOFSTEP]
rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap]
[GOAL]
M : Type u_1
N : Type u_2
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)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → ℕ → M
p : ℕ × ℕ
hp : p ∈ antidiagonal n
⊢ f p n = f p (p.fst + p.snd)
[PROOFSTEP]
rw [Nat.mem_antidiagonal.1 hp]
