-- Mathlib/Data/Nat/Choose/Sum.lean
theorem prod_antidiagonal_pow_choose_succ {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) :
    (∏ ij ∈ antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1) =
      (∏ ij ∈ antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) *
        ∏ ij ∈ antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ ij ∈ antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1 =
    (∏ ij ∈ antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) *
      ∏ ij ∈ antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2

Tactic:
simp only [Nat.prod_antidiagonal_eq_prod_range_succ_mk, prod_pow_choose_succ]

Result:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i =
    (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x) * ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Proof state:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
⊢ f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose (n - i)

Tactic:
rw [choose_symm (this _ hi)]

Result:
no goals

Proof state:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i = ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Tactic:
refine prod_congr rfl fun i hi ↦ ?_

Result:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
⊢ f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose (n - i)

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i =
    (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x) * ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Tactic:
congr 1

Result:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i = ∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x

case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i = ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i =
    (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x) * ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Tactic:
have : ∀ i ∈ range (n + 1), i ≤ n := fun i hi ↦ by simpa [Nat.lt_succ_iff] using hi

Result:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i =
    (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x) * ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Proof state:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i = ∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x

Tactic:
refine prod_congr rfl fun i hi ↦ ?_

Result:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
⊢ f i (n + 1 - i) ^ n.choose i = f i (n - i + 1) ^ n.choose i

Proof state:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
⊢ f i (n + 1 - i) ^ n.choose i = f i (n - i + 1) ^ n.choose i

Tactic:
rw [tsub_add_eq_add_tsub (this _ hi)]

Result:
no goals

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n i : ℕ
hi : i ∈ range (n + 1)
⊢ i ≤ n

Tactic:
simpa [Nat.lt_succ_iff] using hi

Result:
no goals