-- Mathlib/Data/Nat/Choose/Lucas.lean
theorem choose_modEq_choose_mod_mul_choose_div :
    choose n k ≡ choose (n % p) (k % p) * choose (n / p) (k / p) [ZMOD p]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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
⊢ (∑ x ∈ range (n % p + 1),
      ∑ x_1 ∈ range (n / p + 1), if k = x + p * x_1 then 1 * ↑((n % p).choose x * (n / p).choose x_1) else 0) =
    (Int.castRingHom (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]

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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
      1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2)
    else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)

Tactic:
simpa using add_pow_eq_mul_pow_add_pow_div_char (X : (ZMod p)[X]) 1 p _

Result:
no goals

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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
      1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2)
    else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
split_ifs with h

Result:
case pos
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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)
⊢ 1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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)
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ ↑(n.choose k) ≡ ↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)) [ZMOD ↑p]

Tactic:
simp only [← ZMod.intCast_eq_intCast_iff, Int.cast_mul, Int.cast_ofNat,
  ← coeff_X_add_one_pow _ n k, ← eq_intCast (Int.castRingHom (ZMod p)), ← coeff_map,
  Polynomial.map_pow, Polynomial.map_add, Polynomial.map_one, map_X, decompose]

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ ((X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)).coeff k =
    (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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₂

Tactic:
constructor <;> intro h

Result:
case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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₂

case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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₂)

Tactic:
rw [Prod.mk.injEq]

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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₂

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x

Tactic:
intro ⟨x₁, x₂⟩ hx

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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₂)

Proof state:
case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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

Tactic:
rw [← h.left, ← h.right, mod_add_div]

Result:
no goals

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ (∑ i ∈ range (n % p + 1),
          ∑ j ∈ range (n / p + 1), X ^ i * ↑((n % p).choose i) * (X ^ (p * j) * ↑((n / p).choose j))).coeff
      k =
    (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / 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]

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ (∑ k ∈ range (n % p + 1), ∑ k' ∈ range (n / p + 1), X ^ (k + p * k') * ↑((n % p).choose k * (n / p).choose k')).coeff
      k =
    (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(n.choose k) ≡ ↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)) [ZMOD ↑p]

Tactic:
have decompose : ((X : (ZMod p)[X]) + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p) := by
  simpa using add_pow_eq_mul_pow_add_pow_div_char (X : (ZMod p)[X]) 1 p _

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ ↑(n.choose k) ≡ ↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)) [ZMOD ↑p]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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
⊢ (∑ k ∈ range (n % p + 1), ∑ k' ∈ range (n / p + 1), X ^ (k + p * k') * ↑((n % p).choose k * (n / p).choose k')).coeff
      k =
    (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))

Tactic:
simp only [finset_sum_coeff, coeff_mul_natCast, coeff_X_pow, ite_mul, zero_mul, ← cast_mul]

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (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
⊢ (∑ x ∈ range (n % p + 1),
      ∑ x_1 ∈ range (n / p + 1), if k = x + p * x_1 then 1 * ↑((n % p).choose x * (n / p).choose x_1) else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))