awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h_1 : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n + 1 - (k + 2)) ^ (k + 2) < n.descFactorial (k + 2)
have rw : (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
Tactic: rw [succ_sub_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ n.descFactorial 0 ≤ HPow.hPow (β := ℕ) n 0
have rw : 1 ≤ HPow.hPow (β := ℕ) n 0
Tactic: rw [descFactorial_zero, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : 1 ≤ HPow.hPow (β := ℕ) n 0
⊢ n.descFactorial 0 ≤ HPow.hPow (β := ℕ) n 0
have rw₁ : LE.le (α := ℕ) 1 1
Tactic: rw [descFactorial_zero, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ n.descFactorial (k + 1) ≤ n ^ (k + 1)
have rw : (n - k) * n.descFactorial k ≤ n * n ^ k
Tactic: rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm _ n]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : 2 ≤ k + 2
⊢ n.descFactorial (k + 2) < n ^ (k + 2)
have rw : n.descFactorial (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n
Tactic: rw [descFactorial_succ, pow_succ', Nat.mul_comm, Nat.mul_comm n]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ (2 * n)! ≤ (2 * n) ^ n * n !
have rw : (n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !
Tactic: rw [Nat.two_mul, ← factorial_mul_ascFactorial, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) 2 n * n ! ≤ (2 * n)!
have zero : HPow.hPow (α := ℕ) (β := ℕ) 2 0 * 0! ≤ (HMul.hMul (α := ℕ) 2 0)!
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
zero : HPow.hPow (α := ℕ) (β := ℕ) 2 0 * 0! ≤ (HMul.hMul (α := ℕ) 2 0)!
⊢ HPow.hPow (α := ℕ) 2 n * n ! ≤ (2 * n)!
have succ : ∀ (n : ℕ), HPow.hPow (α := ℕ) 2 (n + 1) * (n + 1)! ≤ (2 * (n + 1))!
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) 2 (n + 1) * (n + 1)! ≤ (2 * (n + 1))!
have succ : (n + 1)! * HPow.hPow (α := ℕ) 2 (n + 1) ≤ (n + 1 + (n + 1))!
Tactic: rw [Nat.mul_comm, Nat.two_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
⊢ ascFactorial = ascFactorialBinary
have h : ∀ (n k : ℕ), n.ascFactorial k = n.ascFactorialBinary k
Tactic: ext n k
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ n.ascFactorial k = n.ascFactorialBinary k
have h : ∀ (n : ℕ), n.ascFactorial 0 = 1
Tactic: fun_induction ascFactorialBinary with
  | case1 => simp
  | case2 => simp [ascFactorial]
  | case3 n k ih₁ ih₂ => grind [ascFactorial_mul_ascFactorial]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : ∀ (n : ℕ), n.ascFactorial 0 = 1
⊢ n.ascFactorial k = n.ascFactorialBinary k
have h₁ : ∀ (n : ℕ), n.ascFactorial 1 = n
Tactic: fun_induction ascFactorialBinary with
  | case1 => simp
  | case2 => simp [ascFactorial]
  | case3 n k ih₁ ih₂ => grind [ascFactorial_mul_ascFactorial]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : ∀ (n : ℕ), n.ascFactorial 0 = 1
h₁ : ∀ (n : ℕ), n.ascFactorial 1 = n
⊢ n.ascFactorial k = n.ascFactorialBinary k
have 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)
Tactic: fun_induction ascFactorialBinary with
  | case1 => simp
  | case2 => simp [ascFactorial]
  | case3 n k ih₁ ih₂ => grind [ascFactorial_mul_ascFactorial]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
⊢ factorial = factorialBinarySplitting
have h : ∀ (n : ℕ), n ! = n.factorialBinarySplitting
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
⊢ descFactorial = descFactorialBinary
have h : ∀ (n k : ℕ), n.descFactorial k = n.descFactorialBinary k
Tactic: ext n k
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ n.descFactorial k = if n < k then 0 else (n - k + 1).ascFactorialBinary k
have pos : ∀ (h : n < k), n.descFactorial k = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
pos : ∀ (h : n < k), n.descFactorial k = 0
⊢ n.descFactorial k = if n < k then 0 else (n - k + 1).ascFactorialBinary k
have neg : ∀ (h : ¬n < k), n.descFactorial k = (n - k + 1).ascFactorialBinary k
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : n < k
⊢ n.descFactorial k = 0
have pos : Eq (α := ℕ) 0 0
Tactic: rw [descFactorial_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1).ascFactorialBinary k
have neg : n.descFactorial k = (n - k + 1 + k - 1).descFactorial k
Tactic: rw [← ascFactorial_eq_ascFactorialBinary, ← add_descFactorial_eq_ascFactorial']
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
α : Type u_1
s_1 : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ ∏ i ∈ cons a s has, (f i)! ∣ (∑ i ∈ cons a s has, f i)!
have cons : (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!
Tactic: rw [prod_cons, Finset.sum_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
have empty : ∏ i ∈ ∅, (f i)! ∣ (∑ i ∈ ∅, 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 _ _)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
empty : ∏ i ∈ ∅, (f i)! ∣ (∑ i ∈ ∅, f i)!
⊢ ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
have cons : ∀ (a : α) (s : Finset α) (has : a ∉ s) (ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!),
  ∏ i ∈ cons a s has, (f i)! ∣ (∑ i ∈ cons a s has, 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 _ _)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
n : ℕ
⊢ (n + 1)! = ∏ i ∈ range (n + 1), (i + 1)
have rw : n.succ * n ! = ∏ i ∈ range (n + 1), (i + 1)
Tactic: rw [factorial, prod_range_succ_comm, factorial_eq_prod_range_add_one n]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
n : ℕ
rw : n.succ * n ! = ∏ i ∈ range (n + 1), (i + 1)
⊢ (n + 1)! = ∏ i ∈ range (n + 1), (i + 1)
have rw₁ : n.succ * n ! = (n + 1) * ∏ x ∈ range n, (x + 1)
Tactic: rw [factorial, prod_range_succ_comm, factorial_eq_prod_range_add_one n]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
n : ℕ
rw : n.succ * n ! = ∏ i ∈ range (n + 1), (i + 1)
rw₁ : n.succ * n ! = (n + 1) * ∏ x ∈ range n, (x + 1)
⊢ (n + 1)! = ∏ i ∈ range (n + 1), (i + 1)
have rw₂ : n.succ * ∏ i ∈ range n, (i + 1) = (n + 1) * ∏ x ∈ range n, (x + 1)
Tactic: rw [factorial, prod_range_succ_comm, factorial_eq_prod_range_add_one n]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
n k : ℕ
⊢ n.ascFactorial (k + 1) = ∏ i ∈ range (k + 1), (n + i)
have rw : (n + k) * n.ascFactorial k = ∏ i ∈ range (k + 1), (n + i)
Tactic: rw [ascFactorial, prod_range_succ_comm, ascFactorial_eq_prod_range n k]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
n k : ℕ
rw : (n + k) * n.ascFactorial k = ∏ i ∈ range (k + 1), (n + i)
⊢ n.ascFactorial (k + 1) = ∏ i ∈ range (k + 1), (n + i)
have rw₁ : (n + k) * n.ascFactorial k = (n + k) * ∏ x ∈ range k, (n + x)
Tactic: rw [ascFactorial, prod_range_succ_comm, ascFactorial_eq_prod_range n k]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
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)
⊢ n.ascFactorial (k + 1) = ∏ i ∈ range (k + 1), (n + i)
have rw₂ : (n + k) * ∏ i ∈ range k, (n + i) = (n + k) * ∏ x ∈ range k, (n + x)
Tactic: rw [ascFactorial, prod_range_succ_comm, ascFactorial_eq_prod_range n k]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
n k : ℕ
⊢ n.descFactorial (k + 1) = ∏ i ∈ range (k + 1), (n - i)
have rw : (n - k) * n.descFactorial k = ∏ i ∈ range (k + 1), (n - i)
Tactic: rw [descFactorial, prod_range_succ_comm, descFactorial_eq_prod_range n k]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
n k : ℕ
rw : (n - k) * n.descFactorial k = ∏ i ∈ range (k + 1), (n - i)
⊢ n.descFactorial (k + 1) = ∏ i ∈ range (k + 1), (n - i)
have rw₁ : (n - k) * n.descFactorial k = (n - k) * ∏ x ∈ range k, (n - x)
Tactic: rw [descFactorial, prod_range_succ_comm, descFactorial_eq_prod_range n k]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
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)
⊢ n.descFactorial (k + 1) = ∏ i ∈ range (k + 1), (n - i)
have rw₂ : (n - k) * ∏ i ∈ range k, (n - i) = (n - k) * ∏ x ∈ range k, (n - x)
Tactic: rw [descFactorial, prod_range_succ_comm, descFactorial_eq_prod_range n k]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
k : ℕ
n : ℤ
⊢ Dvd.dvd (α := ℤ) (↑k ! : ℤ) (∏ i ∈ range k, (n + (↑i : ℤ)))
have rw : HMod.hMod (α := ℤ) (∏ i ∈ range k, (n + (↑i : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
Tactic: rw [Int.dvd_iff_emod_eq_zero, Finset.prod_int_mod]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
k : ℕ
n : ℤ
⊢ HMod.hMod (α := ℤ) (∏ i ∈ range k, (n + (↑i : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
have simp_rw : HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
Tactic: simp_rw [← Int.emod_add_emod n]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (hypothesis)
Goal:
k : ℕ
n : ℤ
⊢ HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
have hn : 0 ≤ n % (↑k ! : ℤ)
Tactic: have hn : 0 ≤ n % k ! := Int.emod_nonneg n <| Int.natCast_ne_zero.mpr k.factorial_ne_zero
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
Goal:
k : ℕ
n : ℤ
hn : 0 ≤ n % (↑k ! : ℤ)
⊢ HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
have obtain : ∀ (x : ℕ) (hx : n % (↑k ! : ℤ) = (↑x : ℤ)),
  HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
Tactic: obtain ⟨x, hx⟩ := Int.eq_ofNat_of_zero_le hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (hypothesis)
Goal:
k : ℕ
n : ℤ
hn : 0 ≤ n % (↑k ! : ℤ)
x : ℕ
hx : n % (↑k ! : ℤ) = (↑x : ℤ)
⊢ HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
have hdivk : k ! ∣ x.ascFactorial k
Tactic: have hdivk := x.factorial_dvd_ascFactorial k
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (hypothesis)
Goal:
k : ℕ
n : ℤ
hn : 0 ≤ n % (↑k ! : ℤ)
x : ℕ
hx : n % (↑k ! : ℤ) = (↑x : ℤ)
hdivk : k ! ∣ x.ascFactorial k
⊢ HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
have hdivk₁ : Dvd.dvd (α := ℤ) (↑k ! : ℤ) (∏ x_1 ∈ range k, HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑x_1 : ℤ))
Tactic: zify [x.ascFactorial_eq_prod_range k] at hdivk
Cleared hypotheses: hdivk
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
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 : ℤ))
⊢ HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
have rwa : HMod.hMod (α := ℤ) (∏ i ∈ range k, (n % (↑k ! : ℤ) + (↑i : ℤ))) (↑k ! : ℤ) = 0
Tactic: rwa [← Finset.prod_int_mod, ← Int.dvd_iff_emod_eq_zero, hx]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.BigOperators (goal)
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
⊢ HMod.hMod (α := ℤ) (∏ x ∈ range k, (n % (↑k ! : ℤ) + (↑x : ℤ)) % (↑k ! : ℤ)) (↑k ! : ℤ) = 0
have rwa₁ : Dvd.dvd (α := ℤ) (↑k ! : ℤ) (∏ i ∈ range k, (n % (↑k ! : ℤ) + (↑i : ℤ)))
Tactic: rwa [← Finset.prod_int_mod, ← Int.dvd_iff_emod_eq_zero, hx]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Cast (goal)
Goal:
S : Type u_1
inst : Ring S
a : ℕ
⊢ (↑((a - 1) * a.descFactorial 1) : S) = (↑a : S) * HSub.hSub (α := S) (↑a : S) 1
have zero : (↑(HSub.hSub (α := ℕ) 0 1 * descFactorial 0 1) : S) = (↑0 : S) * HSub.hSub (α := S) (↑0 : S) 1
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Cast (goal)
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
⊢ (↑((a - 1) * a.descFactorial 1) : S) = (↑a : S) * HSub.hSub (α := S) (↑a : S) 1
have succ : ∀ (n : ℕ), (↑((n + 1 - 1) * (n + 1).descFactorial 1) : S) = (↑(n + 1) : S) * HSub.hSub (α := S) (↑(n + 1) : S) 1
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
Goal:
n : ℕ
⊢ (n + 1)‼ = (n + 1) * (n - 1)‼
have zero : (HAdd.hAdd (α := ℕ) 0 1)‼ = HAdd.hAdd (α := ℕ) 0 1 * (HSub.hSub (α := ℕ) 0 1)‼
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1)‼ = HAdd.hAdd (α := ℕ) 0 1 * (HSub.hSub (α := ℕ) 0 1)‼
⊢ (n + 1)‼ = (n + 1) * (n - 1)‼
have succ : ∀ (n : ℕ), (n + 1 + 1)‼ = (n + 1 + 1) * (n + 1 - 1)‼
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
Goal:
k : ℕ
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼
have rw : (k + 1 + 1)! = (k + 2) * k‼ * (k + 1)‼
Tactic: rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
Goal:
k : ℕ
rw : (k + 1 + 1)! = (k + 2) * k‼ * (k + 1)‼
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼
have rw₁ : (k + 1).succ * (k + 1)! = (k + 2) * k‼ * (k + 1)‼
Tactic: rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
Goal:
k : ℕ
rw : (k + 1 + 1)! = (k + 2) * k‼ * (k + 1)‼
rw₁ : (k + 1).succ * (k + 1)! = (k + 2) * k‼ * (k + 1)‼
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼
have rw₂ : (k + 1).succ * ((k + 1)‼ * k‼) = (k + 2) * k‼ * (k + 1)‼
Tactic: rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
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)‼
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼
have rw₃ : (k + 1).succ * (k‼ * (k + 1)‼) = (k + 2) * k‼ * (k + 1)‼
Tactic: rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
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)‼
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼
have rw₄ : (k + 1).succ * (k‼ * (k + 1)‼) = (k + 2) * (k‼ * (k + 1)‼)
Tactic: rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
      mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
Goal:
n : ℕ
⊢ (n + 1)‼ ≤ (n + 1)!
have rw : (n + 1)‼ ≤ (n + 1)‼ * n‼
Tactic: rw [factorial_eq_mul_doubleFactorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
Goal:
n : ℕ
⊢ (2 * (n + 1))‼ = HPow.hPow (α := ℕ) 2 (n + 1) * (n + 1)!
have rw : (2 * n + 2) * (HPow.hPow (α := ℕ) 2 n * n !) = HPow.hPow (α := ℕ) 2 n * 2 * ((n + 1) * n !)
Tactic: rw [mul_add, mul_one, doubleFactorial_add_two, factorial, pow_succ, doubleFactorial_two_mul _,
      succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
Goal:
n : ℕ
⊢ (2 * (n + 1))‼ = ∏ i ∈ Finset.range (n + 1), 2 * (i + 1)
have rw : (2 * n + 2)‼ = (2 * n + 2) * (2 * n)‼
Tactic: rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_even _, mul_comm (2 * n)‼,
      (by ring : 2 * (n + 1) = 2 * n + 2)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.DoubleFactorial (goal)
Goal:
n : ℕ
⊢ (2 * (n + 1) + 1)‼ = ∏ i ∈ Finset.range (n + 1), (2 * (i + 1) + 1)
have rw : (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : Semiring A
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑n ! : A)
m : ℕ
hmn : m ≤ n
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)
have obtain : ∀ (k : ℕ) (hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)) (hmn : m ≤ m + k), IsUnit.{u_1} (M := A) (↑m ! : A)
Tactic: obtain ⟨k, rfl⟩ := exists_add_of_le hmn
Cleared hypotheses: n, hn_fac, hmn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (hypothesis)
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 ! : A)
have hn_fac₁ : IsUnit.{u_1} (M := A) (↑(m + 1 + k)! : A)
Tactic: rw [← add_assoc, add_right_comm] at hn_fac
Cleared hypotheses: hn_fac
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (hypothesis)
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 ! : A)
have this : IsUnit.{u_1} (M := A) (↑(m + 1)! : A)
Tactic: have := ih hn_fac
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (hypothesis)
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)
this : IsUnit.{u_1} (M := A) (↑(m + 1)! : A)
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)
have this₁ : IsUnit.{u_1} (M := A) (↑(m + 1) : A) ∧ IsUnit.{u_1} (M := A) (↑m ! : A)
Tactic: rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : Semiring A
m k : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)
have zero : ∀ {m : ℕ} (hn_fac : IsUnit.{u_1} (M := A) (↑(m + 0)! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)
Tactic: induction k generalizing m with
  | zero => simpa using hn_fac
  | succ k ih =>
    rw [← add_assoc, add_right_comm] at hn_fac
    have := ih hn_fac
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff] at this
    exact this.2
Cleared hypotheses: m, k, hn_fac
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : Semiring A
m k : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)
zero : ∀ {m : ℕ} (hn_fac : IsUnit.{u_1} (M := A) (↑(m + 0)! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)
have succ : ∀ (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 ! : A)
Tactic: induction k generalizing m with
  | zero => simpa using hn_fac
  | succ k ih =>
    rw [← add_assoc, add_right_comm] at hn_fac
    have := ih hn_fac
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff] at this
    exact this.2
Cleared hypotheses: m, k, hn_fac
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : Semiring A
K : Type u_2
inst_1 : Semifield K
inst_2 : CharZero K
inst_3 : Algebra K A
n : ℕ
⊢ IsUnit.{u_1} (M := A) (↑n ! : A)
have suffices : IsUnit.{u_2} (M := K) (↑n ! : K)
Tactic: suffices IsUnit (n ! : K) by
    simpa using this.map (algebraMap K A)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (hypothesis)
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
n : ℕ
⊢ IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p
have hp : Nat.Prime p
Tactic: have hp : p.Prime := Fact.out
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p
⊢ IsUnit.{u_1} (M := A) (↑(n + 1)! : A) ↔ n + 1 < p
have succ : ¬p ∣ n + 1 ∧ n + 1 ≤ p ↔ n + 1 < p
Tactic: rw [factorial_succ, cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff, ih.symm.symm,
      ← Nat.add_one_le_iff, CharP.isUnit_natCast_iff hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
n : ℕ
hp : Nat.Prime p
⊢ IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p
have zero : IsUnit.{u_1} (M := A) (↑0! : A) ↔ 0 < p
Tactic: induction n with
  | zero => simp [hp.pos]
  | succ n ih =>
    -- TODO: why is `.symm.symm` needed here!?
    rw [factorial_succ, cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff, ih.symm.symm,
      ← Nat.add_one_le_iff, CharP.isUnit_natCast_iff hp]
    exact ⟨fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h2 (mt (· ▸ dvd_rfl) h1),
      fun h ↦ ⟨not_dvd_of_pos_of_lt (Nat.succ_pos _) h, h.le⟩⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
n : ℕ
hp : Nat.Prime p
zero : IsUnit.{u_1} (M := A) (↑0! : A) ↔ 0 < p
⊢ IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p
have succ : ∀ (n : ℕ) (ih : IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p), IsUnit.{u_1} (M := A) (↑(n + 1)! : A) ↔ n + 1 < p
Tactic: induction n with
  | zero => simp [hp.pos]
  | succ n ih =>
    -- TODO: why is `.symm.symm` needed here!?
    rw [factorial_succ, cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff, ih.symm.symm,
      ← Nat.add_one_le_iff, CharP.isUnit_natCast_iff hp]
    exact ⟨fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h2 (mt (· ▸ dvd_rfl) h1),
      fun h ↦ ⟨not_dvd_of_pos_of_lt (Nat.succ_pos _) h, h.le⟩⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
h : p.Coprime n
⊢ IsUnit.{u_1} (M := A) (↑n : A)
have obtain : ∀ (m : ℕ) (hm : HPow.hPow (α := A) (↑p : A) m = 0), IsUnit.{u_1} (M := A) (↑n : A)
Tactic: obtain ⟨m, hm⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
this : ∃ (a : A) (b : A), HPow.hPow (α := A) (↑p : A) m * a + (↑n : A) * b = 1
⊢ IsUnit.{u_1} (M := A) (↑n : A)
have obtain : ∀ (a b : A) (h : HPow.hPow (α := A) (↑p : A) m * a + (↑n : A) * b = 1), IsUnit.{u_1} (M := A) (↑n : A)
Tactic: obtain ⟨a, b, h⟩ := this
Cleared hypotheses: this