awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)
have inr : ∀ (ζ : Rˣ) (hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ) (hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a),
  Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)
Tactic: obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hχ h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)
have hζ₃ : (↑ζ : R) ^ n = (↑1 : R)
Tactic: rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val] at hζ₁
Cleared hypotheses: hζ₁, hζ₂
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
R : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
n : ℕ
inst_4 : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : (↑ζ : R) ^ n = (↑1 : R)
hζ₂ : (↑ζ : R) = (χ : (a : F) → R) a
⊢ Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)
have inr : ∀ k < n, ∀ (hk : μ ^ k = (↑ζ : R)), Membership.mem (α := R) (γ := Subalgebra ℤ R) ℤ[μ] ((χ : (a : F) → R) a : R)
Tactic: obtain ⟨k, _, hk⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one hμ hζ₁
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
R : Type u_1
n : ℕ
inst : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ (↑n : R) * y ^ (n - 1)
have 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}))
Tactic: rw [← mem_span_singleton, ← Ideal.Quotient.eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
n : ℕ
inst : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ (↑n : R) * x ^ (n - 1)
have rw : p ∣ y - x
Tactic: rw [geom_sum₂_comm, dvd_geom_sum₂_iff_of_dvd_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
⊢ HPow.hPow (β := ℕ) p 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * (↑n : R) - x ^ n
have zero : HPow.hPow (β := ℕ) p 2 ∣
  HPow.hPow (β := ℕ) (x + p) 0 - x ^ HSub.hSub (α := ℕ) 0 1 * p * (↑0 : R) - HPow.hPow (β := ℕ) x 0
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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
⊢ HPow.hPow (β := ℕ) p 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * (↑n : R) - x ^ n
have succ : ∀ (n : ℕ), HPow.hPow (β := ℕ) p 2 ∣ (x + p) ^ (n + 1) - x ^ (n + 1 - 1) * p * (↑(n + 1) : R) - x ^ (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
⊢ HPow.hPow (β := ℕ) p 2 ∣ (x + p) ^ (n + 1) - x ^ (n + 1 - 1) * p * (↑(n + 1) : R) - x ^ (n + 1)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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 ∣
    ∑ 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)
have 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)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
⊢ 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)
have succ : HPow.hPow (β := ℕ) p 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)
Tactic: suffices p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i) by
      convert! this; abel
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
p x : R
n : ℕ
⊢ HPow.hPow (β := ℕ) p 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)
have succ : ∀ i ∈ range n, HPow.hPow (β := ℕ) p 2 ∣ x ^ i * p ^ (n + 1 - i) * (↑((n + 1).choose i) : R)
Tactic: apply Finset.dvd_sum
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
p x : R
n y : ℕ
hy : y ∈ range n
⊢ y + 2 ≤ n + 1
have linarith : n + 1 < y + 2 →
  -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑y : ℤ) 2) +
      (HAdd.hAdd (α := ℤ) (↑y : ℤ) 1 - (↑n : ℤ)) =
    0
Tactic: linarith [Finset.mem_range.mp hy]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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)
have by : HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ HPow.hPow (β := ℕ) ((↑p : R) * b) 2
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ (a + (↑p : R) * b) ^ i - (a ^ (i - 1) * ((↑p : R) * b) * (↑i : R) + a ^ i)
have by₁ : HPow.hPow (β := ℕ) ((↑p : R) * b) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b : R
p : ℕ
hp : Odd p
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣
    ∑ i ∈ range p, (a + (↑p : R) * b) ^ i * a ^ (p - 1 - i) - (↑p : R) * a ^ (p - 1)
have h1 : ∀ (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]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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)
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣
    ∑ i ∈ range p, (a + (↑p : R) * b) ^ i * a ^ (p - 1 - i) - (↑p : R) * a ^ (p - 1)
have 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}))
Tactic: simp_rw [← mem_span_singleton, ← Ideal.Quotient.eq] at *
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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 :
  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)))
    (∑ x ∈ range p,
      (Ideal.Quotient.mk (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}) : (a : R) → R ⧸ span {(↑p : R) ^ 2})
        ((a ^ (x - 1) * ((↑p : R) * b) * (↑x : R) + a ^ x) * a ^ (p - 1 - x)))
⊢ 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)))
have simp_rw₁ : Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}))
  (∑ i ∈ range p,
    HPow.hPow (α := 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) :
          HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}))
        i *
      HPow.hPow (α := 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 :
          HasQuotient.Quotient R (B := Ideal R) (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}))
        (p - 1 - i))
  (∑ x ∈ range p,
    (Ideal.Quotient.mk (span {HPow.hPow (α := R) (β := ℕ) (↑p : R) 2}) : (a : R) → R ⧸ span {(↑p : R) ^ 2})
      ((a ^ (x - 1) * ((↑p : R) * b) * (↑x : R) + a ^ x) * a ^ (p - 1 - x)))
Tactic: simp_rw [s, RingHom.map_geom_sum₂, ← map_pow, h1, ← map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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 ∈ 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))))
have 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)))
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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 ∈ 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)))
have 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)))
Tactic: simp_rw [← map_sum, sum_add_distrib, map_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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)))
⊢ ∑ 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)))
have 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)))
Tactic: simp_rw [← map_sum, sum_add_distrib, map_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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 ^ (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)))
have 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)))
Tactic: rw [add_right_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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)
have rw : x ≤ p - 1
Tactic: rw [← Nat.add_sub_assoc _ x, Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
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 (α := 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)))
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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)
⊢ 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)))
have 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)))
Tactic: rw [Finset.sum_congr rfl this]