awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
⊢ (↑((a + b).choose a) : K) = (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K)
have rw : (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑(a + b - a)! : K) =
  (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K)
Tactic: rw [cast_choose K (le_add_right _ _), Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
rw :
  (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑(a + b - a)! : K) =
    (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K)
⊢ (↑((a + b).choose a) : K) = (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K)
have rw₁ : (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K) = (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K)
Tactic: rw [cast_choose K (le_add_right _ _), Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : ℕ
⊢ (↑(a.choose 2) : K) = (↑a : K) * HSub.hSub (α := K) (↑a : K) 1 / 2
have rw : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.descFactorial 2) : K) 2
Tactic: rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
    cast_mul, cast_two, eq_div_iff_mul_eq two_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : ℕ
rw : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.descFactorial 2) : K) 2
⊢ (↑(a.choose 2) : K) = (↑a : K) * HSub.hSub (α := K) (↑a : K) 1 / 2
have rw₁ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2! * a.choose 2) : K) 2
Tactic: rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
    cast_mul, cast_two, eq_div_iff_mul_eq two_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : ℕ
rw : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.descFactorial 2) : K) 2
rw₁ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2! * a.choose 2) : K) 2
⊢ (↑(a.choose 2) : K) = (↑a : K) * HSub.hSub (α := K) (↑a : K) 1 / 2
have rw₂ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2 * a.choose 2) : K) 2
Tactic: rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
    cast_mul, cast_two, eq_div_iff_mul_eq two_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : ℕ
rw : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.descFactorial 2) : K) 2
rw₁ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2! * a.choose 2) : K) 2
rw₂ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2 * a.choose 2) : K) 2
⊢ (↑(a.choose 2) : K) = (↑a : K) * HSub.hSub (α := K) (↑a : K) 1 / 2
have rw₃ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.choose 2 * 2) : K) 2
Tactic: rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
    cast_mul, cast_two, eq_div_iff_mul_eq two_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : ℕ
rw : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.descFactorial 2) : K) 2
rw₁ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2! * a.choose 2) : K) 2
rw₂ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2 * a.choose 2) : K) 2
rw₃ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.choose 2 * 2) : K) 2
⊢ (↑(a.choose 2) : K) = (↑a : K) * HSub.hSub (α := K) (↑a : K) 1 / 2
have rw₄ : (↑(a.choose 2) : K) = HMul.hMul (α := K) (↑(a.choose 2) : K) (↑2 : K) / 2
Tactic: rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
    cast_mul, cast_two, eq_div_iff_mul_eq two_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : ℕ
rw : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.descFactorial 2) : K) 2
rw₁ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2! * a.choose 2) : K) 2
rw₂ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2 * a.choose 2) : K) 2
rw₃ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.choose 2 * 2) : K) 2
rw₄ : (↑(a.choose 2) : K) = HMul.hMul (α := K) (↑(a.choose 2) : K) (↑2 : K) / 2
⊢ (↑(a.choose 2) : K) = (↑a : K) * HSub.hSub (α := K) (↑a : K) 1 / 2
have rw₅ : (↑(a.choose 2) : K) = HMul.hMul (α := K) (↑(a.choose 2) : K) 2 / 2
Tactic: rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
    cast_mul, cast_two, eq_div_iff_mul_eq two_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : ℕ
rw : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.descFactorial 2) : K) 2
rw₁ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2! * a.choose 2) : K) 2
rw₂ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2 * a.choose 2) : K) 2
rw₃ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.choose 2 * 2) : K) 2
rw₄ : (↑(a.choose 2) : K) = HMul.hMul (α := K) (↑(a.choose 2) : K) (↑2 : K) / 2
rw₅ : (↑(a.choose 2) : K) = HMul.hMul (α := K) (↑(a.choose 2) : K) 2 / 2
⊢ (↑(a.choose 2) : K) = (↑a : K) * HSub.hSub (α := K) (↑a : K) 1 / 2
have rw₆ : HMul.hMul (α := K) (↑(a.choose 2) : K) 2 = HMul.hMul (α := K) (↑(a.choose 2) : K) 2
Tactic: rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
    cast_mul, cast_two, eq_div_iff_mul_eq two_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Dvd (hypothesis)
Goal:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
⊢ p ∣ (a + b).choose a
have h₁ : p ∣ (a + b)!
Tactic: have h₁ : p ∣ (a + b)! := hp.dvd_factorial.2 h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Dvd (hypothesis)
Goal:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : p ∣ (a + b)!
⊢ p ∣ (a + b).choose a
have h₂ : (p ∣ (a + b).choose a ∨ p ≤ a) ∨ p ≤ b
Tactic: rw [← add_choose_mul_factorial_mul_factorial, ← choose_symm_add, hp.dvd_mul, hp.dvd_mul,
    hp.dvd_factorial, hp.dvd_factorial] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Dvd (goal)
Goal:
p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.choose a)
have rw : p.Coprime (b.descFactorial a / a !)
Tactic: rw [Nat.choose_eq_descFactorial_div_factorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ((n + 1)!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : (((n + 1) * n !).factorization : (a : ℕ) → ℕ) p =
  HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [factorial_succ, factorization_mul (zero_ne_add_one n).symm n.factorial_ne_zero,
          coe_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
rw :
  (((n + 1) * n !).factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ((n + 1)!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₁ : ((n + 1).factorization + n !.factorization : (a : ℕ) → ℕ) p =
  HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [factorial_succ, factorization_mul (zero_ne_add_one n).symm n.factorial_ne_zero,
          coe_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
rw :
  (((n + 1) * n !).factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₁ :
  ((n + 1).factorization + n !.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ((n + 1)!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₂ : HAdd.hAdd (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑(n + 1).factorization : (a : ℕ) → ℕ)
    (⇑n !.factorization : (a : ℕ) → ℕ) p =
  HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [factorial_succ, factorization_mul (zero_ne_add_one n).symm n.factorial_ne_zero,
          coe_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
rw :
  (((n + 1) * n !).factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₁ :
  ((n + 1).factorization + n !.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₂ :
  HAdd.hAdd (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑(n + 1).factorization : (a : ℕ) → ℕ)
      (⇑n !.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ((n + 1)!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₃ : HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) =
  HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [factorial_succ, factorization_mul (zero_ne_add_one n).symm n.factorial_ne_zero,
          coe_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) =
    #({i ∈ Ico 1 b | p ^ i ∣ n + 1}) + ∑ i ∈ Ico 1 b, n / p ^ i
have rw : ((n + 1).factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 b | p ^ i ∣ n + 1})
Tactic: rw [factorization_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), add_left_inj]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
n p : ℕ
hp : Prime p
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have h0 : 2 ≤ p
Tactic: have h0 : 2 ≤ p := hp.two_le
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have h1 : 1 ≤ p * n + 1
Tactic: have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)
have linarith : p * (n + 1) < p * n + 1 →
  HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 (↑p : ℤ) +
      ((↑p : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - (HMul.hMul (α := ℤ) (↑p : ℤ) (↑n : ℤ) + 1)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
linarith :
  p * (n + 1) < p * n + 1 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 (↑p : ℤ) +
        ((↑p : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - (HMul.hMul (α := ℤ) (↑p : ℤ) (↑n : ℤ) + 1)) =
      0
⊢ p * n + 1 ≤ p * (n + 1)
have linarith₁ : p * (n + 1) < p * n + 1 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have h2 : p * n + 1 ≤ p * (n + 1)
Tactic: have h2 : p * n + 1 ≤ p * (n + 1) := by linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have h3 : p * n + 1 ≤ p * (n + 1) + 1
Tactic: have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have h : ¬p ∣ m
Tactic: apply factorization_eq_zero_of_not_dvd
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have h4 : ∀ (m : ℕ) (hm : m ∈ Ico (p * n + 1) (p * (n + 1))), Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: have h4 m (hm : m ∈ Ico (p * n + 1) (p * (n + 1))) : m.factorization p = 0 := by
    apply factorization_eq_zero_of_not_dvd
    exact not_dvd_of_lt_of_lt_mul_succ (mem_Ico.mp hm).left (mem_Ico.mp hm).right
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ) (hm : m ∈ Ico (p * n + 1) (p * (n + 1))), Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have rw : (factorization (∏ x ∈ Ico 1 (p * (n + 1) + 1), x) : (a : ℕ) → ℕ) p =
  HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
      (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
    1
Tactic: rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), ← sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2,
    ← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm,
    coe_add, Pi.add_apply, hp.factorization_self, sum_congr rfl h4, sum_const_zero, zero_add,
    add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ) (hm : m ∈ Ico (p * n + 1) (p * (n + 1))), Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw :
  (factorization (∏ x ∈ Ico 1 (p * (n + 1) + 1), x) : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have rw₁ : ∑ x ∈ Ico 1 (p * (n + 1) + 1), (x.factorization : (a : ℕ) → ℕ) p =
  HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
      (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
    1
Tactic: rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), ← sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2,
    ← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm,
    coe_add, Pi.add_apply, hp.factorization_self, sum_congr rfl h4, sum_const_zero, zero_add,
    add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ) (hm : m ∈ Ico (p * n + 1) (p * (n + 1))), Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw :
  (factorization (∏ x ∈ Ico 1 (p * (n + 1) + 1), x) : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
rw₁ :
  ∑ x ∈ Ico 1 (p * (n + 1) + 1), (x.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have rw₂ : HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p)
    (∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), (i.factorization : (a : ℕ) → ℕ) p) =
  HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
      (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
    1
Tactic: rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), ← sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2,
    ← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm,
    coe_add, Pi.add_apply, hp.factorization_self, sum_congr rfl h4, sum_const_zero, zero_add,
    add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ) (hm : m ∈ Ico (p * n + 1) (p * (n + 1))), Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw :
  (factorization (∏ x ∈ Ico 1 (p * (n + 1) + 1), x) : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
rw₁ :
  ∑ x ∈ Ico 1 (p * (n + 1) + 1), (x.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
rw₂ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p)
      (∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), (i.factorization : (a : ℕ) → ℕ) p) =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have rw₃ : HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p)
    (∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), (i.factorization : (a : ℕ) → ℕ) p) =
  HAdd.hAdd (α := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
    (HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ))
Tactic: rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), ← sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2,
    ← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm,
    coe_add, Pi.add_apply, hp.factorization_self, sum_congr rfl h4, sum_const_zero, zero_add,
    add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ) (hm : m ∈ Ico (p * n + 1) (p * (n + 1))), Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw :
  (factorization (∏ x ∈ Ico 1 (p * (n + 1) + 1), x) : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
rw₁ :
  ∑ x ∈ Ico 1 (p * (n + 1) + 1), (x.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
rw₂ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p)
      (∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), (i.factorization : (a : ℕ) → ℕ) p) =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
rw₃ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p)
      (∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), (i.factorization : (a : ℕ) → ℕ) p) =
    HAdd.hAdd (α := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ))
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have rw₄ : ∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p +
    HAdd.hAdd (α := ℕ) (β := ℕ) (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), (k.factorization : (a : ℕ) → ℕ) p : ℕ)
      (((p * (n + 1)).factorization : (a : ℕ) → ℕ) p : ℕ) =
  HAdd.hAdd (α := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
    (HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ))
Tactic: rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), ← sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2,
    ← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm,
    coe_add, Pi.add_apply, hp.factorization_self, sum_congr rfl h4, sum_const_zero, zero_add,
    add_comm 1]