Theorem: mchoose_lemma (DividedPowers/ForMathlib/CombinatoricsLemmas.lean)

State before:
m n : ℕ
hn : n ≠ 0
⊢ m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
Tactic:
rw [← zero_lt_iff] at hn
State after:
m n : ℕ
hn : 0 < n
⊢ m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial

State before:
m n : ℕ
hn : 0 < n
⊢ m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
Tactic:
induction' m  with m ih
State after:
case zero
n : ℕ
hn : 0 < n
⊢ Nat.factorial 0 * n.factorial ^ 0 * mchoose 0 n = (0 * n).factorial

case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ (m + 1).factorial * n.factorial ^ (m + 1) * mchoose (m + 1) n = ((m + 1) * n).factorial

State before:
case zero
n : ℕ
hn : 0 < n
⊢ Nat.factorial 0 * n.factorial ^ 0 * mchoose 0 n = (0 * n).factorial
Tactic:
rw [mchoose_zero, mul_one, MulZeroClass.zero_mul, Nat.factorial_zero, pow_zero, mul_one]
State after:
no goals

State before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ (m + 1).factorial * n.factorial ^ (m + 1) * mchoose (m + 1) n = ((m + 1) * n).factorial
Tactic:
have hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n :=
  by
  rw [←
    mul_left_inj' (Nat.mul_ne_zero (Nat.factorial_ne_zero (m * n)) (Nat.factorial_ne_zero n)), ←
    mul_assoc, ← mul_assoc, Nat.add_choose_mul_factorial_mul_factorial, ←
    Nat.mul_factorial_pred hn, mul_comm n _, ← mul_assoc, Nat.add_sub_assoc hn (m * n),
    mul_comm, mul_assoc ((m + 1) * (m * n + (n - 1)).choose (n - 1)), mul_assoc (m + 1), ←
    mul_assoc ((m * n + (n - 1)).choose (n - 1)), Nat.add_choose_mul_factorial_mul_factorial, ←
    Nat.mul_factorial_pred (Nat.add_pos_right _ hn), ← Nat.add_sub_assoc hn (m * n)]
  ring
State after:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1).factorial * n.factorial ^ (m + 1) * mchoose (m + 1) n = ((m + 1) * n).factorial

State before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1).factorial * n.factorial ^ (m + 1) * mchoose (m + 1) n = ((m + 1) * n).factorial
Tactic:
rw [mchoose_succ, Nat.factorial_succ, pow_succ, ← mul_assoc]
State after:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    ((m + 1) * n).factorial

State before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    ((m + 1) * n).factorial
Tactic:
conv_rhs => rw [Nat.succ_mul]
State after:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    (m * n + n).factorial

State before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    (m * n + n).factorial
Tactic:
rw [← Nat.add_choose_mul_factorial_mul_factorial, ← ih, ← hmn]
State after:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    (m + 1) * (m * n + n - 1).choose (n - 1) * (m.factorial * n.factorial ^ m * mchoose m n) * n.factorial

State before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    (m + 1) * (m * n + n - 1).choose (n - 1) * (m.factorial * n.factorial ^ m * mchoose m n) * n.factorial
Tactic:
ring_nf
State after:
no goals

State before:
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
Tactic:
rw [←
  mul_left_inj' (Nat.mul_ne_zero (Nat.factorial_ne_zero (m * n)) (Nat.factorial_ne_zero n)), ←
  mul_assoc, ← mul_assoc, Nat.add_choose_mul_factorial_mul_factorial, ←
  Nat.mul_factorial_pred hn, mul_comm n _, ← mul_assoc, Nat.add_sub_assoc hn (m * n),
  mul_comm, mul_assoc ((m + 1) * (m * n + (n - 1)).choose (n - 1)), mul_assoc (m + 1), ←
  mul_assoc ((m * n + (n - 1)).choose (n - 1)), Nat.add_choose_mul_factorial_mul_factorial, ←
  Nat.mul_factorial_pred (Nat.add_pos_right _ hn), ← Nat.add_sub_assoc hn (m * n)]
State after:
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ n * ((m + 1) * (m * n + n - Nat.succ 0).factorial) = (m * n + n) * (m * n + n - 1).factorial

State before:
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ n * ((m + 1) * (m * n + n - Nat.succ 0).factorial) = (m * n + n) * (m * n + n - 1).factorial
Tactic:
ring
State after:
no goals