Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2020 Aaron Anderson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aaron Anderson

! This file was ported from Lean 3 source module algebra.big_operators.nat_antidiagonal
! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.NatAntidiagonal
import Mathlib.Algebra.BigOperators.Basic

/-!
# Big operators for `NatAntidiagonal`

This file contains theorems relevant to big operators over `Finset.NatAntidiagonal`.
-/

open BigOperators

variable {
M: Type ?u.4904
M 
N: Type ?u.1347
N : 
Type _: Type (?u.1344+1)
Type _} [
CommMonoid: Type ?u.6201 β†’ Type ?u.6201
CommMonoid 
M: Type ?u.2
M] [
AddCommMonoid: Type ?u.4630 β†’ Type ?u.4630
AddCommMonoid 
N: Type ?u.5
N]

namespace Finset

namespace Nat

theorem 
prod_antidiagonal_succ: βˆ€ {n : β„•} {f : β„• Γ— β„• β†’ M}, ∏ p in antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p in antidiagonal n, f (p.fst + 1, p.snd)
prod_antidiagonal_succ {
n: β„•
n : 
β„•: Type
β„•} {
f: β„• Γ— β„• β†’ M
f : 
β„•: Type
β„• Γ— 
β„•: Type
β„• β†’ 
M: Type ?u.14
M} :
    (∏ 
p: ?m.99
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal (
n: β„•
n + 
1: ?m.45
1), 
f: β„• Γ— β„• β†’ M
f 
p: ?m.99
p) = 
f: β„• Γ— β„• β†’ M
f (
0: ?m.134
0, 
n: β„•
n + 
1: ?m.144
1) * ∏ 
p: ?m.187
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal 
n: β„•
n, 
f: β„• Γ— β„• β†’ M
f (
p: ?m.187
p.
1: {Ξ± : Type ?u.197} β†’ {Ξ² : Type ?u.196} β†’ Ξ± Γ— Ξ² β†’ Ξ±
1 + 
1: ?m.201
1, 
p: ?m.187
p.
2: {Ξ± : Type ?u.243} β†’ {Ξ² : Type ?u.242} β†’ Ξ± Γ— Ξ² β†’ Ξ²
2) :=
  
Goals accomplished! πŸ™
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)
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)
M: Type u_1

N: Type ?u.17

inst✝¹: CommMonoid M

inst✝: AddCommMonoid N

n: β„•

f: β„• Γ— β„• β†’ M

∏ p in
    cons (0, n + 1)
      (map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β„•))
        (antidiagonal n))
      (_ :
        ¬(0, n + 1) ∈             map
              (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β„•))
              (antidiagonal n)),
    f p =   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)
M: Type u_1

N: Type ?u.17

inst✝¹: CommMonoid M

inst✝: AddCommMonoid N

n: β„•

f: β„• Γ— β„• β†’ M

f (0, n + 1) *     ∏ x in
      map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β„•))
        (antidiagonal n),
      f 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)
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

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

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)
Goals accomplished! πŸ™

#align finset.nat.prod_antidiagonal_succ 
Finset.Nat.prod_antidiagonal_succ: βˆ€ {M : Type u_1} [inst : CommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ M},
  ∏ p in antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p in antidiagonal n, f (p.fst + 1, p.snd)
Finset.Nat.prod_antidiagonal_succ

theorem 
sum_antidiagonal_succ: βˆ€ {n : β„•} {f : β„• Γ— β„• β†’ N}, βˆ‘ p in antidiagonal (n + 1), f p = f (0, n + 1) + βˆ‘ p in antidiagonal n, f (p.fst + 1, p.snd)
sum_antidiagonal_succ {
n: β„•
n : 
β„•: Type
β„•} {
f: β„• Γ— β„• β†’ N
f : 
β„•: Type
β„• Γ— 
β„•: Type
β„• β†’ 
N: Type ?u.1347
N} :
    (βˆ‘ 
p: ?m.1429
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal (
n: β„•
n + 
1: ?m.1375
1), 
f: β„• Γ— β„• β†’ N
f 
p: ?m.1429
p) = 
f: β„• Γ— β„• β†’ N
f (
0: ?m.1462
0, 
n: β„•
n + 
1: ?m.1472
1) + βˆ‘ 
p: ?m.1515
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal 
n: β„•
n, 
f: β„• Γ— β„• β†’ N
f (
p: ?m.1515
p.
1: {Ξ± : Type ?u.1525} β†’ {Ξ² : Type ?u.1524} β†’ Ξ± Γ— Ξ² β†’ Ξ±
1 + 
1: ?m.1529
1, 
p: ?m.1515
p.
2: {Ξ± : Type ?u.1571} β†’ {Ξ² : Type ?u.1570} β†’ Ξ± Γ— Ξ² β†’ Ξ²
2) :=
  @
prod_antidiagonal_succ: βˆ€ {M : Type ?u.2309} [inst : CommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ M},
  ∏ p in antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p in antidiagonal n, f (p.fst + 1, p.snd)
prod_antidiagonal_succ (
Multiplicative: Type ?u.2310 β†’ Type ?u.2310
Multiplicative 
N: Type ?u.1347
N) _ 
_: β„•
_ 
_: β„• Γ— β„• β†’ Multiplicative N
_
#align finset.nat.sum_antidiagonal_succ 
Finset.Nat.sum_antidiagonal_succ: βˆ€ {N : Type u_1} [inst : AddCommMonoid N] {n : β„•} {f : β„• Γ— β„• β†’ N},
  βˆ‘ p in antidiagonal (n + 1), f p = f (0, n + 1) + βˆ‘ p in antidiagonal n, f (p.fst + 1, p.snd)
Finset.Nat.sum_antidiagonal_succ

@[
to_additive: βˆ€ {M : Type u_1} [inst : AddCommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ M},
  βˆ‘ p in antidiagonal n, f (Prod.swap p) = βˆ‘ p in antidiagonal n, f p
to_additive]
theorem 
prod_antidiagonal_swap: βˆ€ {M : Type u_1} [inst : CommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ M},
  ∏ p in antidiagonal n, f (Prod.swap p) = ∏ p in antidiagonal n, f p
prod_antidiagonal_swap {
n: β„•
n : 
β„•: Type
β„•} {
f: β„• Γ— β„• β†’ M
f : 
β„•: Type
β„• Γ— 
β„•: Type
β„• β†’ 
M: Type ?u.4621
M} :
    (∏ 
p: ?m.4650
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal 
n: β„•
n, 
f: β„• Γ— β„• β†’ M
f 
p: ?m.4650
p.
swap: {Ξ± : Type ?u.4653} β†’ {Ξ² : Type ?u.4652} β†’ Ξ± Γ— Ξ² β†’ Ξ² Γ— Ξ±
swap) = ∏ 
p: ?m.4683
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal 
n: β„•
n, 
f: β„• Γ— β„• β†’ M
f 
p: ?m.4683
p := 
Goals accomplished! πŸ™
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
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
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)
M: Type u_1

N: Type ?u.4624

inst✝¹: CommMonoid M

inst✝: AddCommMonoid N

n: β„•

f: β„• Γ— β„• β†’ M

∏ p in map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (antidiagonal n), f (Prod.swap p)
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)
M: Type u_1

N: Type ?u.4624

inst✝¹: CommMonoid M

inst✝: AddCommMonoid N

n: β„•

f: β„• Γ— β„• β†’ M

∏ x in antidiagonal n, f (Prod.swap (↑{ toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } x))
M: Type u_1

N: Type ?u.4624

inst✝¹: CommMonoid M

inst✝: AddCommMonoid N

n: β„•

f: β„• Γ— β„• β†’ M

∏ x in antidiagonal n, f (Prod.swap (↑{ toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } x))

#align finset.nat.prod_antidiagonal_swap 
Finset.Nat.prod_antidiagonal_swap: βˆ€ {M : Type u_1} [inst : CommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ M},
  ∏ p in antidiagonal n, f (Prod.swap p) = ∏ p in antidiagonal n, f p
Finset.Nat.prod_antidiagonal_swap
#align finset.nat.sum_antidiagonal_swap 
Finset.Nat.sum_antidiagonal_swap: βˆ€ {M : Type u_1} [inst : AddCommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ M},
  βˆ‘ p in antidiagonal n, f (Prod.swap p) = βˆ‘ p in antidiagonal n, f p
Finset.Nat.sum_antidiagonal_swap

theorem 
prod_antidiagonal_succ': βˆ€ {n : β„•} {f : β„• Γ— β„• β†’ M}, ∏ p in antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p in antidiagonal n, f (p.fst, p.snd + 1)
prod_antidiagonal_succ' {
n: β„•
n : 
β„•: Type
β„•} {
f: β„• Γ— β„• β†’ M
f : 
β„•: Type
β„• Γ— 
β„•: Type
β„• β†’ 
M: Type ?u.4904
M} : (∏ 
p: ?m.4989
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal (
n: β„•
n + 
1: ?m.4935
1), 
f: β„• Γ— β„• β†’ M
f 
p: ?m.4989
p) =
    
f: β„• Γ— β„• β†’ M
f (
n: β„•
n + 
1: ?m.5027
1, 
0: ?m.5064
0) * ∏ 
p: ?m.5077
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal 
n: β„•
n, 
f: β„• Γ— β„• β†’ M
f (
p: ?m.5077
p.
1: {Ξ± : Type ?u.5084} β†’ {Ξ² : Type ?u.5083} β†’ Ξ± Γ— Ξ² β†’ Ξ±
1, 
p: ?m.5077
p.
2: {Ξ± : Type ?u.5091} β†’ {Ξ² : Type ?u.5090} β†’ Ξ± Γ— Ξ² β†’ Ξ²
2 + 
1: ?m.5095
1) := 
Goals accomplished! πŸ™
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)
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)
M: Type u_1

N: Type ?u.4907

inst✝¹: CommMonoid M

inst✝: AddCommMonoid N

n: β„•

f: β„• Γ— β„• β†’ M

∏ p in antidiagonal (n + 1), f (Prod.swap p) = 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)
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 (p.fst + 1, 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)
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

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)
Goals accomplished! πŸ™

#align finset.nat.prod_antidiagonal_succ' 
Finset.Nat.prod_antidiagonal_succ': βˆ€ {M : Type u_1} [inst : CommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ M},
  ∏ p in antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p in antidiagonal n, f (p.fst, p.snd + 1)
Finset.Nat.prod_antidiagonal_succ'

theorem 
sum_antidiagonal_succ': βˆ€ {n : β„•} {f : β„• Γ— β„• β†’ N}, βˆ‘ p in antidiagonal (n + 1), f p = f (n + 1, 0) + βˆ‘ p in antidiagonal n, f (p.fst, p.snd + 1)
sum_antidiagonal_succ' {
n: β„•
n : 
β„•: Type
β„•} {
f: β„• Γ— β„• β†’ N
f : 
β„•: Type
β„• Γ— 
β„•: Type
β„• β†’ 
N: Type ?u.6198
N} :
    (βˆ‘ 
p: ?m.6280
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal (
n: β„•
n + 
1: ?m.6226
1), 
f: β„• Γ— β„• β†’ N
f 
p: ?m.6280
p) = 
f: β„• Γ— β„• β†’ N
f (
n: β„•
n + 
1: ?m.6316
1, 
0: ?m.6353
0) + βˆ‘ 
p: ?m.6366
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal 
n: β„•
n, 
f: β„• Γ— β„• β†’ N
f (
p: ?m.6366
p.
1: {Ξ± : Type ?u.6373} β†’ {Ξ² : Type ?u.6372} β†’ Ξ± Γ— Ξ² β†’ Ξ±
1, 
p: ?m.6366
p.
2: {Ξ± : Type ?u.6380} β†’ {Ξ² : Type ?u.6379} β†’ Ξ± Γ— Ξ² β†’ Ξ²
2 + 
1: ?m.6384
1) :=
  @
prod_antidiagonal_succ': βˆ€ {M : Type ?u.7160} [inst : CommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ M},
  ∏ p in antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p in antidiagonal n, f (p.fst, p.snd + 1)
prod_antidiagonal_succ' (
Multiplicative: Type ?u.7161 β†’ Type ?u.7161
Multiplicative 
N: Type ?u.6198
N) _ 
_: β„•
_ 
_: β„• Γ— β„• β†’ Multiplicative N
_
#align finset.nat.sum_antidiagonal_succ' 
Finset.Nat.sum_antidiagonal_succ': βˆ€ {N : Type u_1} [inst : AddCommMonoid N] {n : β„•} {f : β„• Γ— β„• β†’ N},
  βˆ‘ p in antidiagonal (n + 1), f p = f (n + 1, 0) + βˆ‘ p in antidiagonal n, f (p.fst, p.snd + 1)
Finset.Nat.sum_antidiagonal_succ'

@[
to_additive: βˆ€ {M : Type u_1} [inst : AddCommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ β„• β†’ M},
  βˆ‘ p in antidiagonal n, f p n = βˆ‘ p in antidiagonal n, f p (p.fst + p.snd)
to_additive]
theorem 
prod_antidiagonal_subst: βˆ€ {M : Type u_1} [inst : CommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ β„• β†’ M},
  ∏ p in antidiagonal n, f p n = ∏ p in antidiagonal n, f p (p.fst + p.snd)
prod_antidiagonal_subst {
n: β„•
n : 
β„•: Type
β„•} {
f: β„• Γ— β„• β†’ β„• β†’ M
f : 
β„•: Type
β„• Γ— 
β„•: Type
β„• β†’ 
β„•: Type
β„• β†’ 
M: Type ?u.9472
M} :
    (∏ 
p: ?m.9503
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal 
n: β„•
n, 
f: β„• Γ— β„• β†’ β„• β†’ M
f 
p: ?m.9503
p 
n: β„•
n) = ∏ 
p: ?m.9527
p in 
antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
antidiagonal 
n: β„•
n, 
f: β„• Γ— β„• β†’ β„• β†’ M
f 
p: ?m.9527
p (
p: ?m.9527
p.
1: {Ξ± : Type ?u.9533} β†’ {Ξ² : Type ?u.9532} β†’ Ξ± Γ— Ξ² β†’ Ξ±
1 + 
p: ?m.9527
p.
2: {Ξ± : Type ?u.9539} β†’ {Ξ² : Type ?u.9538} β†’ Ξ± Γ— Ξ² β†’ Ξ²
2) :=
  
prod_congr: βˆ€ {Ξ² : Type ?u.9586} {Ξ± : Type ?u.9585} {s₁ sβ‚‚ : Finset Ξ±} {f g : Ξ± β†’ Ξ²} [inst : CommMonoid Ξ²],
  s₁ = sβ‚‚ β†’ (βˆ€ (x : Ξ±), x ∈ sβ‚‚ β†’ f x = g x) β†’ Finset.prod s₁ f = Finset.prod sβ‚‚ g
prod_congr 
rfl: βˆ€ {Ξ± : Sort ?u.9630} {a : Ξ±}, a = a
rfl fun 
p: ?m.9637
p 
hp: ?m.9640
hp ↦ 
Goals accomplished! πŸ™
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)
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)
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 n
Goals accomplished! πŸ™

#align finset.nat.prod_antidiagonal_subst 
Finset.Nat.prod_antidiagonal_subst: βˆ€ {M : Type u_1} [inst : CommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ β„• β†’ M},
  ∏ p in antidiagonal n, f p n = ∏ p in antidiagonal n, f p (p.fst + p.snd)
Finset.Nat.prod_antidiagonal_subst
#align finset.nat.sum_antidiagonal_subst 
Finset.Nat.sum_antidiagonal_subst: βˆ€ {M : Type u_1} [inst : AddCommMonoid M] {n : β„•} {f : β„• Γ— β„• β†’ β„• β†’ M},
  βˆ‘ p in antidiagonal n, f p n = βˆ‘ p in antidiagonal n, f p (p.fst + p.snd)
Finset.Nat.sum_antidiagonal_subst

@[
to_additive: βˆ€ {M : Type u_1} [inst : AddCommMonoid M] (f : β„• Γ— β„• β†’ M) (n : β„•),
  βˆ‘ ij in antidiagonal n, f ij = βˆ‘ k in range (Nat.succ n), f (k, n - k)
to_additive]
theorem 
prod_antidiagonal_eq_prod_range_succ_mk: βˆ€ {M : Type u_1} [inst : CommMonoid M] (f : β„• Γ— β„• β†’ M) (n : β„•),
  ∏ ij in antidiagonal n, f ij = ∏ k in range (Nat.succ n), f (k, n - k)
prod_antidiagonal_eq_prod_range_succ_mk {
M: Type ?u.9733
M : 
Type _: Type (?u.9733+1)
Type _} [
CommMonoid: Type ?u.9736 β†’ Type ?u.9736
CommMonoid 
M: Type ?u.9733
M] (
f: β„• Γ— β„• β†’ M
f : 
β„•: Type
β„• Γ— 
β„•: Type
β„• β†’ 
M: Type ?u.9733
M)
    (
n: β„•
n : 
β„•: Type
β„•) : (∏ 
ij: ?m.9756
ij in 
Finset.Nat.antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
Finset.Nat.antidiagonal 
n: β„•
n, 
f: β„• Γ— β„• β†’ M
f 
ij: ?m.9756
ij) = ∏ 
k: ?m.9781
k in 
range: β„• β†’ Finset β„•
range 
n: β„•
n.
succ: β„• β†’ β„•
succ, 
f: β„• Γ— β„• β†’ M
f (
k: ?m.9781
k, 
n: β„•
n - 
k: ?m.9781
k) :=
  
Finset.prod_map: βˆ€ {Ξ² : Type ?u.9841} {Ξ± : Type ?u.9840} {Ξ³ : Type ?u.9839} [inst : CommMonoid Ξ²] (s : Finset Ξ±) (e : Ξ± β†ͺ Ξ³) (f : Ξ³ β†’ Ξ²),
  ∏ x in map e s, f x = ∏ x in s, f (↑e x)
Finset.prod_map (
range: β„• β†’ Finset β„•
range 
n: β„•
n.
succ: β„• β†’ β„•
succ) ⟨fun 
i: ?m.9859
i ↦ (
i: ?m.9859
i, 
n: β„•
n - 
i: ?m.9859
i), fun 
_: ?m.9904
_ 
_: ?m.9907
_ 
h: ?m.9910
h ↦ (
Prod.mk.inj: βˆ€ {Ξ± : Type ?u.9913} {Ξ² : Type ?u.9912} {fst : Ξ±} {snd : Ξ²} {fst_1 : Ξ±} {snd_1 : Ξ²},
  (fst, snd) = (fst_1, snd_1) β†’ fst = fst_1 ∧ snd = snd_1
Prod.mk.inj 
h: ?m.9910
h).
1: βˆ€ {a b : Prop}, a ∧ b β†’ a
1⟩ 
f: β„• Γ— β„• β†’ M
f
#align finset.nat.prod_antidiagonal_eq_prod_range_succ_mk 
Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk: βˆ€ {M : Type u_1} [inst : CommMonoid M] (f : β„• Γ— β„• β†’ M) (n : β„•),
  ∏ ij in antidiagonal n, f ij = ∏ k in range (Nat.succ n), f (k, n - k)
Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk
#align finset.nat.sum_antidiagonal_eq_sum_range_succ_mk 
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk: βˆ€ {M : Type u_1} [inst : AddCommMonoid M] (f : β„• Γ— β„• β†’ M) (n : β„•),
  βˆ‘ ij in antidiagonal n, f ij = βˆ‘ k in range (Nat.succ n), f (k, n - k)
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk

/-- This lemma matches more generally than `Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk` when
using `rw ←`. -/
@[
to_additive: βˆ€ {M : Type u_1} [inst : AddCommMonoid M] (f : β„• β†’ β„• β†’ M) (n : β„•),
  βˆ‘ ij in antidiagonal n, f ij.fst ij.snd = βˆ‘ k in range (Nat.succ n), f k (n - k)
to_additive "This lemma matches more generally than
`Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk` when using `rw ←`."]
theorem 
prod_antidiagonal_eq_prod_range_succ: βˆ€ {M : Type u_1} [inst : CommMonoid M] (f : β„• β†’ β„• β†’ M) (n : β„•),
  ∏ ij in antidiagonal n, f ij.fst ij.snd = ∏ k in range (Nat.succ n), f k (n - k)
prod_antidiagonal_eq_prod_range_succ {
M: Type u_1
M : 
Type _: Type (?u.10073+1)
Type _} [
CommMonoid: Type ?u.10076 β†’ Type ?u.10076
CommMonoid 
M: Type ?u.10073
M] (
f: β„• β†’ β„• β†’ M
f : 
β„•: Type
β„• β†’ 
β„•: Type
β„• β†’ 
M: Type ?u.10073
M) (
n: β„•
n : 
β„•: Type
β„•) :
    (∏ 
ij: ?m.10096
ij in 
Finset.Nat.antidiagonal: β„• β†’ Finset (β„• Γ— β„•)
Finset.Nat.antidiagonal 
n: β„•
n, 
f: β„• β†’ β„• β†’ M
f 
ij: ?m.10096
ij.
1: {Ξ± : Type ?u.10099} β†’ {Ξ² : Type ?u.10098} β†’ Ξ± Γ— Ξ² β†’ Ξ±
1 
ij: ?m.10096
ij.
2: {Ξ± : Type ?u.10105} β†’ {Ξ² : Type ?u.10104} β†’ Ξ± Γ— Ξ² β†’ Ξ²
2) = ∏ 
k: ?m.10131
k in 
range: β„• β†’ Finset β„•
range 
n: β„•
n.
succ: β„• β†’ β„•
succ, 
f: β„• β†’ β„• β†’ M
f 
k: ?m.10131
k (
n: β„•
n - 
k: ?m.10131
k) :=
  
prod_antidiagonal_eq_prod_range_succ_mk: βˆ€ {M : Type ?u.10183} [inst : CommMonoid M] (f : β„• Γ— β„• β†’ M) (n : β„•),
  ∏ ij in antidiagonal n, f ij = ∏ k in range (Nat.succ n), f (k, n - k)
prod_antidiagonal_eq_prod_range_succ_mk 
_: β„• Γ— β„• β†’ ?m.10184
_ 
_: β„•
_
#align finset.nat.prod_antidiagonal_eq_prod_range_succ 
Finset.Nat.prod_antidiagonal_eq_prod_range_succ: βˆ€ {M : Type u_1} [inst : CommMonoid M] (f : β„• β†’ β„• β†’ M) (n : β„•),
  ∏ ij in antidiagonal n, f ij.fst ij.snd = ∏ k in range (Nat.succ n), f k (n - k)
Finset.Nat.prod_antidiagonal_eq_prod_range_succ
#align finset.nat.sum_antidiagonal_eq_sum_range_succ 
Finset.Nat.sum_antidiagonal_eq_sum_range_succ: βˆ€ {M : Type u_1} [inst : AddCommMonoid M] (f : β„• β†’ β„• β†’ M) (n : β„•),
  βˆ‘ ij in antidiagonal n, f ij.fst ij.snd = βˆ‘ k in range (Nat.succ n), f k (n - k)
Finset.Nat.sum_antidiagonal_eq_sum_range_succ
end Nat

end Finset