awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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 + (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}) (∑ x ∈ range p, (↑p : R) * b * 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}))
⊢ 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}))

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

Premises used: Finset.mul_sum, mul_assoc, pow_add
-- 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 : ∀ x ∈ range p, a ^ (x - 1 + (p - 1 - x)) * (↑p : R) * b * (↑x : R) = (↑p : R) * b * a ^ (p - 2) * (↑x : R)
⊢ 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 + (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}) (∑ x ∈ range p, (↑p : R) * b * 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}))

Tactic:
rw [Finset.sum_congr rfl]

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
hx : 0 ∈ range p
zero : a ^ (HSub.hSub (α := ℕ) 0 1 + (p - 1 - 0)) * (↑p : R) * b * 0 = (↑p : R) * b * a ^ (p - 2) * 0
zero₁ : 0 = (↑p : R) * b * a ^ (p - 2) * 0
zero₂ zero₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ a ^ (HSub.hSub (α := ℕ) 0 1 + (p - 1 - 0)) * (↑p : R) * b * (↑0 : R) = (↑p : R) * b * a ^ (p - 2) * (↑0 : R)

Tactic:
rw [Nat.cast_zero, mul_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.cast_zero
-- 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 + 1 ∈ range p
rw : x.succ - 1 + (p - 1) - (x + 1) = p - 2
⊢ x.succ - 1 + (p - 1 - x.succ) = p - 2

Tactic:
rw [← Nat.add_sub_assoc (Nat.le_sub_one_of_lt (Finset.mem_range.mp hx))]

Premises used: Nat.add_sub_assoc, 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 + 1 ∈ range p
⊢ x.succ - 1 + (p - 1) - (x + 1) = p - 2

Tactic:
congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)

Premises used: Nat.add_sub_cancel_left, congr_arg, Nat.pred
-- 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 + 1 ∈ range p
⊢ x.succ - 1 + (p - 1) - (x + 1) = p - 2

Tactic:
exact congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)

Premises used: Nat.add_sub_cancel_left, congr_arg, Nat.pred
-- 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 + 1 ∈ range p
⊢ x.succ - 1 + (p - 1 - x.succ) = p - 2

Tactic:
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 _ _)
-- 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 + 1 ∈ range p
this : x.succ - 1 + (p - 1 - x.succ) = p - 2
succ : a ^ (p - 2) * (↑p : R) * b * (↑(x + 1) : R) = (↑p : R) * b * a ^ (p - 2) * (↑(x + 1) : R)
⊢ a ^ (x + 1 - 1 + (p - 1 - (x + 1))) * (↑p : R) * b * (↑(x + 1) : R) = (↑p : R) * b * a ^ (p - 2) * (↑(x + 1) : R)

Tactic:
rw [this]
-- 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 + 1 ∈ range p
this : x.succ - 1 + (p - 1 - x.succ) = p - 2
⊢ a ^ (p - 2) * (↑p : R) * b * (↑(x + 1) : R) = (↑p : R) * b * a ^ (p - 2) * (↑(x + 1) : R)

Tactic:
ring1
-- 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
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ range p, (↑x : R)) (↑(∑ x ∈ range p, x) : R)

Tactic:
simp only [Nat.cast_sum]

Premises used: Nat.cast_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
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ range p, (↑x : R)) (↑(∑ x ∈ range p, x) : R)

Tactic:
have : Finset.sum (range p) (fun (x : ℕ) ↦ (x : R)) =
          ((Finset.sum (range p) (fun (x : ℕ) ↦ (x : ℕ)))) := by simp only [Nat.cast_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
this : Eq.{u_1 + 1} (α := R) (∑ x ∈ range p, (↑x : R)) (↑(∑ x ∈ range p, x) : R)
simp :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        ((↑p : R) * b * (a ^ (p - 2) * (↑(∑ x ∈ range p, x) : R))) :
      HasQuotient.Quotient R (B := Ideal R) (span {s}))
    (0 : 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})) =
    (Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * a ^ (p - 1))

Tactic:
simp only [add_eq_right, ← Finset.mul_sum, this]

Premises used: Finset.mul_sum, add_eq_right
-- 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 : Eq.{u_1 + 1} (α := R) (∑ x ∈ range p, (↑x : R)) (↑(∑ x ∈ range p, x) : R)
simp :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * b * (a ^ (p - 2) * (↑(p * (p - 1) / 2) : R))) :
      HasQuotient.Quotient R (B := Ideal R) (span {s}))
    (0 : HasQuotient.Quotient R (B := Ideal R) (span {s}))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s})
        ((↑p : R) * b * (a ^ (p - 2) * (↑(∑ x ∈ range p, x) : R))) :
      HasQuotient.Quotient R (B := Ideal R) (span {s}))
    (0 : HasQuotient.Quotient R (B := Ideal R) (span {s}))

Tactic:
simp only [Finset.sum_range_id]

Premises used: Finset.sum_range_id
-- 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 : Eq.{u_1 + 1} (α := R) (∑ x ∈ range p, (↑x : R)) (↑(∑ x ∈ range p, x) : R)
simp :
  HMul.hMul (α := 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) :
          HasQuotient.Quotient R (B := Ideal R) (span {s}))
        ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) b : HasQuotient.Quotient R (B := Ideal R) (span {s})) *
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
        ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (a ^ (p - 2)) :
          HasQuotient.Quotient R (B := Ideal R) (span {s}))
        (HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
          ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑p : R))
          ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑((p - 1) / 2) : R))) =
    0
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
    ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) ((↑p : R) * b * (a ^ (p - 2) * (↑(p * (p - 1) / 2) : R))) :
      HasQuotient.Quotient R (B := Ideal R) (span {s}))
    (0 : HasQuotient.Quotient R (B := Ideal R) (span {s}))

Tactic:
simp only [Nat.cast_mul, map_mul,
          Nat.mul_div_assoc p (even_iff_two_dvd.mp (Nat.Odd.sub_odd hp odd_one))]

Premises used: map_mul, Nat.cast_mul, odd_one, Nat.Odd.sub_odd, Iff.mp, even_iff_two_dvd, Nat.mul_div_assoc
-- 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 : Eq.{u_1 + 1} (α := R) (∑ x ∈ range p, (↑x : R)) (↑(∑ x ∈ range p, x) : R)
ring_nf :
  HMul.hMul (β := HasQuotient.Quotient R (B := Ideal R) (span {s}))
        (HMul.hMul (β := HasQuotient.Quotient R (B := Ideal R) (span {s}))
          (HPow.hPow (α := HasQuotient.Quotient R (B := Ideal R) (span {s})) (β := ℕ)
            ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑p : R)) 2)
          ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) b :
            HasQuotient.Quotient R (B := Ideal R) (span {s})))
        ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (a ^ (p - 2)) :
          HasQuotient.Quotient R (B := Ideal R) (span {s})) *
      (Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑((p - 1) / 2) : R) =
    0
⊢ HMul.hMul (α := 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) :
          HasQuotient.Quotient R (B := Ideal R) (span {s}))
        ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) b : HasQuotient.Quotient R (B := Ideal R) (span {s})) *
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
        ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (a ^ (p - 2)) :
          HasQuotient.Quotient R (B := Ideal R) (span {s}))
        (HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
          ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑p : R))
          ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑((p - 1) / 2) : R))) =
    0

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
this : Eq.{u_1 + 1} (α := R) (∑ x ∈ range p, (↑x : R)) (↑(∑ x ∈ range p, x) : R)
rw :
  HPow.hPow (α := HasQuotient.Quotient R (B := Ideal R) (span {s})) (β := ℕ)
        ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑p : R)) 2 *
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (span {s}))
        ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) b : HasQuotient.Quotient R (B := Ideal R) (span {s}))
        (HMul.hMul (α := 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}) (a ^ (p - 2)) :
            HasQuotient.Quotient R (B := Ideal R) (span {s}))
          ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑((p - 1) / 2) : R) :
            HasQuotient.Quotient R (B := Ideal R) (span {s}))) =
    0
⊢ HMul.hMul (β := HasQuotient.Quotient R (B := Ideal R) (span {s}))
        (HMul.hMul (β := HasQuotient.Quotient R (B := Ideal R) (span {s}))
          (HPow.hPow (α := HasQuotient.Quotient R (B := Ideal R) (span {s})) (β := ℕ)
            ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑p : R)) 2)
          ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) b :
            HasQuotient.Quotient R (B := Ideal R) (span {s})))
        ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (a ^ (p - 2)) :
          HasQuotient.Quotient R (B := Ideal R) (span {s})) *
      (Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑((p - 1) / 2) : R) =
    0

Tactic:
rw [mul_assoc, mul_assoc]

Premises used: mul_assoc