-- Mathlib/NumberTheory/Multiplicity.lean
theorem odd_sq_dvd_geom_sum₂_sub (hp : Odd p) :
    (p : R) ^ 2 ∣ (∑ i ∈ range p, (a + p * b) ^ i * a ^ (p - 1 - i)) - p * a ^ (p - 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
⊢ ↑p ^ 2 ∣ ∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)

Tactic:
have h1 : ∀ (i : ℕ),
    (p : R) ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * i + a ^ i) := by
  intro i
  calc
    ↑p ^ 2 ∣ (↑p * b) ^ 2 := by simp only [mul_pow, dvd_mul_right]
    _ ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) := by
      simp only [sq_dvd_add_pow_sub_sub (↑p * b) a i, ← sub_sub]

Result:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 : ∀ (i : ℕ), ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
⊢ ↑p ^ 2 ∣ ∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)

Tactic:
simp only [Nat.cast_sum]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 : ∀ (i : ℕ), ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
⊢ ↑p ^ 2 ∣ ∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)

Tactic:
simp_rw [← mem_span_singleton, ← Ideal.Quotient.eq] at *

Result:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
⊢ (Ideal.Quotient.mk (span {↑p ^ 2})) (∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i)) =
    (Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1))

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) (↑p * b * (a ^ (p - 2) * ↑(∑ x ∈ range p, x))) = 0

Tactic:
simp only [Finset.sum_range_id]

Result:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) (↑p * b * (a ^ (p - 2) * ↑(p * (p - 1) / 2))) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x + (p - 1 - x))) =
    (Ideal.Quotient.mk (span {s})) (∑ _x ∈ range p, a ^ (p - 1))

Tactic:
have : ∀ (x : ℕ), (hx : x ∈ range p) → a ^ (x + (p - 1 - x)) = a ^ (p - 1) := by
  intro x hx
  rw [← Nat.add_sub_assoc _ x, Nat.add_sub_cancel_left]
  exact Nat.le_sub_one_of_lt (Finset.mem_range.mp hx)

Result:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∀ x ∈ range p, a ^ (x + (p - 1 - x)) = a ^ (p - 1)
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x + (p - 1 - x))) =
    (Ideal.Quotient.mk (span {s})) (∑ _x ∈ range p, a ^ (p - 1))

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    (Ideal.Quotient.mk (span {s})) (↑p * b * ∑ x ∈ range p, a ^ (p - 2) * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))

Tactic:
simp only [Finset.mul_sum, ← mul_assoc, ← pow_add]

Result:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, ↑p * b * a ^ (p - 2) * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))

Proof state:
case e_a.h.e_6.h.e_f
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (fun x => a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x) = fun x => a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))

Tactic:
simp [pow_add a, mul_assoc]

Result:
no goals