awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
i j : ℕ
rw : (i + j).choose j * i ! * j ! = (i + j).choose j * j ! * (i + j - j)!
rw₁ : (i + j).choose j * i ! * j ! = (i + j).choose j * j ! * i !
rw₂ rw₃ : (i + j).choose j * j ! * i ! = (i + j).choose j * j ! * i !
⊢ (i + j).choose j * i ! * j ! = (i + j)!

Tactic:
rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), Nat.add_sub_cancel_right,
    Nat.mul_right_comm]

Premises used: Nat.add_sub_cancel_right, Nat.mul_right_comm, Nat.le_add_left, Nat.choose_mul_factorial_mul_factorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k ≤ n
rw : k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)
⊢ k ! * (n - k)! ∣ n !

Tactic:
rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]

Premises used: Nat.choose_mul_factorial_mul_factorial, Nat.mul_assoc
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)

Tactic:
Nat.dvd_mul_left _ _

Premises used: Nat.dvd_mul_left
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)

Tactic:
exact Nat.dvd_mul_left _ _

Premises used: Nat.dvd_mul_left
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : i ! * j ! ∣ (i + j)!), i ! * j ! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!

Tactic:
rwa [Nat.add_sub_cancel_left i j] at this

Premises used: Nat.add_sub_cancel_left
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
i j : ℕ
suffices : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!

Tactic:
suffices i ! * (i + j - i)! ∣ (i + j)! by
    rwa [Nat.add_sub_cancel_left i j] at this
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!

Tactic:
factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, Nat.factorial_mul_factorial_dvd_factorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!

Tactic:
exact factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, Nat.factorial_mul_factorial_dvd_factorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k ≤ n
rw : n.choose (n - k) = n ! / (k ! * (n - k)!)
rw₁ : n ! / ((n - k)! * (n - (n - k))!) = n ! / (k ! * (n - k)!)
rw₂ : n ! / ((n - k)! * k !) = n ! / (k ! * (n - k)!)
rw₃ rw₄ : n ! / (k ! * (n - k)!) = n ! / (k ! * (n - k)!)
⊢ n.choose (n - k) = n.choose k

Tactic:
rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _),
    Nat.sub_sub_self hk, Nat.mul_comm]

Premises used: Nat.sub_sub_self, Nat.sub_le, Nat.mul_comm, Nat.choose_eq_factorial_div_factorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n a b : ℕ
h : n = a + b
this : n.choose (n - b) = n.choose b
⊢ (a + b).choose a = (a + b).choose b

Tactic:
rw [h, Nat.add_sub_cancel_right] at this

Premises used: Nat.add_sub_cancel_right
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
rwa rwa₁ rwa₂ rwa₃ : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b

Tactic:
rwa [h]
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n a b : ℕ
h : n = a + b
suffices : n.choose (n - b) = n.choose b
⊢ n.choose a = n.choose b

Tactic:
suffices choose n (n - b) = choose n b by
    rw [h, Nat.add_sub_cancel_right] at this; rwa [h]
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n a b : ℕ
h : n = a + b
⊢ n.choose (n - b) = n.choose b

Tactic:
choose_symm (h ▸ le_add_left _ _)

Premises used: Nat.le_add_left, Eq.rec, Nat.choose_symm, Eq.symm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n a b : ℕ
h : n = a + b
⊢ n.choose (n - b) = n.choose b

Tactic:
exact choose_symm (h ▸ le_add_left _ _)

Premises used: Nat.choose_symm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
a b : ℕ
⊢ (a + b).choose a = (a + b).choose b

Tactic:
choose_symm_of_eq_add rfl

Premises used: rfl, Nat.choose_symm_of_eq_add
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m : ℕ
h : 2 * m + 1 = m + 1 + m
⊢ (2 * m + 1).choose (m + 1) = (2 * m + 1).choose m

Tactic:
apply choose_symm_of_eq_add

Premises used: Nat.choose_symm_of_eq_add
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m : ℕ
h : 2 * m + 1 = 1 + m + m
h₁ : 2 * m + 1 = 1 + (m + m)
h₂ : 1 + 2 * m = 1 + (m + m)
h₃ h₄ : 1 + (m + m) = 1 + (m + m)
⊢ 2 * m + 1 = m + 1 + m

Tactic:
rw [Nat.add_comm m 1, Nat.add_assoc 1 m m, Nat.add_comm (2 * m) 1, Nat.two_mul m]

Premises used: HMul.hMul, Nat.add_assoc, Nat.two_mul, OfNat.ofNat, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
rw : (n + 1) * n.choose k = (n.choose (k + 1) + n.choose k) * (k + 1)
rw₁ : (n + 1) * n.choose k = (n.choose k + n.choose (k + 1)) * (k + 1)
rw₂ : (n + 1) * n.choose k = n.succ.choose k.succ * (k + 1)
rw₃ rw₄ : (n + 1).choose (k + 1) * (k + 1) = n.succ.choose k.succ * (k + 1)
⊢ (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)

Tactic:
rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]

Premises used: Nat.choose, Nat.choose_succ_succ, Nat.add_one_mul_choose_eq, Nat.add_mul, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)

Tactic:
have e : (n + 1) * choose n k = choose n (k + 1) * (k + 1) + choose n k * (k + 1) := by
    rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
rw : (n + 1) * n.choose k - n.choose k * (k + 1) = n.choose k * (n - k)
rw₁ : n.choose k * (n + 1) - n.choose k * (k + 1) = n.choose k * (n - k)
rw₂ : n.choose k * (n + 1 - (k + 1)) = n.choose k * (n - k)
rw₃ rw₄ : n.choose k * (n - k) = n.choose k * (n - k)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)

Tactic:
rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]

Premises used: Nat.mul_sub_left_distrib, Nat.mul_comm, Nat.add_sub_add_right, Nat.sub_eq_of_eq_add
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
rw : (n + 1).choose n + (n + 1).choose n.succ = n + 1 + 1
rw₁ : n + 1 + (n + 1).choose n.succ = n + 1 + 1
rw₂ rw₃ : n + 1 + 1 = n + 1 + 1
⊢ (n + 1 + 1).choose (n + 1) = n + 1 + 1

Tactic:
rw [choose_succ_succ, choose_succ_self_right n, choose_self]

Premises used: Nat.choose_succ_succ, Nat.choose_self
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
⊢ n.choose 0 * (n + 1) = (n + 1).choose 0 * (n + 1 - 0)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
succ : ∀ (hk : k + 1 ≤ n + 1), n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
succ₁ : ∀ (hk : n + 1 < k + 1), n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
obtain hk | hk := le_or_gt (k + 1) (n + 1)

Premises used: le_or_gt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k + 1 ≤ n + 1
succ : n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))
succ₁ : n.choose (k + 1) * (n + 1) = n.choose k * (n + 1 - (k + 1)) + n.choose k.succ * (n + 1 - (k + 1))
succ₂ : n.choose (k + 1) * (n + 1) = n.choose k * (n - k) + n.choose k.succ * (n - k)
succ₃ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n - k)
succ₄ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n.succ - k.succ)
succ₅ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + (n.choose k.succ * n.succ - n.choose k.succ * k.succ)
succ₆ succ₇ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (n + 1)
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
rw [choose_succ_succ, Nat.add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
        Nat.mul_sub_left_distrib, Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)]

Premises used: Nat.mul_sub_left_distrib, Nat.choose_succ_succ, Nat.mul_le_mul_left, Nat.choose_succ_right_eq, Nat.succ_sub_succ, Nat.add_sub_cancel', Nat.add_mul
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : n + 1 < k + 1
succ : n.choose (k + 1) * (n + 1) = 0 * (n + 1 - (k + 1))
succ₁ : 0 * (n + 1) = 0 * (n + 1 - (k + 1))
succ₂ : 0 = 0 * (n + 1 - (k + 1))
succ₃ succ₄ : Eq (α := ℕ) 0 0
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
        Nat.zero_mul]

Premises used: Nat.lt_succ_self, Nat.zero_mul, Nat.choose_eq_zero_of_lt, LT.lt.trans
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
zero : n.choose 0 * (n + 1) = (n + 1).choose 0 * (n + 1 - 0)
succ : ∀ (k : ℕ), n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
⊢ n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)

Tactic:
cases k with
  | zero => simp
  | succ k =>
    obtain hk | hk := le_or_gt (k + 1) (n + 1)
    · rw [choose_succ_succ, Nat.add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
        Nat.mul_sub_left_distrib, Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)]
    · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
        Nat.zero_mul]

Premises used: Nat.mul_sub_left_distrib, Nat.choose_succ_succ, Nat.zero_mul, Nat.choose_succ_right_eq, le_or_gt, HAdd.hAdd, Nat.zero, Nat.succ_sub_succ, OfNat.ofNat, Nat.succ, Nat.add_mul
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
rw : (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose (n - 1) * ((m * n)! * n !)
⊢ (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1)

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

Premises used: HMul.hMul, Nat.mul_ne_zero, Nat.factorial_ne_zero, Nat.mul_left_inj
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
set :
  let p := n - 1;
  (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)
⊢ (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
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
⊢ n = p + 1

Tactic:
have hp : n = p + 1 := (succ_pred_eq_of_ne_zero hn).symm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
simp :
  (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)!)
⊢ (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]

Premises used: Nat.add_succ_sub_one
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
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:
lia
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
rw rw₁ : (m * (p + 1) + (p + 1))! = (m * (p + 1) + (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]

Premises used: Nat.add_choose_mul_factorial_mul_factorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
rw rw₁ : (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
⊢ (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!

Tactic:
rw [factorial_succ]

Premises used: Nat.factorial_succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
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:
lia
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
rw rw₁ : (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p)! * ((p + 1) * (m + 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]

Premises used: Nat.add_choose_mul_factorial_mul_factorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
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:
lia
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
rw rw₁ :
  (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) * p ! * (m + 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]

Premises used: Nat.factorial_succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
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:
lia
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
by :
  (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₁ : (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
by₂ : (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!
by₃ : (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
by₄ : (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p)! * ((p + 1) * (m + 1))
by₅ : (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))
by₆ :
  (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))
by₇ :
  (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))
by₈ :
  (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)!)
⊢ (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 lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((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 lia
    _ = (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 lia

Premises used: Nat.choose, HMul.hMul, HAdd.hAdd, Nat.factorial, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
pos : ∀ (hm : m = 0), (m * n).choose n = m * (m * n - 1).choose (n - 1)
neg : ∀ (hm : ¬m = 0), (m * n).choose n = m * (m * n - 1).choose (n - 1)
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
by_cases hm : m = 0
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
hm : m = 0
pos : 0 < n
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
simp only [hm, Nat.zero_mul, Nat.choose_eq_zero_iff]

Premises used: Nat.choose_eq_zero_iff, Nat.zero_mul
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ 0 < n

Tactic:
Nat.pos_of_ne_zero hn

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ 0 < n

Tactic:
exact Nat.pos_of_ne_zero hn

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
⊢ m = p + 1

Tactic:
have hp : m = p + 1 := (succ_pred_eq_of_ne_zero hm).symm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
neg : ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
simp only [hp]
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
neg : (p * n + 1 * n).choose n = (p + 1) * (p * n + 1 * n - 1).choose (n - 1)
neg₁ : (p * n + n).choose n = (p + 1) * (p * n + n - 1).choose (n - 1)
neg₂ neg₃ : (p + 1) * (p * n + n - 1).choose (n - 1) = (p + 1) * (p * n + n - 1).choose (n - 1)
⊢ ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)

Tactic:
rw [Nat.add_mul, Nat.one_mul, choose_mul_add hn]

Premises used: Nat.one_mul, Nat.add_mul, Nat.choose_mul_add
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
rw : (n + 1).ascFactorial k = (n + k).choose k * k !
⊢ (n + 1).ascFactorial k = k ! * (n + k).choose k

Tactic:
rw [Nat.mul_comm]

Premises used: Nat.mul_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
apply : (n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!
⊢ (n + 1).ascFactorial k = (n + k).choose k * k !

Tactic:
apply Nat.mul_right_cancel (n + k - k).factorial_pos

Premises used: HSub.hSub, Nat.mul_right_cancel, HAdd.hAdd, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
rw : (n + 1).ascFactorial k * (n + k - k)! = (n + k)!
rw₁ : (n + 1).ascFactorial k * n ! = (n + k)!
rw₂ : (n + 1).ascFactorial k * n ! = n ! * (n + 1).ascFactorial k
rw₃ rw₄ : n ! * (n + 1).ascFactorial k = n ! * (n + 1).ascFactorial k
⊢ (n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!

Tactic:
rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
    ← factorial_mul_ascFactorial, Nat.mul_comm]

Premises used: Nat.factorial_mul_ascFactorial, Nat.add_sub_cancel_right, Nat.le_add_left, Nat.choose_mul_factorial_mul_factorial, Nat.mul_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
zero : ascFactorial 0 k = k ! * (0 + k - 1).choose k
succ : ∀ (n : ℕ), (n + 1).ascFactorial k = k ! * (n + 1 + k - 1).choose k
⊢ n.ascFactorial k = k ! * (n + k - 1).choose k

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
zero : ascFactorial 0 0 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
zero₁ : ∀ (n : ℕ), ascFactorial 0 (n + 1) = (n + 1)! * (0 + (n + 1) - 1).choose (n + 1)
⊢ ascFactorial 0 k = k ! * (0 + k - 1).choose k

Tactic:
cases k
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
zero : 1 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
zero₁ : 1 = 0! * 1
zero₂ : 1 = HMul.hMul (α := ℕ) 1 1
zero₃ zero₄ : Eq (α := ℕ) 1 1
⊢ ascFactorial 0 0 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0

Tactic:
rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]

Premises used: Nat.mul_one, Nat.ascFactorial_zero, Nat.factorial_zero, Nat.choose_zero_right
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
⊢ ascFactorial 0 (n + 1) = (n + 1)! * (0 + (n + 1) - 1).choose (n + 1)

Tactic:
simp only [zero_ascFactorial, Nat.zero_add, succ_sub_succ_eq_sub,
        Nat.sub_zero, choose_succ_self, Nat.mul_zero]

Premises used: Nat.zero_ascFactorial, Nat.mul_zero, Nat.sub_zero, Nat.zero_add, Nat.choose_succ_self, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k n : ℕ
succ : k ! * (n + k).choose k = k ! * (n + 1 + k - 1).choose k
⊢ (n + 1).ascFactorial k = k ! * (n + 1 + k - 1).choose k

Tactic:
rw [ascFactorial_eq_factorial_mul_choose]

Premises used: Nat.ascFactorial_eq_factorial_mul_choose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k n : ℕ
⊢ k ! * (n + k).choose k = k ! * (n + 1 + k - 1).choose k

Tactic:
simp only [succ_add_sub_one]

Premises used: Nat.succ_add_sub_one
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ k ! ∣ n.ascFactorial k

Tactic:
⟨(n + k - 1).choose k, ascFactorial_eq_factorial_mul_choose' _ _⟩

Premises used: Nat.choose, HSub.hSub, Nat.ascFactorial_eq_factorial_mul_choose', HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
apply : k ! * (n + k).choose k = k ! * ((n + 1).ascFactorial k / k !)
⊢ (n + k).choose k = (n + 1).ascFactorial k / k !

Tactic:
apply Nat.mul_left_cancel k.factorial_pos

Premises used: Nat.mul_left_cancel, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
rw : (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)
⊢ k ! * (n + k).choose k = k ! * ((n + 1).ascFactorial k / k !)

Tactic:
rw [← ascFactorial_eq_factorial_mul_choose]

Premises used: Nat.ascFactorial_eq_factorial_mul_choose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)

Tactic:
(Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm

Premises used: Nat.factorial_dvd_ascFactorial, Eq.symm, Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)

Tactic:
exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm

Premises used: Nat.factorial_dvd_ascFactorial, Eq.symm, Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ (n + k - 1).choose k = n.ascFactorial k / k !

Tactic:
Nat.eq_div_of_mul_eq_right k.factorial_ne_zero (ascFactorial_eq_factorial_mul_choose' _ _).symm

Premises used: Nat.eq_div_of_mul_eq_right, Nat.ascFactorial_eq_factorial_mul_choose', Nat.factorial_ne_zero, Eq.symm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
inl : ∀ (h : n < k), n.descFactorial k = k ! * n.choose k
inr : ∀ (h : n ≥ k), n.descFactorial k = k ! * n.choose k
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
obtain h | h := Nat.lt_or_ge n k

Premises used: Nat.lt_or_ge
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
h : n < k
inl : 0 = k ! * n.choose k
inl₁ : 0 = k ! * 0
inl₂ inl₃ : Eq (α := ℕ) 0 0
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, Nat.mul_zero]

Premises used: Iff.mpr, Nat.choose_eq_zero_of_lt, Nat.mul_zero, Nat.descFactorial_eq_zero_iff_lt
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
h : n ≥ k
inr : n.descFactorial k = n.choose k * k !
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
rw [Nat.mul_comm]

Premises used: Nat.mul_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
h : n ≥ k
inr : n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!
⊢ n.descFactorial k = n.choose k * k !

Tactic:
apply Nat.mul_right_cancel (n - k).factorial_pos

Premises used: HSub.hSub, Nat.mul_right_cancel, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
h : n ≥ k
inr : n.descFactorial k * (n - k)! = n !
inr₁ : n.descFactorial k * (n - k)! = (n - k)! * n.descFactorial k
inr₂ inr₃ : (n - k)! * n.descFactorial k = (n - k)! * n.descFactorial k
⊢ n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!

Tactic:
rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, Nat.mul_comm]

Premises used: Nat.choose_mul_factorial_mul_factorial, Nat.mul_comm, Nat.factorial_mul_descFactorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ k ! ∣ n.descFactorial k

Tactic:
⟨n.choose k, descFactorial_eq_factorial_mul_choose _ _⟩

Premises used: Nat.choose, Exists.intro, Nat.descFactorial_eq_factorial_mul_choose