-- 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 : ℕ))
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 : ℕ))
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 (α := ℕ) ((factorization (∏ x ∈ Ico 1 (p * n + 1), x) : (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 : ℕ) =
  ∑ x ∈ Ico 1 (p * n + 1), (x.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]