awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
n : ℕ
inst : CommRing R
x y p : R
h :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {p}))
    ((Ideal.Quotient.mk (span {p}) : (a : R) → R ⧸ span {p}) x : HasQuotient.Quotient R (B := Ideal R) (span {p}))
    ((Ideal.Quotient.mk (span {p}) : (a : R) → R ⧸ span {p}) y : HasQuotient.Quotient R (B := Ideal R) (span {p}))
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ (↑n : R) * y ^ (n - 1)

Tactic:
simp only [← mem_span_singleton, ← eq_zero_iff_mem, RingHom.map_geom_sum₂, h, geom_sum₂_self,
    map_mul, map_pow, map_natCast]

Premises used: geom_sum₂_self, map_pow, Ideal.Quotient.eq_zero_iff_mem, map_mul, map_natCast, RingHom.map_geom_sum₂, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
n : ℕ
inst : CommRing R
x y p : R
h : p ∣ x - y
rw : p ∣ y - x
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ (↑n : R) * x ^ (n - 1)

Tactic:
rw [geom_sum₂_comm, dvd_geom_sum₂_iff_of_dvd_sub]

Premises used: dvd_geom_sum₂_iff_of_dvd_sub, geom_sum₂_comm
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
n : ℕ
inst : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ y - x

Tactic:
simpa using h.neg_right

Premises used: Dvd.dvd.neg_right
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
n : ℕ
inst : CommRing R
x y : R
h : (↑n : R) ∣ x - y
⊢ Dvd.dvd.{u_1} (α := R) (↑n : R) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i))

Tactic:
(dvd_geom_sum₂_iff_of_dvd_sub h).mpr (dvd_mul_right _ _)

Premises used: Iff.mpr, dvd_geom_sum₂_iff_of_dvd_sub, dvd_mul_right
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
zero :
  HPow.hPow (β := ℕ) p 2 ∣
    HPow.hPow (β := ℕ) (x + p) 0 - x ^ HSub.hSub (α := ℕ) 0 1 * p * (↑0 : R) - HPow.hPow (β := ℕ) x 0
succ : ∀ (n : ℕ), HPow.hPow (β := ℕ) p 2 ∣ (x + p) ^ (n + 1) - x ^ (n + 1 - 1) * p * (↑(n + 1) : R) - x ^ (n + 1)
⊢ HPow.hPow (β := ℕ) p 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * (↑n : R) - x ^ n

Tactic:
rcases n with - | n
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
⊢ HPow.hPow (β := ℕ) p 2 ∣
    HPow.hPow (β := ℕ) (x + p) 0 - x ^ HSub.hSub (α := ℕ) 0 1 * p * (↑0 : R) - HPow.hPow (β := ℕ) x 0

Tactic:
simp only [pow_zero, Nat.cast_zero, sub_zero, sub_self, dvd_zero, mul_zero]

Premises used: dvd_zero, sub_self, sub_zero, pow_zero, MulZeroClass.mul_zero, Nat.cast_zero
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
succ :
  HPow.hPow (β := ℕ) p 2 ∣
    ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * (↑((n + 1).choose m) : R) + x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 +
          x ^ (n + 1) -
        x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 -
      x ^ (n + 1)
⊢ HPow.hPow (β := ℕ) p 2 ∣ (x + p) ^ (n + 1) - x ^ (n + 1 - 1) * p * (↑(n + 1) : R) - x ^ (n + 1)

Tactic:
simp only [add_pow, sum_range_succ, add_tsub_cancel_left, pow_one, Nat.choose_succ_self_right,
      Nat.cast_succ, tsub_self, pow_zero, mul_one, Nat.choose_self, Nat.cast_zero, zero_add,
      Nat.succ_sub_succ_eq_sub, Nat.sub_zero]

Premises used: Nat.cast_succ, tsub_self, Nat.choose_succ_self_right, add_tsub_cancel_left, zero_add, pow_zero, pow_one, add_pow, Nat.sub_zero, Nat.cast_zero, mul_one, Nat.succ_sub_succ_eq_sub, Finset.sum_range_succ, Nat.choose_self
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
this : HPow.hPow (β := ℕ) p 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)
⊢ HPow.hPow (β := ℕ) p 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)

Tactic:
this
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
this : HPow.hPow (β := ℕ) p 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)
h :
  ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * (↑((n + 1).choose m) : R) + x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 +
          x ^ (n + 1) -
        x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 -
      x ^ (n + 1) =
    ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)
⊢ HPow.hPow (β := ℕ) p 2 ∣
    ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * (↑((n + 1).choose m) : R) + x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 +
          x ^ (n + 1) -
        x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 -
      x ^ (n + 1)

Tactic:
convert! this
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
this : HPow.hPow (β := ℕ) p 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)
⊢ ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * (↑((n + 1).choose m) : R) + x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 +
          x ^ (n + 1) -
        x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 -
      x ^ (n + 1) =
    ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)

Tactic:
abel
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
succ : HPow.hPow (β := ℕ) p 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)
⊢ HPow.hPow (β := ℕ) p 2 ∣
    ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * (↑((n + 1).choose m) : R) + x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 +
          x ^ (n + 1) -
        x ^ n * p * HAdd.hAdd (α := R) (↑n : R) 1 -
      x ^ (n + 1)

Tactic:
suffices p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i) by
      convert! this; abel
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
succ : ∀ i ∈ range n, HPow.hPow (β := ℕ) p 2 ∣ x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)
⊢ HPow.hPow (β := ℕ) p 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)

Tactic:
apply Finset.dvd_sum

Premises used: Finset.dvd_sum
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n y : ℕ
hy : y ∈ range n
linarith :
  n + 1 < y + 2 →
    -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑y : ℤ) 2) +
        (HAdd.hAdd (α := ℤ) (↑y : ℤ) 1 - (↑n : ℤ)) =
      0
⊢ y + 2 ≤ n + 1

Tactic:
linarith [Finset.mem_range.mp hy]

Premises used: Finset.mem_range, Iff.mp
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n y : ℕ
hy : y ∈ range n
⊢ p ^ (n + 1 - y) ∣ x ^ y * p ^ (n + 1 - y) * (↑((n + 1).choose y) : R)

Tactic:
dvd_mul_of_dvd_left (dvd_mul_left _ _) _

Premises used: dvd_mul_of_dvd_left, dvd_mul_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
p x : R
n y : ℕ
hy : y ∈ range n
⊢ HPow.hPow (β := ℕ) p 2 ∣ x ^ y * p ^ (n + 1 - y) * (↑((n + 1).choose y) : R)

Tactic:
calc
      p ^ 2 ∣ p ^ (n + 1 - y) :=
        pow_dvd_pow p (le_tsub_of_add_le_left (by linarith [Finset.mem_range.mp hy]))
      _ ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y) :=
        dvd_mul_of_dvd_left (dvd_mul_left _ _) _

Premises used: dvd_mul_of_dvd_left, Nat.choose, le_tsub_of_add_le_left, pow_dvd_pow, HSub.hSub, dvd_mul_left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
n : ℕ
inst : CommRing R
x y p : R
hp : Prime p
hxy : p ∣ x - y
hx : ¬p ∣ x
hn : ¬p ∣ (↑n : R)
⊢ ¬p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)

Tactic:
fun h =>
  hx <|
    hp.dvd_of_dvd_pow <| (hp.dvd_or_dvd <| (dvd_geom_sum₂_iff_of_dvd_sub' hxy).mp h).resolve_left hn

Premises used: Prime.dvd_or_dvd, Or.resolve_left, Iff.mp, Prime.dvd_of_dvd_pow, Not, dvd_geom_sum₂_iff_of_dvd_sub'
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
a b : R
p : ℕ
hp : Odd p
i : ℕ
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ HPow.hPow (β := ℕ) ((↑p : R) * b) 2

Tactic:
simp only [mul_pow, dvd_mul_right]

Premises used: dvd_mul_right, mul_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
a b : R
p : ℕ
hp : Odd p
i : ℕ
⊢ HPow.hPow (β := ℕ) ((↑p : R) * b) 2 ∣ (a + (↑p : R) * b) ^ i - (a ^ (i - 1) * ((↑p : R) * b) * (↑i : R) + a ^ i)

Tactic:
simp only [sq_dvd_add_pow_sub_sub (↑p * b) a i, ← sub_sub]

Premises used: HMul.hMul, sub_sub, sq_dvd_add_pow_sub_sub
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
a b : R
p : ℕ
hp : Odd p
i : ℕ
by : HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ HPow.hPow (β := ℕ) ((↑p : R) * b) 2
by₁ : HPow.hPow (β := ℕ) ((↑p : R) * b) 2 ∣ (a + (↑p : R) * b) ^ i - (a ^ (i - 1) * ((↑p : R) * b) * (↑i : R) + a ^ i)
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ (a + (↑p : R) * b) ^ i - (a ^ (i - 1) * ((↑p : R) * b) * (↑i : R) + a ^ i)

Tactic:
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]

Premises used: HMul.hMul, HSub.hSub, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
a b : R
p : ℕ
hp : Odd p
⊢ ∀ (i : ℕ),
    HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ (a + (↑p : R) * b) ^ i - (a ^ (i - 1) * ((↑p : R) * b) * (↑i : R) + a ^ i)

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]
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ (a + (↑p : R) * b) ^ i - (a ^ (i - 1) * ((↑p : R) * b) * (↑i : R) + a ^ i)
simp_rw :
  ∀
    (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}))),
    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}))
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣
    ∑ i ∈ range p, (a + (↑p : R) * b) ^ i * a ^ (p - 1 - i) - (↑p : R) * a ^ (p - 1)

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

Premises used: Ideal.Quotient.eq, Ideal.mem_span_singleton
-- 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
ring_nf :
  ∑ x ∈ range p,
      (Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        (a ^ (x - 1) * a ^ (p - 1 - x) * (↑p : R) * b * (↑x : R) + a ^ x * a ^ (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 ^ x * a ^ (p - 1 - x)))
⊢ ∑ 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))))

Tactic:
ring_nf
-- 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
simp_rw :
  (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) + a ^ x * a ^ (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 ^ x * a ^ (p - 1 - x)))
simp_rw₁ :
  (Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
      (HAdd.hAdd (α := R) (∑ x ∈ range p, a ^ (x - 1) * a ^ (p - 1 - x) * (↑p : R) * b * (↑x : R))
        (∑ x ∈ range p, a ^ x * a ^ (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 ^ x * a ^ (p - 1 - x)))
⊢ ∑ x ∈ range p,
      (Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        (a ^ (x - 1) * a ^ (p - 1 - x) * (↑p : R) * b * (↑x : R) + a ^ x * a ^ (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 ^ x * a ^ (p - 1 - x)))

Tactic:
simp_rw [← map_sum, sum_add_distrib, map_add]

Premises used: Finset.sum_add_distrib, map_add, map_sum
-- 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
rw :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ x ∈ range p, a ^ (x + (p - 1 - x))))
    ((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}))
      ((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)))

Tactic:
rw [add_right_inj]

Premises used: add_right_inj
-- 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
x : ℕ
hx : x ∈ range p
rw : x ≤ p - 1
⊢ a ^ (x + (p - 1 - x)) = a ^ (p - 1)

Tactic:
rw [← Nat.add_sub_assoc _ x, Nat.add_sub_cancel_left]

Premises used: Nat.add_sub_assoc, Nat.add_sub_cancel_left
-- 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
x : ℕ
hx : x ∈ range p
⊢ x ≤ p - 1

Tactic:
Nat.le_sub_one_of_lt (Finset.mem_range.mp hx)

Premises used: Finset.mem_range, Nat.le_sub_one_of_lt, Iff.mp
-- 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
x : ℕ
hx : x ∈ range p
⊢ x ≤ p - 1

Tactic:
exact Nat.le_sub_one_of_lt (Finset.mem_range.mp hx)

Premises used: Finset.mem_range, Nat.le_sub_one_of_lt, Iff.mp
-- 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
⊢ ∀ (x : ℕ) (hx : x ∈ range p), a ^ (x + (p - 1 - x)) = 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)
-- 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
this : ∀ (x : ℕ) (hx : x ∈ range p), a ^ (x + (p - 1 - x)) = a ^ (p - 1)
rw rw₁ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ x ∈ range p, a ^ (p - 1)))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ _x ∈ range p, a ^ (p - 1)))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ x ∈ range p, a ^ (x + (p - 1 - x))))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (∑ _x ∈ range p, a ^ (p - 1)))

Tactic:
rw [Finset.sum_congr rfl this]

Premises used: Finset.sum_congr, rfl
-- 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
⊢ 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}))

Tactic:
simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]

Premises used: Finset.card_range, nsmul_eq_mul, Finset.sum_const