M : Type u_1
N : Type ?u.17
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)
M : Type u_1
N : Type ?u.17
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)
rw [antidiagonal_succ, prod_cons, prod_map]
no goals
M : Type u_1
N : Type ?u.17
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)
rfl