awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
l k n' : ℕ
succ : (n' + l)! * (n' + (l + 1)).ascFactorial k = (n' + (l + k))!
succ₁ : (n' + l)! * (n' + l + 1).ascFactorial k = (n' + (l + k))!
succ₂ : (n' + l + k)! = (n' + (l + k))!
succ₃ succ₄ : (n' + (l + k))! = (n' + (l + k))!
⊢ (n' + l)! * (n' + (1 + l)).ascFactorial k = (n' + (l + k))!

Tactic:
rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]

Premises used: Nat.factorial_mul_ascFactorial, Nat.add_assoc, OfNat.ofNat, Nat.add_comm
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n l k : ℕ
zero : ascFactorial 0 l * (0 + l).ascFactorial k = ascFactorial 0 (l + k)
succ : ∀ (n' : ℕ), (n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k = (n' + 1).ascFactorial (l + k)
⊢ n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k)

Tactic:
cases n with
  | zero =>
    cases l
    · simp only [ascFactorial_zero, Nat.add_zero, Nat.one_mul, Nat.zero_add]
    · simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]
  | succ n' =>
    apply Nat.mul_left_cancel (factorial_pos n')
    simp only [Nat.add_assoc, ← Nat.mul_assoc, factorial_mul_ascFactorial]
    rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]

Premises used: Nat.factorial_mul_ascFactorial, Nat.ascFactorial_zero, Nat.mul_assoc, Nat.zero_mul, Nat.zero_ascFactorial, Nat.add_assoc, Nat.zero, Nat.add_zero, Nat.zero_add, OfNat.ofNat, Nat.succ, Nat.one_mul, Nat.add_right_comm, Nat.add_comm
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ (n + 1).ascFactorial k = (n + k)! / n !

Tactic:
Nat.eq_div_of_mul_eq_right n.factorial_ne_zero (factorial_mul_ascFactorial _ _)

Premises used: Nat.factorial_mul_ascFactorial, Nat.eq_div_of_mul_eq_right, Nat.factorial_ne_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : 0 < n
⊢ n.ascFactorial k = (n + k - 1)! / (n - 1)!

Tactic:
Nat.eq_div_of_mul_eq_right (n - 1).factorial_ne_zero (factorial_mul_ascFactorial' _ _ h)

Premises used: Nat.eq_div_of_mul_eq_right, HSub.hSub, Nat.factorial_ne_zero, Nat.factorial_mul_ascFactorial', OfNat.ofNat
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : (n - k + k) * (n - k).ascFactorial k = (n - k).ascFactorial (k + 1)
rw₁ rw₂ : (n - k + k) * (n - k).ascFactorial k = (n - k + k) * (n - k).ascFactorial k
⊢ (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)

Tactic:
rw [succ_ascFactorial, ascFactorial_succ]

Premises used: Nat.ascFactorial_succ, Nat.succ_ascFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : HPow.hPow (β := ℕ) n 0 ≤ 1
rw₁ rw₂ : LE.le (α := ℕ) 1 1
⊢ HPow.hPow (β := ℕ) n 0 ≤ n.ascFactorial 0

Tactic:
rw [ascFactorial_zero, Nat.pow_zero]

Premises used: Nat.ascFactorial_zero, Nat.pow_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : n * n ^ k ≤ n * n.succ.ascFactorial k
⊢ n ^ (k + 1) ≤ n.ascFactorial (k + 1)

Tactic:
rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, ← succ_ascFactorial]

Premises used: Nat.ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, Nat.succ_ascFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ n * n ^ k ≤ n * n.succ.ascFactorial k

Tactic:
Nat.mul_le_mul (Nat.le_refl n)
      (Nat.le_trans (Nat.pow_le_pow_left (le_succ n) k) (pow_succ_le_ascFactorial n.succ k))

Premises used: Nat.le_refl, Nat.le_succ, Nat.mul_le_mul, Nat.le_trans, Nat.succ, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ n * n ^ k ≤ n * n.succ.ascFactorial k

Tactic:
exact Nat.mul_le_mul (Nat.le_refl n)
      (Nat.le_trans (Nat.pow_le_pow_left (le_succ n) k) (pow_succ_le_ascFactorial n.succ k))

Premises used: Nat.le_refl, Nat.le_succ, Nat.mul_le_mul, Nat.le_trans, Nat.succ, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : (n + 1) * (n + 1) ^ (k + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)
⊢ (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)

Tactic:
rw [Nat.pow_succ, ascFactorial, Nat.mul_comm]

Premises used: Nat.ascFactorial, Nat.pow_succ, Nat.mul_comm
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)

Tactic:
Nat.mul_lt_mul_of_lt_of_le' (Nat.lt_add_of_pos_right k.succ_pos)
    (pow_succ_le_ascFactorial n.succ _) (Nat.pow_pos n.succ_pos)

Premises used: Nat.mul_lt_mul_of_lt_of_le', Nat.lt_add_of_pos_right, Nat.pow_succ_le_ascFactorial, Nat.succ_pos, Nat.pow_pos, Nat.succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)

Tactic:
exact Nat.mul_lt_mul_of_lt_of_le' (Nat.lt_add_of_pos_right k.succ_pos)
    (pow_succ_le_ascFactorial n.succ _) (Nat.pow_pos n.succ_pos)

Premises used: Nat.mul_lt_mul_of_lt_of_le', Nat.lt_add_of_pos_right, Nat.pow_succ_le_ascFactorial, Nat.succ_pos, Nat.pow_pos, Nat.succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
h : LE.le (α := ℕ) 2 1
⊢ HPow.hPow (β := ℕ) (n + 1) 1 < (n + 1).ascFactorial 1

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : 1 ≤ HPow.hPow (β := ℕ) (n + 0) 0
rw₁ rw₂ : LE.le (α := ℕ) 1 1
⊢ (n + 1).ascFactorial 0 ≤ HPow.hPow (β := ℕ) (n + 0) 0

Tactic:
rw [ascFactorial_zero, Nat.pow_zero]

Premises used: Nat.ascFactorial_zero, Nat.pow_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : (n + 1).ascFactorial k * (n + k + 1) ≤ (n + k + 1) ^ k * (n + k + 1)
⊢ (n + 1).ascFactorial (k + 1) ≤ (n + (k + 1)) ^ (k + 1)

Tactic:
rw [ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, ← Nat.add_assoc, Nat.add_right_comm n 1 k]

Premises used: Nat.ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, Nat.add_assoc, OfNat.ofNat, Nat.add_right_comm
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k + 1) ≤ (n + k + 1) ^ k * (n + k + 1)

Tactic:
Nat.mul_le_mul_right _
      (Nat.le_trans (ascFactorial_le_pow_add _ k) (Nat.pow_le_pow_left (le_succ _) _))

Premises used: Nat.mul_le_mul_right, Nat.le_succ, Nat.le_trans, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k + 1) ≤ (n + k + 1) ^ k * (n + k + 1)

Tactic:
exact Nat.mul_le_mul_right _
      (Nat.le_trans (ascFactorial_le_pow_add _ k) (Nat.pow_le_pow_left (le_succ _) _))

Premises used: Nat.mul_le_mul_right, Nat.le_succ, Nat.le_trans, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
h : LE.le (α := ℕ) 2 1
⊢ (n + 1).ascFactorial 1 < HPow.hPow (β := ℕ) (n + 1) 1

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : 2 ≤ k + 2
rw : (n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)
⊢ (n + 1).ascFactorial (k + 2) < (n + (k + 2)) ^ (k + 2)

Tactic:
rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]

Premises used: Nat.ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, HAdd.hAdd, OfNat.ofNat, Nat.succ_add_eq_add_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : 2 ≤ k + 2
⊢ (n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)

Tactic:
Nat.mul_lt_mul_of_le_of_lt (le_refl _) (Nat.lt_of_le_of_lt (ascFactorial_le_pow_add n _)
      (Nat.pow_lt_pow_left (Nat.lt_succ_self _) k.succ_ne_zero)) (succ_pos _)

Premises used: le_refl, Nat.lt_succ_self, Nat.lt_of_le_of_lt, Nat.mul_lt_mul_of_le_of_lt, Nat.succ_ne_zero, Nat.succ_pos, Nat.ascFactorial_le_pow_add, Nat.pow_lt_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : 2 ≤ k + 2
⊢ (n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)

Tactic:
exact Nat.mul_lt_mul_of_le_of_lt (le_refl _) (Nat.lt_of_le_of_lt (ascFactorial_le_pow_add n _)
      (Nat.pow_lt_pow_left (Nat.lt_succ_self _) k.succ_ne_zero)) (succ_pos _)

Premises used: le_refl, Nat.lt_succ_self, Nat.lt_of_le_of_lt, Nat.mul_lt_mul_of_le_of_lt, Nat.succ_ne_zero, Nat.succ_pos, Nat.ascFactorial_le_pow_add, Nat.pow_lt_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ 0 < (n + 1).ascFactorial k

Tactic:
Nat.lt_of_lt_of_le (Nat.pow_pos n.succ_pos) (pow_succ_le_ascFactorial (n + 1) k)

Premises used: HAdd.hAdd, Nat.pow_succ_le_ascFactorial, Nat.succ_pos, Nat.pow_pos, OfNat.ofNat, Nat.lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ n.descFactorial 0 = 1

Tactic:
rfl

Premises used: rfl, Nat.descFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ n.descFactorial (k + 1) = (n - k) * n.descFactorial k

Tactic:
rfl

Premises used: rfl, Nat.descFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k : ℕ
rw : (0 - k) * descFactorial 0 k = 0
rw₁ : 0 * descFactorial 0 k = 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ descFactorial 0 (k + 1) = 0

Tactic:
rw [descFactorial_succ, Nat.zero_sub, Nat.zero_mul]

Premises used: Nat.zero_sub, Nat.descFactorial_succ, Nat.zero_mul
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ n.descFactorial 1 = n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : (n + 1).descFactorial (HAdd.hAdd (α := ℕ) 0 1) = (n + 1) * 1
rw₁ : n + 1 = (n + 1) * 1
rw₂ rw₃ : n + 1 = n + 1
⊢ (n + 1).descFactorial (HAdd.hAdd (α := ℕ) 0 1) = (n + 1) * n.descFactorial 0

Tactic:
rw [descFactorial_zero, descFactorial_one, Nat.mul_one]

Premises used: Nat.descFactorial_one, Nat.mul_one, Nat.descFactorial_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k.succ
rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial k.succ
rw₂ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
rw₃ : (n - k) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
rw₄ rw₅ : (n + 1) * ((n - k) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ

Tactic:
rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]

Premises used: Nat.mul_left_comm, Nat.descFactorial_succ, Nat.succ_sub_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : (n + 1) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0
rw₁ : (n + 1) * 1 = (n + 1) * n.descFactorial 0
rw₂ rw₃ : (n + 1) * 1 = (n + 1) * 1
⊢ (n + 1 - 0) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0

Tactic:
rw [Nat.sub_zero, descFactorial_zero, descFactorial_zero]

Premises used: Nat.descFactorial_zero, Nat.sub_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * ((n + 1 - k) * (n + 1).descFactorial k) = (n + 1) * n.descFactorial (k + 1)
rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial (k + 1)
rw₂ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
rw₃ : (n - k) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
rw₄ rw₅ : (n + 1) * ((n - k) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)

Tactic:
rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]

Premises used: Nat.mul_left_comm, Nat.descFactorial_succ, Nat.succ_sub_succ, Nat.descFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
rw : 1 = 0!
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ descFactorial 0 0 = 0!

Tactic:
rw [descFactorial_zero, factorial_zero]

Premises used: Nat.descFactorial_zero, Nat.factorial_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : (n + 1) * n.descFactorial n = n.succ !
rw₁ : (n + 1) * n ! = n.succ !
rw₂ rw₃ : (n + 1) * n ! = (n + 1) * n !
⊢ n.succ.descFactorial n.succ = n.succ !

Tactic:
rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]

Premises used: Nat.factorial_succ, Nat.succ_descFactorial_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ n.descFactorial 0 = 0 ↔ n < 0

Tactic:
simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]

Premises used: Nat.one_ne_zero, Nat.not_lt_zero, Nat.descFactorial_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : n ≤ k → n ≠ k → n ≤ k
⊢ n.descFactorial k.succ = 0 ↔ n < k.succ

Tactic:
rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
      Nat.sub_eq_zero_iff_le, Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]

Premises used: Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp, Nat.sub_eq_zero_iff_le, Nat.descFactorial_succ, Nat.lt_succ_iff, Nat.mul_eq_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k

Tactic:
fun h _ => h
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k

Tactic:
exact fun h _ => h
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ 0 < n.descFactorial k ↔ k ≤ n

Tactic:
simp [Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : (n + 0).descFactorial 0 = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ (n + 0).descFactorial 0 = (n + 1).ascFactorial 0

Tactic:
rw [ascFactorial_zero, descFactorial_zero]

Premises used: Nat.ascFactorial_zero, Nat.descFactorial_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : (n + k).succ.descFactorial k.succ = (n + 1).ascFactorial k.succ
rw₁ : (n + k + 1) * (n + k).descFactorial k = (n + 1).ascFactorial k.succ
rw₂ : (n + k + 1) * (n + k).descFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
rw₃ : (n + k + 1) * (n + 1).ascFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
rw₄ rw₅ : (n + 1 + k) * (n + 1).ascFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
⊢ (n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ

Tactic:
rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]

Premises used: Nat.ascFactorial_succ, Nat.add_succ, Nat.add_right_comm, Nat.succ_descFactorial_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : (n + 0 - 1).descFactorial 0 = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ (n + 0 - 1).descFactorial 0 = n.ascFactorial 0

Tactic:
rw [ascFactorial_zero, descFactorial_zero]

Premises used: Nat.ascFactorial_zero, Nat.descFactorial_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ
rw₁ : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = (n + k) * n.ascFactorial k
rw₂ : (n.succ + k - 1 - k) * (n.succ + k - 1).descFactorial k = (n + k) * n.ascFactorial k
rw₃ : (n.succ + k - 1 - k) * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
rw₄ : (n.succ + k - 1 - k) * n.succ.ascFactorial k = n * n.succ.ascFactorial k
rw₅ : (n + k - k) * n.succ.ascFactorial k = n * n.succ.ascFactorial k
rw₆ rw₇ : n * n.succ.ascFactorial k = n * n.succ.ascFactorial k
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ

Tactic:
rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]

Premises used: Nat.succ_add_sub_one, Nat.ascFactorial_succ, Nat.descFactorial_succ, Nat.add_sub_cancel, Nat.succ_add_eq_add_succ, Nat.succ_ascFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
h : 0 ≤ n
rw : (n - 0)! * 1 = n !
rw₁ : (n - 0)! = n !
rw₂ rw₃ : n ! = n !
⊢ (n - 0)! * n.descFactorial 0 = n !

Tactic:
rw [descFactorial_zero, Nat.mul_one, Nat.sub_zero]

Premises used: Nat.mul_one, Nat.descFactorial_zero, Nat.sub_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k : ℕ
h : k.succ ≤ 0
exfalso : False
⊢ (0 - k.succ)! * descFactorial 0 k.succ = 0!

Tactic:
exfalso
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k : ℕ
h : k.succ ≤ 0
⊢ False

Tactic:
not_succ_le_zero k h

Premises used: Nat.not_succ_le_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k : ℕ
h : k.succ ≤ 0
⊢ False

Tactic:
exact not_succ_le_zero k h

Premises used: Nat.not_succ_le_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k.succ ≤ n.succ
rw : (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₁ : (n - k)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₂ : (n - k)! * (n + 1) * n.descFactorial k = n.succ !
rw₃ : (n + 1) * (n - k)! * n.descFactorial k = n.succ !
rw₄ : (n + 1) * ((n - k)! * n.descFactorial k) = n.succ !
rw₅ : (n + 1) * n ! = n.succ !
rw₆ rw₇ : (n + 1) * n ! = (n + 1) * n !
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !

Tactic:
rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]

Premises used: Nat.factorial_succ, HSub.hSub, Nat.mul_comm, Nat.mul_assoc, Nat.factorial, Nat.succ_le_succ_iff, Iff.mp, Nat.succ_sub_succ, Nat.succ_descFactorial_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
pos : ∀ (hmn : m ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
neg : ∀ (hmn : ¬m ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
by_cases hmn : m ≤ n
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
pos : (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
apply Nat.mul_left_cancel (n - m).factorial_pos

Premises used: HSub.hSub, Nat.mul_left_cancel, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ n - m = n - k - (m - k)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ m - k ≤ n - k

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
pos : (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
pos₁ : (n - k - (m - k))! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
pos₂ : (n - k - (m - k))! * (n - k).descFactorial (m - k) * n.descFactorial k = n !
pos₃ : (n - k)! * n.descFactorial k = n !
pos₄ pos₅ : n ! = n !
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m

Tactic:
rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]

Premises used: Nat.mul_assoc, Nat.factorial_mul_descFactorial, le_trans
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ n < m

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
neg : (n - k).descFactorial (m - k) * n.descFactorial k = 0
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
rw [descFactorial_eq_zero_iff_lt.mpr (show n < m by lia)]

Premises used: Iff.mpr, Nat.descFactorial_eq_zero_iff_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
pos : ∀ (hkn : k ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = 0
neg : ∀ (hkn : ¬k ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = 0
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Tactic:
by_cases hkn : k ≤ n
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ n - k < m - k

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
pos : 0 * n.descFactorial k = 0
pos₁ pos₂ : Eq (α := ℕ) 0 0
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Tactic:
rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by lia), Nat.zero_mul]

Premises used: Iff.mpr, Nat.zero_mul, Nat.descFactorial_eq_zero_iff_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
⊢ n < k

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
neg : (n - k).descFactorial (m - k) * 0 = 0
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Tactic:
rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by lia), Nat.mul_zero]

Premises used: Iff.mpr, Nat.mul_zero, Nat.descFactorial_eq_zero_iff_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k ≤ n
apply : (n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)
⊢ n.descFactorial k = n ! / (n - k)!

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

Premises used: HSub.hSub, Nat.mul_left_cancel, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k ≤ n
rw : n ! = (n - k)! * (n ! / (n - k)!)
⊢ (n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)

Tactic:
rw [factorial_mul_descFactorial h]

Premises used: Nat.factorial_mul_descFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)

Tactic:
(Nat.mul_div_cancel' <| factorial_dvd_factorial <| Nat.sub_le n k).symm

Premises used: Nat.sub_le, Nat.factorial_dvd_factorial, Eq.symm, Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)

Tactic:
exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| Nat.sub_le n k).symm

Premises used: Nat.sub_le, Nat.factorial_dvd_factorial, Eq.symm, Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m : ℕ
h : k ≤ m
⊢ k.descFactorial 0 ≤ k.descFactorial 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ (k - n) * k.descFactorial n ≤ (m - n) * m.descFactorial n

Tactic:
Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih

Premises used: Nat.sub_le_sub_right, Nat.mul_le_mul
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ (k - n) * k.descFactorial n ≤ (m - n) * m.descFactorial n

Tactic:
exact Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih

Premises used: Nat.sub_le_sub_right, Nat.mul_le_mul
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k m : ℕ
h : k ≤ m
zero : k.descFactorial 0 ≤ k.descFactorial 0
succ : ∀ (n : ℕ) (ih : k.descFactorial n ≤ m.descFactorial n), k.descFactorial (n + 1) ≤ m.descFactorial (n + 1)
⊢ k.descFactorial n ≤ m.descFactorial n

Tactic:
induction n with
  | zero => rfl
  | succ n ih =>
    rw [descFactorial_succ, descFactorial_succ]
    exact Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih

Premises used: Nat.descFactorial_succ, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : HPow.hPow (β := ℕ) (n + 1 - 0) 0 ≤ 1
rw₁ rw₂ : LE.le (α := ℕ) 1 1
⊢ HPow.hPow (β := ℕ) (n + 1 - 0) 0 ≤ n.descFactorial 0

Tactic:
rw [descFactorial_zero, Nat.pow_zero]

Premises used: Nat.pow_zero, Nat.descFactorial_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : (n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ n.descFactorial (k + 1)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, Nat.mul_comm]

Premises used: Nat.pow_succ, Nat.mul_comm, Nat.descFactorial_succ, Nat.succ_sub_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : (n - k) ^ k ≤ n.descFactorial k
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k

Tactic:
apply Nat.mul_le_mul_left

Premises used: Nat.mul_le_mul_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ (n - k) ^ k ≤ n.descFactorial k

Tactic:
(le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k)
      (pow_sub_le_descFactorial n k))

Premises used: Nat.le_succ, Nat.sub_le_sub_right, Nat.pow_le_pow_left, le_trans
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ (n - k) ^ k ≤ n.descFactorial k

Tactic:
exact (le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k)
      (pow_sub_le_descFactorial n k))

Premises used: Nat.le_succ, Nat.sub_le_sub_right, Nat.pow_le_pow_left, le_trans