awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
h : HAdd.hAdd (α := ℕ) 0 2 ≤ n
rw : (n - HAdd.hAdd (α := ℕ) 0 1) * (n - HAdd.hAdd (α := ℕ) 0 1) < (n - 1) * n
⊢ (n - HAdd.hAdd (α := ℕ) 0 1) ^ HAdd.hAdd (α := ℕ) 0 2 < n.descFactorial (HAdd.hAdd (α := ℕ) 0 2)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, Nat.pow_one, descFactorial_one]

Premises used: Nat.descFactorial_one, Nat.pow_succ, Nat.descFactorial_succ, Nat.pow_one
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
h : HAdd.hAdd (α := ℕ) 0 2 ≤ n
⊢ n - HAdd.hAdd (α := ℕ) 0 1 < n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
h : HAdd.hAdd (α := ℕ) 0 2 ≤ n
⊢ (n - HAdd.hAdd (α := ℕ) 0 1) * (n - HAdd.hAdd (α := ℕ) 0 1) < (n - 1) * n

Tactic:
exact Nat.mul_lt_mul_of_pos_left (by lia) (Nat.sub_pos_of_lt h)

Premises used: Nat.sub_pos_of_lt, Nat.mul_lt_mul_of_pos_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
rw : (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < n.descFactorial (k + 1 + 2)

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

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

Tactic:
Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)

Premises used: Nat.sub_pos_of_lt, Nat.mul_lt_mul_of_pos_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
refine : (n - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)

Tactic:
refine Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)

Premises used: Nat.sub_pos_of_lt, Nat.mul_lt_mul_of_pos_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_

Premises used: Nat.lt_of_le_of_lt, Nat.le_succ, Nat.sub_le_sub_right, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
refine : (n.succ - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)
⊢ (n - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
refine Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_

Premises used: Nat.lt_of_le_of_lt, Nat.le_succ, Nat.sub_le_sub_right, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
rw : (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
⊢ (n.succ - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
rw [succ_sub_succ]

Premises used: Nat.succ_sub_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
pow_sub_lt_descFactorial' (Nat.le_trans (le_succ _) h)

Premises used: Nat.le_succ, Nat.le_trans
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
exact pow_sub_lt_descFactorial' (Nat.le_trans (le_succ _) h)

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

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

Tactic:
rw [succ_sub_succ]

Premises used: Nat.succ_sub_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h_1 : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
pow_sub_lt_descFactorial' h

Premises used: Nat.pow_sub_lt_descFactorial'
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h_1 : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
exact pow_sub_lt_descFactorial' h

Premises used: Nat.pow_sub_lt_descFactorial'
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : 1 ≤ HPow.hPow (β := ℕ) n 0
rw₁ rw₂ : LE.le (α := ℕ) 1 1
⊢ n.descFactorial 0 ≤ HPow.hPow (β := ℕ) n 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.descFactorial k ≤ n * n ^ k
⊢ n.descFactorial (k + 1) ≤ n ^ (k + 1)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm _ n]

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

Tactic:
Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)

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

Tactic:
exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)

Premises used: Nat.sub_le, Nat.mul_le_mul
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hn : n ≠ 0
h : LE.le (α := ℕ) 2 1
⊢ n.descFactorial 1 < HPow.hPow (β := ℕ) n 1

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

Tactic:
rw [descFactorial_succ, pow_succ', Nat.mul_comm, Nat.mul_comm n]

Premises used: Nat.pow_succ', Nat.mul_comm, Nat.descFactorial_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : 2 ≤ k + 2
⊢ n - (k + 1) < n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : 2 ≤ k + 2
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : 2 ≤ k + 2
⊢ n.descFactorial (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n

Tactic:
exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (by lia) (Nat.pow_pos <| by lia)

Premises used: Nat.mul_lt_mul_of_le_of_lt, Nat.descFactorial_le_pow, Nat.pow_pos
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : (n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !
⊢ (2 * n)! ≤ (2 * n) ^ n * n !

Tactic:
rw [Nat.two_mul, ← factorial_mul_ascFactorial, Nat.mul_comm]

Premises used: Nat.factorial_mul_ascFactorial, Nat.mul_comm, Nat.two_mul
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ (n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !

Tactic:
Nat.mul_le_mul_right _ (ascFactorial_le_pow_add _ _)

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

Tactic:
exact Nat.mul_le_mul_right _ (ascFactorial_le_pow_add _ _)

Premises used: Nat.mul_le_mul_right, Nat.ascFactorial_le_pow_add
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
zero : HPow.hPow (α := ℕ) (β := ℕ) 2 0 * 0! ≤ (HMul.hMul (α := ℕ) 2 0)!
succ : ∀ (n : ℕ), HPow.hPow (α := ℕ) 2 (n + 1) * (n + 1)! ≤ (2 * (n + 1))!
⊢ HPow.hPow (α := ℕ) 2 n * n ! ≤ (2 * n)!

Tactic:
obtain _ | n := n
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 0 * 0! ≤ (HMul.hMul (α := ℕ) 2 0)!

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
succ : (n + 1)! * HPow.hPow (α := ℕ) 2 (n + 1) ≤ (n + 1 + (n + 1))!
⊢ HPow.hPow (α := ℕ) 2 (n + 1) * (n + 1)! ≤ (2 * (n + 1))!

Tactic:
rw [Nat.mul_comm, Nat.two_mul]

Premises used: Nat.mul_comm, Nat.two_mul
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ (n + 1)! * HPow.hPow (α := ℕ) 2 (n + 1) ≤ (n + 1)! * (n + 2) ^ (n + 1)

Tactic:
Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (le_add_left _ _) _)

Premises used: Nat.le_add_left, Nat.mul_le_mul_left, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ (n + 1)! * (n + 2) ^ (n + 1) ≤ (n + 1 + (n + 1))!

Tactic:
Nat.factorial_mul_pow_le_factorial

Premises used: Nat.factorial_mul_pow_le_factorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ (n + 1)! * HPow.hPow (α := ℕ) 2 (n + 1) ≤ (n + 1 + (n + 1))!

Tactic:
calc
    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) :=
      Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (le_add_left _ _) _)
    _ ≤ _ := Nat.factorial_mul_pow_le_factorial

Premises used: Nat.le_add_left, Nat.mul_le_mul_left, Nat.factorial_mul_pow_le_factorial, HAdd.hAdd, OfNat.ofNat, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
h : ∀ (n k : ℕ), n.ascFactorial k = n.ascFactorialBinary k
⊢ ascFactorial = ascFactorialBinary

Tactic:
ext n k
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ n.ascFactorial 0 = 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ n.ascFactorial 1 = n

Tactic:
simp [ascFactorial]

Premises used: Nat.ascFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
ih₁ : n.ascFactorial ((k + 2) / 2) = n.ascFactorialBinary ((k + 2) / 2)
ih₂ : (n + (k + 2) / 2).ascFactorial ((k + 2 + 1) / 2) = (n + (k + 2) / 2).ascFactorialBinary ((k + 2 + 1) / 2)
⊢ n.ascFactorial k.succ.succ =
    n.ascFactorialBinary ((k + 2) / 2) * (n + (k + 2) / 2).ascFactorialBinary ((k + 2 + 1) / 2)

Tactic:
grind [ascFactorial_mul_ascFactorial]

Premises used: Nat.ascFactorial_mul_ascFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : ∀ (n : ℕ), n.ascFactorial 0 = 1
h₁ : ∀ (n : ℕ), n.ascFactorial 1 = n
h₂ :
  ∀ (n k : ℕ) (ih₁ : n.ascFactorial ((k + 2) / 2) = n.ascFactorialBinary ((k + 2) / 2))
    (ih₂ : (n + (k + 2) / 2).ascFactorial ((k + 2 + 1) / 2) = (n + (k + 2) / 2).ascFactorialBinary ((k + 2 + 1) / 2)),
    n.ascFactorial k.succ.succ =
      n.ascFactorialBinary ((k + 2) / 2) * (n + (k + 2) / 2).ascFactorialBinary ((k + 2 + 1) / 2)
⊢ n.ascFactorial k = n.ascFactorialBinary k

Tactic:
fun_induction ascFactorialBinary with
  | case1 => simp
  | case2 => simp [ascFactorial]
  | case3 n k ih₁ ih₂ => grind [ascFactorial_mul_ascFactorial]

Premises used: Nat.ascFactorial, Nat.ascFactorialBinary, Nat.ascFactorial_mul_ascFactorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
h : ∀ (n : ℕ), n ! = n.factorialBinarySplitting
⊢ factorial = factorialBinarySplitting

Tactic:
ext n
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ n ! = n.factorialBinarySplitting

Tactic:
simp [factorialBinarySplitting, ← ascFactorial_eq_ascFactorialBinary]

Premises used: Nat.ascFactorial_eq_ascFactorialBinary, Nat.factorialBinarySplitting
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
h : ∀ (n k : ℕ), n.descFactorial k = n.descFactorialBinary k
⊢ descFactorial = descFactorialBinary

Tactic:
ext n k
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
pos : ∀ (h : n < k), n.descFactorial k = 0
neg : ∀ (h : ¬n < k), n.descFactorial k = (n - k + 1).ascFactorialBinary k
⊢ n.descFactorial k = if n < k then 0 else (n - k + 1).ascFactorialBinary k

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : n < k
pos pos₁ : Eq (α := ℕ) 0 0
⊢ n.descFactorial k = 0

Tactic:
rw [descFactorial_of_lt h]

Premises used: Nat.descFactorial_of_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : ¬n < k
neg : n.descFactorial k = (n - k + 1 + k - 1).descFactorial k
⊢ n.descFactorial k = (n - k + 1).ascFactorialBinary k

Tactic:
rw [← ascFactorial_eq_ascFactorialBinary, ← add_descFactorial_eq_ascFactorial']

Premises used: Nat.ascFactorial_eq_ascFactorialBinary, Nat.add_descFactorial_eq_ascFactorial'
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1 + k - 1).descFactorial k

Tactic:
grind
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
⊢ Monotone factorial

Tactic:
fun _ _ => factorial_le

Premises used: Monotone, Nat.factorial_le
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ LT.lt (α := ℕ) 0 (∏ i ∈ s, (f i)!)

Tactic:
prod_pos fun _ _ ↦ factorial_pos _

Premises used: Finset.prod_pos, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i ∈ ∅, (f i)! ∣ (∑ i ∈ ∅, f i)!

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
α : Type u_1
s_1 : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
cons : (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!
⊢ ∏ i ∈ Finset.cons a s has, (f i)! ∣ (∑ i ∈ Finset.cons a s has, f i)!

Tactic:
rw [prod_cons, Finset.sum_cons]

Premises used: Finset.sum_cons, Finset.prod_cons
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
α : Type u_1
s_1 : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!

Tactic:
(mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)

Premises used: Nat.factorial_mul_factorial_dvd_factorial_add, mul_dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
α : Type u_1
s_1 : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!

Tactic:
exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)

Premises used: Nat.factorial_mul_factorial_dvd_factorial_add, mul_dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
empty : ∏ i ∈ ∅, (f i)! ∣ (∑ i ∈ ∅, f i)!
cons :
  ∀ (a : α) (s : Finset α) (has : a ∉ s) (ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!),
    ∏ i ∈ Finset.cons a s has, (f i)! ∣ (∑ i ∈ Finset.cons a s has, f i)!
⊢ ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s has ih =>
    rw [prod_cons, Finset.sum_cons]
    exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)

Premises used: Finset.sum_cons, Finset.cons, Finset.prod_cons
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
n : ℕ
rw : n.succ * n ! = ∏ i ∈ range (n + 1), (i + 1)
rw₁ : n.succ * n ! = (n + 1) * ∏ x ∈ range n, (x + 1)
rw₂ rw₃ : n.succ * ∏ i ∈ range n, (i + 1) = (n + 1) * ∏ x ∈ range n, (x + 1)
⊢ (n + 1)! = ∏ i ∈ range (n + 1), (i + 1)

Tactic:
rw [factorial, prod_range_succ_comm, factorial_eq_prod_range_add_one n]

Premises used: Finset.prod_range_succ_comm, Nat.factorial
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
n : ℕ
⊢ ∏ i ∈ range n, (i + 1) = n !

Tactic:
factorial_eq_prod_range_add_one _ |>.symm

Premises used: Eq.symm, Nat.factorial_eq_prod_range_add_one
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
n k : ℕ
rw : (n + k) * n.ascFactorial k = ∏ i ∈ range (k + 1), (n + i)
rw₁ : (n + k) * n.ascFactorial k = (n + k) * ∏ x ∈ range k, (n + x)
rw₂ rw₃ : (n + k) * ∏ i ∈ range k, (n + i) = (n + k) * ∏ x ∈ range k, (n + x)
⊢ n.ascFactorial (k + 1) = ∏ i ∈ range (k + 1), (n + i)

Tactic:
rw [ascFactorial, prod_range_succ_comm, ascFactorial_eq_prod_range n k]

Premises used: Nat.ascFactorial, Finset.prod_range_succ_comm
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
n k : ℕ
rw : (n - k) * n.descFactorial k = ∏ i ∈ range (k + 1), (n - i)
rw₁ : (n - k) * n.descFactorial k = (n - k) * ∏ x ∈ range k, (n - x)
rw₂ rw₃ : (n - k) * ∏ i ∈ range k, (n - i) = (n - k) * ∏ x ∈ range k, (n - x)
⊢ n.descFactorial (k + 1) = ∏ i ∈ range (k + 1), (n - i)

Tactic:
rw [descFactorial, prod_range_succ_comm, descFactorial_eq_prod_range n k]

Premises used: Finset.prod_range_succ_comm, Nat.descFactorial
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
k : ℕ
n : ℤ
rw : HMod.hMod (α := ℤ) (∏ i ∈ range k, (n + (↑i : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
⊢ Dvd.dvd (α := ℤ) (↑k ! : ℤ) (∏ i ∈ range k, (n + (↑i : ℤ)))

Tactic:
rw [Int.dvd_iff_emod_eq_zero, Finset.prod_int_mod]

Premises used: Finset.prod_int_mod, Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
k : ℕ
n : ℤ
simp_rw : HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
⊢ HMod.hMod (α := ℤ) (∏ i ∈ range k, (n + (↑i : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0

Tactic:
simp_rw [← Int.emod_add_emod n]

Premises used: Int.emod_add_emod
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
k : ℕ
n : ℤ
⊢ 0 ≤ n % (↑k ! : ℤ)

Tactic:
have hn : 0 ≤ n % k ! := Int.emod_nonneg n <| Int.natCast_ne_zero.mpr k.factorial_ne_zero
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
k : ℕ
n : ℤ
hn : 0 ≤ n % (↑k ! : ℤ)
obtain :
  ∀ (x : ℕ) (hx : n % (↑k ! : ℤ) = (↑x : ℤ)),
    HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
⊢ HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0

Tactic:
obtain ⟨x, hx⟩ := Int.eq_ofNat_of_zero_le hn

Premises used: Int.eq_ofNat_of_zero_le
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
k : ℕ
n : ℤ
hn : 0 ≤ n % (↑k ! : ℤ)
x : ℕ
hx : n % (↑k ! : ℤ) = (↑x : ℤ)
⊢ k ! ∣ x.ascFactorial k

Tactic:
have hdivk := x.factorial_dvd_ascFactorial k
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
k : ℕ
n : ℤ
hn : 0 ≤ n % (↑k ! : ℤ)
x : ℕ
hx : n % (↑k ! : ℤ) = (↑x : ℤ)
hdivk : k ! ∣ x.ascFactorial k
⊢ Dvd.dvd (α := ℤ) (↑k ! : ℤ) (∏ x_1 ∈ range k, HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑x_1 : ℤ))

Tactic:
zify [x.ascFactorial_eq_prod_range k] at hdivk

Premises used: Nat.ascFactorial_eq_prod_range
-- Module: Mathlib.Data.Nat.Factorial.BigOperators
Goal:
k : ℕ
n : ℤ
hn : 0 ≤ n % (↑k ! : ℤ)
x : ℕ
hx : n % (↑k ! : ℤ) = (↑x : ℤ)
hdivk : Dvd.dvd (α := ℤ) (↑k ! : ℤ) (∏ x_1 ∈ range k, HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑x_1 : ℤ))
rwa : HMod.hMod (α := ℤ) (∏ i ∈ range k, (n % (↑k ! : ℤ) + (↑i : ℤ))) (↑k ! : ℤ) = 0
rwa₁ : Dvd.dvd (α := ℤ) (↑k ! : ℤ) (∏ i ∈ range k, (n % (↑k ! : ℤ) + (↑i : ℤ)))
rwa₂ rwa₃ rwa₄ rwa₅ : Dvd.dvd (α := ℤ) (↑k ! : ℤ) (∏ i ∈ range k, HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑i : ℤ))
⊢ HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0

Tactic:
rwa [← Finset.prod_int_mod, ← Int.dvd_iff_emod_eq_zero, hx]

Premises used: Finset.prod_int_mod, Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.Data.Nat.Factorial.Cast
Goal:
S : Type u_1
inst : Ring S
a : ℕ
zero : (↑(HSub.hSub (α := ℕ) 0 1 * descFactorial 0 1) : S) = (↑0 : S) * HSub.hSub (α := S) (↑0 : S) 1
succ : ∀ (n : ℕ), (↑((n + 1 - 1) * (n + 1).descFactorial 1) : S) = (↑(n + 1) : S) * HSub.hSub (α := S) (↑(n + 1) : S) 1
⊢ (↑((a - 1) * a.descFactorial 1) : S) = (↑a : S) * HSub.hSub (α := S) (↑a : S) 1

Tactic:
cases a
-- Module: Mathlib.Data.Nat.Factorial.Cast
Goal:
S : Type u_1
inst : Ring S
⊢ (↑(HSub.hSub (α := ℕ) 0 1 * descFactorial 0 1) : S) = (↑0 : S) * HSub.hSub (α := S) (↑0 : S) 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorial.Cast
Goal:
S : Type u_1
inst : Ring S
n : ℕ
⊢ (↑((n + 1 - 1) * (n + 1).descFactorial 1) : S) = (↑(n + 1) : S) * HSub.hSub (α := S) (↑(n + 1) : S) 1

Tactic:
simp [mul_add, add_mul]

Premises used: add_mul, mul_add
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ (n + 2)‼ = (n + 2) * n‼

Tactic:
rfl

Premises used: Nat.doubleFactorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1)‼ = HAdd.hAdd (α := ℕ) 0 1 * (HSub.hSub (α := ℕ) 0 1)‼
succ : ∀ (n : ℕ), (n + 1 + 1)‼ = (n + 1 + 1) * (n + 1 - 1)‼
⊢ (n + 1)‼ = (n + 1) * (n - 1)‼

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
⊢ (HAdd.hAdd (α := ℕ) 0 1)‼ = HAdd.hAdd (α := ℕ) 0 1 * (HSub.hSub (α := ℕ) 0 1)‼

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ (n + 1 + 1)‼ = (n + 1 + 1) * (n + 1 - 1)‼

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
k : ℕ
rw : (k + 1 + 1)! = (k + 2) * k‼ * (k + 1)‼
rw₁ : (k + 1).succ * (k + 1)! = (k + 2) * k‼ * (k + 1)‼
rw₂ : (k + 1).succ * ((k + 1)‼ * k‼) = (k + 2) * k‼ * (k + 1)‼
rw₃ : (k + 1).succ * (k‼ * (k + 1)‼) = (k + 2) * k‼ * (k + 1)‼
rw₄ rw₅ : (k + 1).succ * (k‼ * (k + 1)‼) = (k + 2) * (k‼ * (k + 1)‼)
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼

Tactic:
rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
      mul_assoc]

Premises used: mul_assoc, Nat.doubleFactorial, Nat.factorial, mul_comm, Nat.doubleFactorial_add_two
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
rw : (n + 1)‼ ≤ (n + 1)‼ * n‼
⊢ (n + 1)‼ ≤ (n + 1)!

Tactic:
rw [factorial_eq_mul_doubleFactorial]

Premises used: Nat.factorial_eq_mul_doubleFactorial
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ (n + 1)‼ ≤ (n + 1)‼ * n‼

Tactic:
Nat.le_mul_of_pos_right _ n.doubleFactorial_pos

Premises used: Nat.le_mul_of_pos_right, Nat.doubleFactorial_pos
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ (n + 1)‼ ≤ (n + 1)‼ * n‼

Tactic:
exact Nat.le_mul_of_pos_right _ n.doubleFactorial_pos

Premises used: Nat.le_mul_of_pos_right, Nat.doubleFactorial_pos
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
rw : (2 * n + 2) * (HPow.hPow (α := ℕ) 2 n * n !) = HPow.hPow (α := ℕ) 2 n * 2 * ((n + 1) * n !)
⊢ (2 * (n + 1))‼ = HPow.hPow (α := ℕ) 2 (n + 1) * (n + 1)!

Tactic:
rw [mul_add, mul_one, doubleFactorial_add_two, factorial, pow_succ, doubleFactorial_two_mul _,
      succ_eq_add_one]

Premises used: Nat.succ_eq_add_one, pow_succ, Nat.factorial, Nat.doubleFactorial_add_two, mul_add, mul_one
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ (2 * n + 2) * (HPow.hPow (α := ℕ) 2 n * n !) = HPow.hPow (α := ℕ) 2 n * 2 * ((n + 1) * n !)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ 2 * (n + 1) = 2 * n + 2

Tactic:
ring
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
rw : (2 * n + 2)‼ = (2 * n + 2) * (2 * n)‼
⊢ (2 * (n + 1))‼ = ∏ i ∈ Finset.range (n + 1), 2 * (i + 1)

Tactic:
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_even _, mul_comm (2 * n)‼,
      (by ring : 2 * (n + 1) = 2 * n + 2)]

Premises used: HMul.hMul, Nat.doubleFactorial, mul_comm, Finset.prod_range_succ, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ (2 * n + 2)‼ = (2 * n + 2) * (2 * n)‼

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ 2 * (n + 1) + 1 = 2 * n + 1 + 2

Tactic:
ring
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
rw : (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼
⊢ (2 * (n + 1) + 1)‼ = ∏ i ∈ Finset.range (n + 1), (2 * (i + 1) + 1)

Tactic:
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_odd _, mul_comm (2 * n + 1)‼,
      (by ring : 2 * (n + 1) + 1 = 2 * n + 1 + 2)]

Premises used: HMul.hMul, Nat.doubleFactorial, HAdd.hAdd, mul_comm, Finset.prod_range_succ, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorial.DoubleFactorial
Goal:
n : ℕ
⊢ 0 < n‼

Tactic:
positivity
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑n ! : A)
m : ℕ
hmn : m ≤ n
obtain : ∀ (k : ℕ) (hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)) (hmn : m ≤ m + k), IsUnit.{u_1} (M := A) (↑m ! : A)
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)

Tactic:
obtain ⟨k, rfl⟩ := exists_add_of_le hmn

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
m : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(m + 0)! : A)
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)

Tactic:
simpa using hn_fac
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
k : ℕ
ih : ∀ {m : ℕ} (hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)
m : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(m + (k + 1))! : A)
⊢ IsUnit.{u_1} (M := A) (↑(m + 1 + k)! : A)

Tactic:
rw [← add_assoc, add_right_comm] at hn_fac

Premises used: add_assoc, add_right_comm
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
k : ℕ
ih : ∀ {m : ℕ} (hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)
m : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(m + 1 + k)! : A)
⊢ IsUnit.{u_1} (M := A) (↑(m + 1)! : A)

Tactic:
have := ih hn_fac