R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : R
p : ℕ
hp : Odd p
h1 : ∀ (i : ℕ), ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
⊢ ↑p ^ 2 ∣ ∑ i in range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : R
p : ℕ
hp : Odd p
⊢ ↑p ^ 2 ∣ ∑ i in range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)
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]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i)) =
    ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1))
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : R
p : ℕ
hp : Odd p
h1 : ∀ (i : ℕ), ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
⊢ ↑p ^ 2 ∣ ∑ i in range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)
simp_rw [← mem_span_singleton, ← Ideal.Quotient.eq] at *
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 {↑p ^ 2})) (∑ i in range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i)) =
    ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1))
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i)) =
    ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1))
let s : R := (p : R)^2
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : R
p : ℕ
hp : Odd p
i : ℕ
⊢ ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : R
p : ℕ
hp : Odd p
⊢ ∀ (i : ℕ), ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
intro i
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : R
p : ℕ
hp : Odd p
i : ℕ
⊢ ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ 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]
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : R
p : ℕ
hp : Odd p
i : ℕ
⊢ ↑p ^ 2 ∣ (↑p * b) ^ 2
simp only [mul_pow, dvd_mul_right]
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : R
p : ℕ
hp : Odd p
i : ℕ
⊢ (↑p * b) ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
simp only [sq_dvd_add_pow_sub_sub (↑p * b) a i, ← sub_sub]
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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})) (∑ i in range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i)) =
    ∑ i in range p, ↑(Ideal.Quotient.mk (span {s})) ((a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) * a ^ (p - 1 - i))
simp_rw [RingHom.map_geom_sum₂, ← map_pow, h1, ← _root_.map_mul]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p,
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (x - 1) * a ^ (p - 1 - x) * ↑p * b * ↑x + a ^ x * a ^ (p - 1 - x)) =
    ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x + (p - 1 - x)))
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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
⊢ ∑ i in range p, ↑(Ideal.Quotient.mk (span {s})) ((a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) * a ^ (p - 1 - i)) =
    ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (x + (p - 1 - x)))
ring
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 {↑p ^ 2})) (∑ x in range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x + (p - 1 - x))) =
    ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x + (p - 1 - x)))
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p,
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (x - 1) * a ^ (p - 1 - x) * ↑p * b * ↑x + a ^ x * a ^ (p - 1 - x)) =
    ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x + (p - 1 - x)))
simp only [← pow_add, map_add, Finset.sum_add_distrib, ← map_sum]
case e_a.h.e_6.h.e_f
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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)))
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 {↑p ^ 2})) (∑ x in range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x + (p - 1 - x))) =
    ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, a ^ (x + (p - 1 - x)))
congr
no goals
case e_a.h.e_6.h.e_f
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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)))
simp [pow_add a, mul_assoc]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, a ^ (x + (p - 1 - x))) =
    ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (p - 1))
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (x + (p - 1 - x))) =
    ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (p - 1))
rw [add_right_inj]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 : ℕ), x ∈ range p → a ^ (x + (p - 1 - x)) = a ^ (p - 1)
⊢ ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (x + (p - 1 - x))) =
    ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (p - 1))
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, a ^ (x + (p - 1 - x))) =
    ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (p - 1))
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_pred_of_lt (Finset.mem_range.mp hx)
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 : ℕ), x ∈ range p → a ^ (x + (p - 1 - x)) = a ^ (p - 1)
⊢ ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (x + (p - 1 - x))) =
    ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (p - 1))
rw [Finset.sum_congr rfl this]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : x ∈ range p
⊢ a ^ (x + (p - 1 - x)) = a ^ (p - 1)
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 : ℕ), x ∈ range p → a ^ (x + (p - 1 - x)) = a ^ (p - 1)
intro x hx
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : x ∈ range p
⊢ x ≤ p - 1
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : x ∈ range p
⊢ a ^ (x + (p - 1 - x)) = a ^ (p - 1)
rw [← Nat.add_sub_assoc _ x, Nat.add_sub_cancel_left]
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : x ∈ range p
⊢ x ≤ p - 1
exact Nat.le_pred_of_lt (Finset.mem_range.mp hx)
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (p - 1)) =
    ↑(Ideal.Quotient.mk (span {s})) (∑ x in range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      ↑(Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))
simp only [add_right_inj, Finset.sum_const, Finset.card_range, nsmul_eq_mul]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 {↑p ^ 2})) (∑ x in range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1)) =
    ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, ↑p * b * a ^ (p - 2) * ↑x) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1))
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in 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 in range p, a ^ (p - 2) * ↑x) +
      ↑(Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))
simp only [Finset.mul_sum, ← mul_assoc, ← pow_add]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 : ℕ), x ∈ range p → a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x = ↑p * b * a ^ (p - 2) * ↑x
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 {↑p ^ 2})) (∑ x in range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1)) =
    ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ x in range p, ↑p * b * a ^ (p - 2) * ↑x) +
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1))
rw [Finset.sum_congr rfl]
case zero
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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
hx : Nat.zero ∈ range p
⊢ a ^ (Nat.zero - 1 + (p - 1 - Nat.zero)) * ↑p * b * ↑Nat.zero = ↑p * b * a ^ (p - 2) * ↑Nat.zero

case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : Nat.succ x ∈ range p
⊢ a ^ (Nat.succ x - 1 + (p - 1 - Nat.succ x)) * ↑p * b * ↑(Nat.succ x) = ↑p * b * a ^ (p - 2) * ↑(Nat.succ x)
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 : ℕ), x ∈ range p → a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x = ↑p * b * a ^ (p - 2) * ↑x
rintro (⟨⟩ | ⟨x⟩) hx
no goals
case zero
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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
hx : Nat.zero ∈ range p
⊢ a ^ (Nat.zero - 1 + (p - 1 - Nat.zero)) * ↑p * b * ↑Nat.zero = ↑p * b * a ^ (p - 2) * ↑Nat.zero
rw [Nat.cast_zero, MulZeroClass.mul_zero, MulZeroClass.mul_zero]
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : Nat.succ x ∈ range p
this : Nat.succ x - 1 + (p - 1 - Nat.succ x) = p - 2
⊢ a ^ (Nat.succ x - 1 + (p - 1 - Nat.succ x)) * ↑p * b * ↑(Nat.succ x) = ↑p * b * a ^ (p - 2) * ↑(Nat.succ x)
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : Nat.succ x ∈ range p
⊢ a ^ (Nat.succ x - 1 + (p - 1 - Nat.succ x)) * ↑p * b * ↑(Nat.succ x) = ↑p * b * a ^ (p - 2) * ↑(Nat.succ x)
have : x.succ - 1 + (p - 1 - x.succ) = p - 2 := by
  rw [← Nat.add_sub_assoc (Nat.le_pred_of_lt (Finset.mem_range.mp hx))]
  exact congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : Nat.succ x ∈ range p
this : Nat.succ x - 1 + (p - 1 - Nat.succ x) = p - 2
⊢ a ^ (p - 2) * ↑p * b * ↑(Nat.succ x) = ↑p * b * a ^ (p - 2) * ↑(Nat.succ x)
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : Nat.succ x ∈ range p
this : Nat.succ x - 1 + (p - 1 - Nat.succ x) = p - 2
⊢ a ^ (Nat.succ x - 1 + (p - 1 - Nat.succ x)) * ↑p * b * ↑(Nat.succ x) = ↑p * b * a ^ (p - 2) * ↑(Nat.succ x)
rw [this]
no goals
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : Nat.succ x ∈ range p
this : Nat.succ x - 1 + (p - 1 - Nat.succ x) = p - 2
⊢ a ^ (p - 2) * ↑p * b * ↑(Nat.succ x) = ↑p * b * a ^ (p - 2) * ↑(Nat.succ x)
ring1
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : Nat.succ x ∈ range p
⊢ Nat.succ x - 1 + (p - 1) - Nat.succ x = p - 2
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : Nat.succ x ∈ range p
⊢ Nat.succ x - 1 + (p - 1 - Nat.succ x) = p - 2
rw [← Nat.add_sub_assoc (Nat.le_pred_of_lt (Finset.mem_range.mp hx))]
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y : 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 : ℕ
hx : Nat.succ x ∈ range p
⊢ Nat.succ x - 1 + (p - 1) - Nat.succ x = p - 2
exact congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {s})) (↑p * b * ∑ x in range p, a ^ (p - 2) * ↑x) +
      ↑(Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    ↑(Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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})) (↑p * b * ∑ x in range p, a ^ (p - 2) * ↑x) +
      ↑(Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    ↑(Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))
have : Finset.sum (range p) (fun (x : ℕ) ↦ (x : R)) =
    ((Finset.sum (range p) (fun (x : ℕ)  ↦ (x : ℕ)))) := by simp only [Nat.cast_sum]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * b * (a ^ (p - 2) * ↑(∑ x in range p, x))) = 0
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {s})) (↑p * b * ∑ x in range p, a ^ (p - 2) * ↑x) +
      ↑(Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    ↑(Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))
simp only [add_left_eq_self, ← Finset.mul_sum, this]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * b * (a ^ (p - 2) * ↑(∑ x in range p, x))) = 0
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * b * (a ^ (p - 2) * ↑(∑ x in range p, x))) = 0
norm_cast
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * b * (a ^ (p - 2) * ↑(p * (p - 1) / 2))) = 0
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * b * (a ^ (p - 2) * ↑(∑ x in range p, x))) = 0
simp only [Finset.sum_range_id]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * b * (a ^ (p - 2) * ↑(p * (p - 1) / 2))) = 0
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * b * (a ^ (p - 2) * ↑(p * (p - 1) / 2))) = 0
norm_cast
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p * ↑(Ideal.Quotient.mk (span {↑p ^ 2})) b *
      (↑(Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (p - 2)) *
        (↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p * ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑((p - 1) / 2))) =
    0
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * b * (a ^ (p - 2) * ↑(p * (p - 1) / 2))) = 0
simp only [Nat.cast_mul, _root_.map_mul,
    Nat.mul_div_assoc p (even_iff_two_dvd.mp (Nat.Odd.sub_odd hp odd_one))]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p ^ 2 * ↑(Ideal.Quotient.mk (span {↑p ^ 2})) b *
        ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (p - 2)) *
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑((p - 1) / 2) =
    0
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p * ↑(Ideal.Quotient.mk (span {↑p ^ 2})) b *
      (↑(Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (p - 2)) *
        (↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p * ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑((p - 1) / 2))) =
    0
ring
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p ^ 2 *
      (↑(Ideal.Quotient.mk (span {↑p ^ 2})) b *
        (↑(Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (p - 2)) * ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑((p - 1) / 2))) =
    0
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p ^ 2 * ↑(Ideal.Quotient.mk (span {↑p ^ 2})) b *
        ↑(Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (p - 2)) *
      ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑((p - 1) / 2) =
    0
rw [mul_assoc, mul_assoc]
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p ^ 2 = 0
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p ^ 2 *
      (↑(Ideal.Quotient.mk (span {↑p ^ 2})) b *
        (↑(Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (p - 2)) * ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑((p - 1) / 2))) =
    0
refine' mul_eq_zero_of_left _ _
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ (fun x => x ^ 2) ↑p ∈ span {↑p ^ 2}
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ ↑(Ideal.Quotient.mk (span {↑p ^ 2})) ↑p ^ 2 = 0
refine' Ideal.Quotient.eq_zero_iff_mem.mpr _
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
⊢ (fun x => x ^ 2) ↑p ∈ span {↑p ^ 2}
simp [mem_span_singleton]
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x y : 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 in range p, ↑x = ↑(∑ x in range p, x)
simp only [Nat.cast_sum]