-- 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:
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₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
h' : x₁ < p
⊢ (x₁, x₂).1 % p = x₁ ∧ x₂ = (x₁, x₂).1 / p + (x₁, x₂).2

Tactic:
exact ⟨mod_eq_of_lt h', self_eq_add_left.mpr (div_eq_of_lt h')⟩

Result:
no goals

Proof state:
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))

Tactic:
rw [mem_product, mem_range, mem_range, not_and_or, lt_succ, not_le, not_lt] at h

Result:
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 : n % p < (k % p, k / p).1 ∨ n / p + 1 ≤ (k % p, k / p).2
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Proof state:
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₂ : ℕ
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₂

Tactic:
rw [h, add_mul_mod_self_left, add_mul_div_left _ _ Fin.pos', eq_comm (b := x₂)]

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₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
h' : x₁ < p
⊢ (x₁, x₂).1 % p = x₁ ∧ x₂ = (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 + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)).coeff k =
    (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))

Tactic:
simp only [add_pow, one_pow, mul_one, ← pow_mul, sum_mul_sum]

Result:
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)))

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
h✝ : n / p + 1 ≤ (k % p, k / p).2
⊢ ?m.14644 < ?m.14645

Tactic:
tauto

Result:
no goals

Proof state:
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₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
⊢ k % p = x₁ ∧ k / p = x₂

Tactic:
have h' : x₁ < p := lt_of_lt_of_le hx.left <| mod_lt _ Fin.pos'

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₂ : ℕ
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₂

Proof state:
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))

Tactic:
simp

Result:
no goals

Proof state:
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 : n % p < (k % p, k / p).1 ∨ n / p + 1 ≤ (k % p, k / p).2
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
cases h <;> simp [choose_eq_zero_of_lt (by tauto)]

Result:
no goals

Proof state:
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₂

Tactic:
simp only [mem_product, mem_range] at hx

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₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
⊢ k % p = x₁ ∧ k / p = x₂