-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}))
      ((Ideal.Quotient.mk (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}) : (a : R) → R ⧸ span {(↑p : R) ^ 2})
          ((a + (↑p : R) * b) ^ i) :
        HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}))
      ((Ideal.Quotient.mk (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}) : (a : R) → R ⧸ span {(↑p : R) ^ 2})
          (a ^ (i - 1) * ((↑p : R) * b) * (↑i : R) + a ^ i) :
        HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}))
s : R := HPow.hPow (α := R) (β := ℕ) (↑p : R) 2
i :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ i ∈ range p, (a + (↑p : R) * b) ^ i * a ^ (p - 1 - i)))
    (∑ i ∈ range p,
      (Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        ((a ^ (i - 1) * ((↑p : R) * b) * (↑i : R) + a ^ i) * a ^ (p - 1 - i)))
i₁ :
  ∑ i ∈ range p,
      (Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        ((a ^ (i - 1) * ((↑p : R) * b) * (↑i : R) + a ^ i) * a ^ (p - 1 - i)) =
    HAdd.hAdd (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * ((↑p : R) * (b * (↑x : R))))))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ x ∈ range p, a ^ (x + (p - 1 - x))))
i₂ :
  HAdd.hAdd (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * ((↑p : R) * (b * (↑x : R))))))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ x ∈ range p, a ^ (x + (p - 1 - x)))) =
    HAdd.hAdd (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * ((↑p : R) * (b * (↑x : R))))))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ _x ∈ range p, a ^ (p - 1)))
i₃ :
  HAdd.hAdd (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * ((↑p : R) * (b * (↑x : R))))))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ _x ∈ range p, a ^ (p - 1))) =
    HAdd.hAdd (α := HasQuotient.Quotient R (B := Ideal R) (span {s})) (β :=
      HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
          (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * ((↑p : R) * (b * (↑x : R))))) :
        HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * a ^ (p - 1)) :
        HasQuotient.Quotient R (B := Ideal R) (span {s}))
i₄ :
  HAdd.hAdd (α := HasQuotient.Quotient R (B := Ideal R) (span {s})) (β :=
      HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
          (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * ((↑p : R) * (b * (↑x : R))))) :
        HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * a ^ (p - 1)) :
        HasQuotient.Quotient R (B := Ideal R) (span {s})) =
    HAdd.hAdd (α := HasQuotient.Quotient R (B := Ideal R) (span {s})) (β :=
      HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * b * ∑ x ∈ range p, a ^ (p - 2) * (↑x : R)) :
        HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * a ^ (p - 1)) :
        HasQuotient.Quotient R (B := Ideal R) (span {s}))
i₅ :
  HAdd.hAdd (α := HasQuotient.Quotient R (B := Ideal R) (span {s})) (β :=
      HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * b * ∑ x ∈ range p, a ^ (p - 2) * (↑x : R)) :
        HasQuotient.Quotient R (B := Ideal R) (span {s}))
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * a ^ (p - 1)) :
        HasQuotient.Quotient R (B := Ideal R) (span {s})) =
    (Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * a ^ (p - 1))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}))
    ((Ideal.Quotient.mk (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}) : (a : R) → R ⧸ span {(↑p : R) ^ 2})
        (∑ i ∈ range p, (a + (↑p : R) * b) ^ i * a ^ (p - 1 - i)) :
      HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}))
    ((Ideal.Quotient.mk (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}) : (a : R) → R ⧸ span {(↑p : R) ^ 2})
        ((↑p : R) * a ^ (p - 1)) :
      HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}))

Tactic:
calc
    (Ideal.Quotient.mk (span {s})) (∑ i ∈ range p, (a + (p : R) * b) ^ i * a ^ (p - 1 - i)) =
        ∑ i ∈ Finset.range p,
        mk (span {s}) ((a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) * a ^ (p - 1 - i)) := by
      simp_rw [s, RingHom.map_geom_sum₂, ← map_pow, h1, ← map_mul]
    _ =
        mk (span {s})
            (∑ x ∈ Finset.range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
          mk (span {s}) (∑ x ∈ Finset.range p, a ^ (x + (p - 1 - x))) := by
      ring_nf
      simp_rw [← map_sum, sum_add_distrib, map_add]
    _ =
        mk (span {s})
            (∑ x ∈ Finset.range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
          mk (span {s}) (∑ _x ∈ Finset.range p, a ^ (p - 1)) := by
      rw [add_right_inj]
      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)
      rw [Finset.sum_congr rfl this]
    _ =
        mk (span {s})
            (∑ x ∈ Finset.range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
          mk (span {s}) (↑p * a ^ (p - 1)) := by
      simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
    _ =
        mk (span {s}) (↑p * b * ∑ x ∈ Finset.range p, a ^ (p - 2) * x) +
          mk (span {s}) (↑p * a ^ (p - 1)) := by
      simp only [Finset.mul_sum, ← mul_assoc, ← pow_add]
      rw [Finset.sum_congr rfl]
      rintro (⟨⟩ | ⟨x⟩) hx
      · rw [Nat.cast_zero, mul_zero, mul_zero]
      · have : x.succ - 1 + (p - 1 - x.succ) = p - 2 := by
          rw [← Nat.add_sub_assoc (Nat.le_sub_one_of_lt (Finset.mem_range.mp hx))]
          exact congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)
        rw [this]
        ring1
    _ = mk (span {s}) (↑p * a ^ (p - 1)) := by
      have : Finset.sum (range p) (fun (x : ℕ) ↦ (x : R)) =
          ((Finset.sum (range p) (fun (x : ℕ) ↦ (x : ℕ)))) := by simp only [Nat.cast_sum]
      simp only [add_eq_right, ← Finset.mul_sum, this]
      norm_cast
      simp only [Finset.sum_range_id]
      norm_cast
      simp only [Nat.cast_mul, map_mul,
          Nat.mul_div_assoc p (even_iff_two_dvd.mp (Nat.Odd.sub_odd hp odd_one))]
      ring_nf
      rw [mul_assoc, mul_assoc]
      refine mul_eq_zero_of_left ?_ _
      refine Ideal.Quotient.eq_zero_iff_mem.mpr ?_
      simp [s]

Premises used: HMul.hMul, Ideal.Quotient.mk, HSub.hSub, Nat.cast, Finset.range, HPow.hPow, HAdd.hAdd, Ideal.span, Singleton.singleton, OfNat.ofNat, DFunLike.coe, Finset.sum