awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : n < p
pos : ∀ (hnk : n < k), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg : ∀ (hnk : k ≤ n), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
by_cases! hnk : n < k
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : n < p
hnk : n < k
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp [choose_eq_zero_of_lt hnk]

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : n < p
hnk : k ≤ n
neg : Eq (α := ℕ) (((n ! / (k ! * (n - k)!)).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg₁ : Eq (α := ℕ) ((n !.factorization - (k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg₂ :
  HSub.hSub (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n !.factorization : (a : ℕ) → ℕ)
      (⇑(k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p =
    0
neg₃ :
  HSub.hSub (α := ℕ) (β := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
      (((k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) =
    0
neg₄ : HSub.hSub (α := ℕ) (β := ℕ) (0 : ℕ) (((k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) = 0
neg₅ neg₆ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rw [choose_eq_factorial_div_factorial hnk,
    factorization_div (factorial_mul_factorial_dvd_factorial hnk), Finsupp.coe_tsub,
    Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]

Premises used: Nat.factorial_mul_factorial_dvd_factorial, Nat.factorization_div, Finsupp.coe_tsub, zero_tsub, Pi.sub_apply, Nat.choose_eq_factorial_div_factorial, Nat.factorization_factorial_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n : ℕ
h : 2 * n < p
⊢ Eq (α := ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
factorization_choose_eq_zero_of_lt h

Premises used: Nat.centralBinom, Nat.factorization_choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n : ℕ
h_pos : LT.lt (α := ℕ) (0 : ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ p ≤ 2 * n

Tactic:
le_of_not_gt (pos_iff_ne_zero.mp h_pos ∘ factorization_centralBinom_eq_zero_of_two_mul_lt)

Premises used: Function.comp, le_of_not_gt, Nat.factorization_centralBinom_eq_zero_of_two_mul_lt, Iff.mp, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n k : ℕ
hkn : k ≤ n
rw : (n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
| n.choose k

Tactic:
rw [← prod_factorization_pow_eq_self (choose_ne_zero hkn)]

Premises used: Nat.choose_ne_zero, Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n k : ℕ
hkn : k ≤ n
conv_rhs :
  Eq (α := ℕ) (∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ))
    ((n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
⊢ ∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) = n.choose k

Tactic:
conv_rhs => rw [← prod_factorization_pow_eq_self (choose_ne_zero hkn)]

Premises used: Nat.choose_ne_zero, Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n k : ℕ
hkn : k ≤ n
rw :
  Eq (α := ℕ) ((n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
    (∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ))
⊢ Eq (α := ℕ) (∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ))
    ((n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n k : ℕ
hkn : k ≤ n
h : (n.choose k).factorization.support ⊆ Finset.range (n + 1)
hf :
  ∀ x ∈ Finset.range (n + 1),
    x ∉ (n.choose k).factorization.support →
      Eq (α := ℕ) ((fun (x1 x2 : ℕ) ↦ x1 ^ x2) x (((n.choose k).factorization : (a : ℕ) → ℕ) x)) 1
⊢ Eq (α := ℕ) ((n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
    (∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
apply Finset.prod_subset

Premises used: Finset.prod_subset
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
h : p < n + 1
⊢ p ∈ Finset.range (n + 1)

Tactic:
rw [Finset.mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
h : ∀ (hp : n + 1 ≤ p), p ∉ (n.choose k).factorization.support
⊢ p < n + 1

Tactic:
contrapose! hp
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
h : ¬Ne (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h₁ : Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h₂ h₃ : Eq (α := ℕ) 0 0
⊢ p ∉ (n.choose k).factorization.support

Tactic:
rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]

Premises used: Finsupp.mem_support_iff, Classical.not_not, Nat.factorization_choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hf :
  p ∈ Finset.range (n + 1) →
    p ∉ (n.choose k).factorization.support →
      Eq (α := ℕ) ((fun (x1 x2 : ℕ) ↦ x1 ^ x2) p (((n.choose k).factorization : (a : ℕ) → ℕ) p)) 1
⊢ p ∈ Finset.range (n + 1) →
    p ∉ (n.choose k).factorization.support →
      Eq (α := ℕ) ((fun (x1 x2 : ℕ) ↦ x1 ^ x2) p (((n.choose k).factorization : (a : ℕ) → ℕ) p)) 1

Tactic:
_
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
h : p ∈ Finset.range (n + 1)
h2 : p ∉ (n.choose k).factorization.support
⊢ Eq (α := ℕ) ((fun (x1 x2 : ℕ) ↦ x1 ^ x2) p (((n.choose k).factorization : (a : ℕ) → ℕ) p)) 1

Tactic:
simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]

Premises used: Iff.mpr, Finsupp.mem_support_iff, Classical.not_not, mt, Iff.mp
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n : ℕ
hkn : n ≤ 2 * n
⊢ ∏ p ∈ Finset.range (2 * n + 1), HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) =
    n.centralBinom

Tactic:
apply prod_pow_factorization_choose

Premises used: Nat.prod_pow_factorization_choose
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n : ℕ
⊢ n ≤ 2 * n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
⊢ 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)

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

Premises used: OfNat.ofNat, Polynomial.X, add_pow_eq_mul_pow_add_pow_div_char
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
⊢ 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)

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 _
-- Module: Mathlib.Data.Nat.Choose.Lucas
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)
simp :
  (HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)).coeff k =
    (Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
      (HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ))
⊢ (↑(n.choose k) : ℤ) ≡ HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ) [ZMOD
    (↑p : ℤ)]

Tactic:
simp only [← ZMod.intCast_eq_intCast_iff,
    ← 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]

Premises used: Polynomial.map_one, Polynomial.coeff_map, Polynomial.map_pow, Polynomial.map_add, Polynomial.map_X, eq_intCast, ZMod, ZMod.intCast_eq_intCast_iff, Int.castRingHom, Polynomial.coeff_X_add_one_pow
-- Module: Mathlib.Data.Nat.Choose.Lucas
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)
simp :
  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)
⊢ (HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)).coeff k =
    (Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
      (HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ))

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

Premises used: one_pow, pow_mul, add_pow, mul_one, Finset.sum_mul_sum
-- Module: Mathlib.Data.Nat.Choose.Lucas
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 :
  ∀ (k k' : ℕ),
    HPow.hPow (α := (ZMod p)[X]) X k * (↑((n % p).choose k) : (ZMod p)[X]) *
      (HPow.hPow (α := (ZMod p)[X]) X (p * k') * (↑((n / p).choose k') : (ZMod p)[X]))
| 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

Tactic:
enter [1, 2, k, 2, k']
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k_1 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)
k k' : ℕ
h : HPow.hPow (α := (ZMod p)[X]) X (k + p * k') * (↑((n % p).choose k * (n / p).choose k') : (ZMod p)[X])
| HPow.hPow (α := (ZMod p)[X]) X k * (↑((n % p).choose k) : (ZMod p)[X]) *
    (HPow.hPow (α := (ZMod p)[X]) X (p * k') * (↑((n / p).choose k') : (ZMod p)[X]))

Tactic:
rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]

Premises used: HMul.hMul, mul_assoc, pow_add, Nat.cast_mul, HPow.hPow, mul_right_comm, Polynomial.X
-- Module: Mathlib.Data.Nat.Choose.Lucas
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 : ∀ (k k' : ℕ), HPow.hPow (α := (ZMod p)[X]) X (k + p * k') * (↑((n % p).choose k * (n / p).choose k') : (ZMod p)[X])
| 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

Tactic:
enter [1, 2, k, 2, k']
    rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]

Premises used: mul_assoc, pow_add, Nat.cast_mul
-- Module: Mathlib.Data.Nat.Choose.Lucas
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)
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)
⊢ 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)

Tactic:
conv_lhs =>
    enter [1, 2, k, 2, k']
    rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]

Premises used: mul_assoc, pow_add, Nat.cast_mul
-- Module: Mathlib.Data.Nat.Choose.Lucas
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)
rw : k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ (k % p, k / p) = (x₁, x₂)

Tactic:
rw [Prod.mk.injEq]

Premises used: Prod.mk.injEq
-- Module: Mathlib.Data.Nat.Choose.Lucas
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₂
mpr : k % p = x₁ ∧ k / p = x₂ → k = (x₁, x₂).1 + p * (x₁, x₂).2
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ k % p = x₁ ∧ k / p = x₂

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Choose.Lucas
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
⊢ x₁ < n % p + 1 ∧ x₂ < n / p + 1

Tactic:
simp only [mem_product, mem_range] at hx

Premises used: Finset.mem_range, Finset.mem_product
-- Module: Mathlib.Data.Nat.Choose.Lucas
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
⊢ x₁ < p

Tactic:
have h' : x₁ < p := lt_of_lt_of_le hx.left <| mod_lt _ Fin.pos'
-- Module: Mathlib.Data.Nat.Choose.Lucas
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
mp : (x₁, x₂).1 % p = x₁ ∧ x₂ = (x₁, x₂).1 / p + (x₁, x₂).2
⊢ k % p = x₁ ∧ k / p = x₂

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

Premises used: eq_comm, Nat.add_mul_div_left, Fin.pos', Nat.add_mul_mod_self_left
-- Module: Mathlib.Data.Nat.Choose.Lucas
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
⊢ (x₁, x₂).1 % p = x₁ ∧ x₂ = (x₁, x₂).1 / p + (x₁, x₂).2

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

Premises used: Iff.mpr, Nat.mod_eq_of_lt, And.intro, Nat.div_eq_of_lt, right_eq_add
-- Module: Mathlib.Data.Nat.Choose.Lucas
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
⊢ (x₁, x₂).1 % p = x₁ ∧ x₂ = (x₁, x₂).1 / p + (x₁, x₂).2

Tactic:
exact ⟨mod_eq_of_lt h', right_eq_add.mpr (div_eq_of_lt h')⟩
-- Module: Mathlib.Data.Nat.Choose.Lucas
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
mpr₂ mpr₃ : k = k
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2

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

Premises used: Nat.mod_add_div, And.right, And.left
-- Module: Mathlib.Data.Nat.Choose.Lucas
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 ∈ 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]
-- Module: Mathlib.Data.Nat.Choose.Lucas
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
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)) : ℤ))
⊢ 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:
simp only [finsetSum_coeff, coeff_mul_natCast, coeff_X_pow, ite_mul, zero_mul, ← cast_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.coeff_X_pow, Polynomial.finsetSum_coeff, Nat.cast_mul, ite_mul, Polynomial.coeff_mul_natCast
-- Module: Mathlib.Data.Nat.Choose.Lucas
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
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)) : ℤ)
⊢ 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:
rw [← sum_product', sum_congr rfl (fun a ha ↦ if_congr (h_iff a ha) rfl rfl), sum_ite_eq]

Premises used: if_congr, Finset.sum_product', Finset.sum_congr, Finset.sum_ite_eq, rfl
-- Module: Mathlib.Data.Nat.Choose.Lucas
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)) : ℤ)
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)) : ℤ))
⊢ (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:
split_ifs with h
-- Module: Mathlib.Data.Nat.Choose.Lucas
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)
⊢ 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:
simp
-- Module: Mathlib.Data.Nat.Choose.Lucas
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)
⊢ 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

Premises used: not_le, Finset.mem_range, not_lt, Nat.lt_succ_iff, not_and_or, Finset.mem_product
-- Module: Mathlib.Data.Nat.Choose.Lucas
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)) : ℤ))
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)) : ℤ))
⊢ Eq (α := ZMod p) 0
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))

Tactic:
cases h
-- Module: Mathlib.Data.Nat.Choose.Lucas
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 < (k % p, k / p).1

Tactic:
tauto
-- Module: Mathlib.Data.Nat.Choose.Lucas
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
⊢ Eq (α := ZMod p) 0
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))

Tactic:
simp [choose_eq_zero_of_lt (by tauto)]

Premises used: Nat.choose_eq_zero_of_lt