case A
R✝ : Type ?u.210813
M✝ : Type ?u.210816
R : Type ?u.210819
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i

R✝ : Type ?u.210813
M✝ : Type ?u.210816
R : Type ?u.210819
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
⊢ ∏ i in range (n + 2), f i (n + 1 - i) ^ Nat.choose (n + 1) i =
    (∏ 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
R✝ : Type ?u.210813
M✝ : Type ?u.210816
R : Type ?u.210819
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i in range (n + 2), f i (n + 1 - i) ^ Nat.choose (n + 1) i =
    (∏ 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
have A : (∏ i in range (n + 1), f (i + 1) (n - i) ^ (n.choose (i + 1))) * f 0 (n + 1) =
  ∏ i in range (n + 1), f i (n + 1 - i) ^ (n.choose i)
R✝ : Type ?u.210813
M✝ : Type ?u.210816
R : Type ?u.210819
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
⊢ (∏ k in range (n + 1), f (k + 1) (n + 1 - (k + 1)) ^ Nat.choose (n + 1) (k + 1)) *
      f 0 (n + 1 - 0) ^ Nat.choose (n + 1) 0 =
    (∏ 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
R✝ : Type ?u.210813
M✝ : Type ?u.210816
R : Type ?u.210819
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
⊢ ∏ i in range (n + 2), f i (n + 1 - i) ^ Nat.choose (n + 1) i =
    (∏ 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
rw [prod_range_succ']
no goals
R✝ : Type ?u.210813
M✝ : Type ?u.210816
R : Type ?u.210819
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
⊢ (∏ k in range (n + 1), f (k + 1) (n + 1 - (k + 1)) ^ Nat.choose (n + 1) (k + 1)) *
      f 0 (n + 1 - 0) ^ Nat.choose (n + 1) 0 =
    (∏ 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
simpa [Nat.choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using mul_comm _ _
case A
R✝ : Type ?u.210813
M✝ : Type ?u.210816
R : Type ?u.210819
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x in range n, f (x + 1) (n - x) ^ Nat.choose n (x + 1)) * f (n + 1) (n - n) ^ Nat.choose n (n + 1) * f 0 (n + 1) =
    (∏ k in range n, f (k + 1) (n + 1 - (k + 1)) ^ Nat.choose n (k + 1)) * f 0 (n + 1 - 0) ^ Nat.choose n 0
case A
R✝ : Type ?u.210813
M✝ : Type ?u.210816
R : Type ?u.210819
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
rw [prod_range_succ, prod_range_succ']
no goals
case A
R✝ : Type ?u.210813
M✝ : Type ?u.210816
R : Type ?u.210819
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x in range n, f (x + 1) (n - x) ^ Nat.choose n (x + 1)) * f (n + 1) (n - n) ^ Nat.choose n (n + 1) * f 0 (n + 1) =
    (∏ k in range n, f (k + 1) (n + 1 - (k + 1)) ^ Nat.choose n (k + 1)) * f 0 (n + 1 - 0) ^ Nat.choose n 0
simp