R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    (∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x) *
      ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ ij in Nat.antidiagonal (n + 1), f ij.fst ij.snd ^ Nat.choose (n + 1) ij.fst =
    (∏ ij in Nat.antidiagonal n, f ij.fst (ij.snd + 1) ^ Nat.choose n ij.fst) *
      ∏ ij in Nat.antidiagonal n, f (ij.fst + 1) ij.snd ^ Nat.choose n ij.snd
simp only [Nat.prod_antidiagonal_eq_prod_range_succ_mk, prod_pow_choose_succ]
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    (∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x) *
      ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    (∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x) *
      ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
have : ∀ i ∈ range (n + 1), i ≤ n := fun i hi ↦ by simpa [Nat.lt_succ_iff] using hi
case e_a
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i = ∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x

case e_a
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    (∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x) *
      ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
congr 1
no goals
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n i : ℕ
hi : i ∈ range (n + 1)
⊢ i ≤ n
simpa [Nat.lt_succ_iff] using hi
case e_a
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
i : ℕ
hi : i ∈ range (succ n)
⊢ f i (n + 1 - i) ^ Nat.choose n i = f i (n - i + 1) ^ Nat.choose n i
case e_a
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i = ∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x
refine prod_congr rfl fun i hi ↦ ?_
no goals
case e_a
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
i : ℕ
hi : i ∈ range (succ n)
⊢ f i (n + 1 - i) ^ Nat.choose n i = f i (n - i + 1) ^ Nat.choose n i
rw [tsub_add_eq_add_tsub (this _ hi)]
case e_a
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
i : ℕ
hi : i ∈ range (succ n)
⊢ f (i + 1) (n - i) ^ Nat.choose n i = f (i + 1) (n - i) ^ Nat.choose n (n - i)
case e_a
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
refine prod_congr rfl fun i hi ↦ ?_
no goals
case e_a
R✝ : Type ?u.321125
M✝ : Type ?u.321128
R : Type ?u.321131
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
i : ℕ
hi : i ∈ range (succ n)
⊢ f (i + 1) (n - i) ^ Nat.choose n i = f (i + 1) (n - i) ^ Nat.choose n (n - i)
rw [Nat.choose_symm (this _ hi)]