Theorem: Polynomial.dvd_C_mul_X_sub_one_pow_add_one (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ (C a * X - 1) ^ p + 1
Tactic:
rw [sub_eq_add_neg, add_pow_prime_eq hpri, (hpri.odd_of_ne_two hp).neg_pow, one_pow,
  mul_pow, ← C.map_pow, add_comm, add_comm (_ * _), ← add_assoc, ← add_assoc,
  add_right_neg, zero_add]
State after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ C (a ^ p) * X ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)

State before:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ C (a ^ p) * X ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
Tactic:
refine dvd_add (dvd_mul_of_dvd_left (_root_.map_dvd C h₁) _) ((_root_.map_dvd C h₂).trans ?_)
State after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C (↑p * a) ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)

State before:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C (↑p * a) ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
Tactic:
rw [map_mul, map_natCast]
State after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ ↑p * C a ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)

State before:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ ↑p * C a ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
Tactic:
exact mul_dvd_mul_left _ (Finset.dvd_sum (fun x hx ↦ dvd_mul_of_dvd_left
  (dvd_mul_of_dvd_left (dvd_pow (dvd_mul_right _ _) (Finset.mem_Ioo.mp hx).1.ne.symm) _) _))
State after:
no goals