awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
⊢ Eq (α := ZMod p)
    (coeff
        (∑ i ∈ range (n % p + 1),
          ∑ j ∈ range (n / p + 1),
            HPow.hPow (α := (ZMod p)[X]) X i * (↑((n % p).choose i) : (ZMod p)[X]) *
              (HPow.hPow (α := (ZMod p)[X]) X (p * j) * (↑((n / p).choose j) : (ZMod p)[X])))
        k :
      ZMod p)
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
        (HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ)) :
      ZMod p)
have conv_lhs : Eq (α := ZMod p)
  (coeff
      (∑ k ∈ range (n % p + 1),
        ∑ k' ∈ range (n / p + 1),
          HPow.hPow (α := (ZMod p)[X]) X (k + p * k') * (↑((n % p).choose k * (n / p).choose k') : (ZMod p)[X]))
      k :
    ZMod p)
  ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
      (HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ)) :
    ZMod p)
Tactic: conv_lhs =>
    enter [1, 2, k, 2, k']
    rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ (k % p, k / p) = (x₁, x₂)
have rw : k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ k % p = x₁ ∧ k / p = x₂
Tactic: rw [Prod.mk.injEq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ k % p = x₁ ∧ k / p = x₂
have mp : k = (x₁, x₂).1 + p * (x₁, x₂).2 → k % p = x₁ ∧ k / p = x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
mp : k = (x₁, x₂).1 + p * (x₁, x₂).2 → k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ k % p = x₁ ∧ k / p = x₂
have mpr : k % p = x₁ ∧ k / p = x₂ → k = (x₁, x₂).1 + p * (x₁, x₂).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (hypothesis)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
⊢ k % p = x₁ ∧ k / p = x₂
have hx₁ : x₁ < n % p + 1 ∧ x₂ < n / p + 1
Tactic: simp only [mem_product, mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (hypothesis)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
x₁ x₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
⊢ k % p = x₁ ∧ k / p = x₂
have h' : x₁ < p
Tactic: have h' : x₁ < p := lt_of_lt_of_le hx.left <| mod_lt _ Fin.pos'
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
x₁ x₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
h' : x₁ < p
⊢ k % p = x₁ ∧ k / p = x₂
have mp : (x₁, x₂).1 % p = x₁ ∧ x₂ = (x₁, x₂).1 / p + (x₁, x₂).2
Tactic: rw [h, add_mul_mod_self_left, add_mul_div_left _ _ Fin.pos', eq_comm (b := x₂)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2
have mpr : k = (k % p, x₂).1 + p * (k % p, x₂).2
Tactic: rw [← h.left, ← h.right, mod_add_div]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
mpr : k = (k % p, x₂).1 + p * (k % p, x₂).2
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2
have mpr₁ : k = (k % p, k / p).1 + p * (k % p, k / p).2
Tactic: rw [← h.left, ← h.right, mod_add_div]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
mpr : k = (k % p, x₂).1 + p * (k % p, x₂).2
mpr₁ : k = (k % p, k / p).1 + p * (k % p, k / p).2
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2
have mpr₂ : k = k
Tactic: rw [← h.left, ← h.right, mod_add_div]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (hypothesis)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
⊢ Eq (α := ZMod p)
    (coeff
        (∑ k ∈ range (n % p + 1),
          ∑ k' ∈ range (n / p + 1),
            HPow.hPow (α := (ZMod p)[X]) X (k + p * k') * (↑((n % p).choose k * (n / p).choose k') : (ZMod p)[X]))
        k :
      ZMod p)
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
        (HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ)) :
      ZMod p)
have h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
Tactic: have h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1),
      k = x.1 + p * x.2 ↔ (k % p, k / p) = x := by
    intro ⟨x₁, x₂⟩ hx
    rw [Prod.mk.injEq]
    constructor <;> intro h
    · simp only [mem_product, mem_range] at hx
      have h' : x₁ < p := lt_of_lt_of_le hx.left <| mod_lt _ Fin.pos'
      rw [h, add_mul_mod_self_left, add_mul_div_left _ _ Fin.pos', eq_comm (b := x₂)]
      exact ⟨mod_eq_of_lt h', right_eq_add.mpr (div_eq_of_lt h')⟩
    · rw [← h.left, ← h.right, mod_add_div]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ Eq (α := ZMod p)
    (coeff
        (∑ k ∈ range (n % p + 1),
          ∑ k' ∈ range (n / p + 1),
            HPow.hPow (α := (ZMod p)[X]) X (k + p * k') * (↑((n % p).choose k * (n / p).choose k') : (ZMod p)[X]))
        k :
      ZMod p)
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
        (HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ)) :
      ZMod p)
have simp : Eq (α := ZMod p)
  (∑ x ∈ range (n % p + 1),
    ∑ x_1 ∈ range (n / p + 1),
      if k = x + p * x_1 then HMul.hMul (α := ZMod p) 1 (↑((n % p).choose x * (n / p).choose x_1) : ZMod p) else 0)
  ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))
Tactic: simp only [finsetSum_coeff, coeff_mul_natCast, coeff_X_pow, ite_mul, zero_mul, ← cast_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ Eq (α := ZMod p)
    (∑ x ∈ range (n % p + 1),
      ∑ x_1 ∈ range (n / p + 1),
        if k = x + p * x_1 then HMul.hMul (α := ZMod p) 1 (↑((n % p).choose x * (n / p).choose x_1) : ZMod p) else 0)
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))
have rw : (if (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1) then
    HMul.hMul (α := ZMod p) 1 (↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) : ZMod p)
  else 0) =
  (Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ)
Tactic: rw [← sum_product', sum_congr rfl (fun a ha ↦ if_congr (h_iff a ha) rfl rfl), sum_ite_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ (if (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1) then
      HMul.hMul (α := ZMod p) 1 (↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) : ZMod p)
    else 0) =
    (Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ)
have pos : ∀ (h : (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1)),
  HMul.hMul (α := ZMod p) 1 (↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) : ZMod p) =
    (Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
pos :
  ∀ (h : (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1)),
    HMul.hMul (α := ZMod p) 1 (↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) : ZMod p) =
      (Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ)
⊢ (if (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1) then
      HMul.hMul (α := ZMod p) 1 (↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) : ZMod p)
    else 0) =
    (Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ)
have neg : ∀ (h : (k % p, k / p) ∉ range (n % p + 1) ×ˢ range (n / p + 1)),
  Eq (α := ZMod p) 0
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (hypothesis)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∉ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ Eq (α := ZMod p) 0
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))
have h₁ : n % p < (k % p, k / p).1 ∨ n / p + 1 ≤ (k % p, k / p).2
Tactic: rw [mem_product, mem_range, mem_range, not_and_or, Nat.lt_succ_iff, not_le, not_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : n % p < (k % p, k / p).1 ∨ n / p + 1 ≤ (k % p, k / p).2
⊢ Eq (α := ZMod p) 0
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))
have neg : n % p < (k % p, k / p).1 →
  Eq (α := ZMod p) 0
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : n % p < (k % p, k / p).1 ∨ n / p + 1 ≤ (k % p, k / p).2
neg :
  n % p < (k % p, k / p).1 →
    Eq (α := ZMod p) 0
      ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))
⊢ Eq (α := ZMod p) 0
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))
have neg₁ : n / p + 1 ≤ (k % p, k / p).2 →
  Eq (α := ZMod p) 0
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
⊢ n.choose k ≡ (n % p).choose (k % p) * (n / p).choose (k / p) [MOD p]
have rw : (↑(n.choose k) : ℤ) ≡ (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: rw [← Int.natCast_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑(∏ i ∈ range a.succ, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
have rw : HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
    (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
  HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) *
    (↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) : ℤ) [ZMOD
  (↑p : ℤ)]
Tactic: rw [prod_range_succ, cast_mul, ← mul_assoc, mul_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
        (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) *
      (↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
have h₁ : (↑((n / p ^ a).choose (k / p ^ a)) : ℤ) ≡
  HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
    (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
  (↑p : ℤ)]
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
⊢ (↑((n / p ^ a).choose (k / p ^ a)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
have h₁ : HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
  HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
    (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
  (↑p : ℤ)]
Tactic: apply choose_modEq_choose_mod_mul_choose_div.trans
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
have h₁ : HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
  HMul.hMul (α := ℤ) (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ)
    (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
  (↑p : ℤ)]
Tactic: simp_rw [pow_succ, Nat.div_div_eq_div_mul, mul_comm, Int.ModEq.refl]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
h₁ :
  HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
have h₂ : HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ) ≡
  HMul.hMul (α := ℤ) (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ)
    (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
  (↑p : ℤ)]
Tactic: simp_rw [pow_succ, Nat.div_div_eq_div_mul, mul_comm, Int.ModEq.refl]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
h₁ :
  HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
h₂ :
  HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ)
      (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
have h₃ : HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / (p * p ^ a)).choose (k / (p * p ^ a))) : ℤ) ≡
  HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ)
    (↑((n / (p * p ^ a)).choose (k / (p * p ^ a))) : ℤ) [ZMOD
  (↑p : ℤ)]
Tactic: simp_rw [pow_succ, Nat.div_div_eq_div_mul, mul_comm, Int.ModEq.refl]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ (↑(n.choose k) : ℤ) ≡ ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
have apply : HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
    (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
  ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: apply (choose_modEq_choose_mul_prod_range_choose a).trans
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
have simp_rw : HMul.hMul (α := ℤ) (↑(choose 0 (k / p ^ a)) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
  ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
simp_rw :
  HMul.hMul (α := ℤ) (↑(choose 0 (k / p ^ a)) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
have simp_rw₁ : HMul.hMul (α := ℤ) (↑(choose 0 0) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
  ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
simp_rw :
  HMul.hMul (α := ℤ) (↑(choose 0 (k / p ^ a)) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₁ :
  HMul.hMul (α := ℤ) (↑(choose 0 0) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
have simp_rw₂ : HMul.hMul (α := ℤ) (↑1 : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
  ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
simp_rw :
  HMul.hMul (α := ℤ) (↑(choose 0 (k / p ^ a)) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₁ :
  HMul.hMul (α := ℤ) (↑(choose 0 0) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₂ :
  HMul.hMul (α := ℤ) (↑1 : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
have simp_rw₃ : HMul.hMul (α := ℤ) 1 (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
  ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]