-- Mathlib/Data/Nat/Choose/Mul.lean
theorem choose_mul_add {m n : ℕ} (hn : n ≠ 0) :
    (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1)

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)

Tactic:
simp only [hp, add_succ_sub_one]

Result:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)

Tactic:
calc
  (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p+1))! * (p+1)!)
    = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p+1))! * (p+1)! := by ring
  _ = (m * (p+ 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
  _ = ((m * (p+ 1) + p) + 1)! := by ring_nf
  _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
  _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by ring
  _ = ((m * (p + 1) + p).choose p * (m * (p+1))! * (p)!) * ((p + 1) * (m + 1)) := by
    rw [add_choose_mul_factorial_mul_factorial]
  _ = (m * (p + 1) + p).choose p * (m * (p+1))! * (((p + 1) * (p)!) * (m + 1)) := by ring
  _ = (m * (p + 1) + p).choose p * (m * (p+1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
  _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by ring

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!

Tactic:
ring_nf

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))

Tactic:
rw [add_choose_mul_factorial_mul_factorial]

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!

Tactic:
rw [add_choose_mul_factorial_mul_factorial]

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!

Tactic:
rw [factorial_succ]

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
⊢ (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1)

Tactic:
rw [← Nat.mul_left_inj (mul_ne_zero (factorial_ne_zero (m * n)) (factorial_ne_zero n))]

Result:
m n : ℕ
hn : n ≠ 0
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose (n - 1) * ((m * n)! * n !)

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))

Tactic:
ring

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p)! * ((p + 1) * (m + 1))

Tactic:
ring

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)

Tactic:
ring

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!

Tactic:
ring

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose (n - 1) * ((m * n)! * n !)

Tactic:
set p := n - 1

Result:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1))

Tactic:
rw [factorial_succ]

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)

Tactic:
have hp : n = p + 1 := (succ_pred_eq_of_ne_zero hn).symm

Result:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)