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

Tactic:
mul_eq_zero_of_left ?_ _

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

Tactic:
refine mul_eq_zero_of_left ?_ _

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

Tactic:
Ideal.Quotient.eq_zero_iff_mem.mpr ?_

Premises used: Iff.mpr, Submodule.Quotient.mk, Ideal.Quotient.eq_zero_iff_mem, Quot.map, Quotient.map'
-- 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)
refine : Membership.mem (γ := Ideal R) (span {s}) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) (↑p : R))
⊢ HPow.hPow (α := HasQuotient.Quotient R (B := Ideal R) (span {s})) (β := ℕ)
      ((Ideal.Quotient.mk (span {s}) : (a : R) → R ⧸ span {s}) (↑p : R)) 2 =
    0

Tactic:
refine Ideal.Quotient.eq_zero_iff_mem.mpr ?_

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem
-- 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)
⊢ Membership.mem (γ := Ideal R) (span {s}) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) (↑p : R))

Tactic:
simp [s]
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R
hp : Prime p
x y : R
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : ¬p ∣ (↑n : R)
rw : emultiplicity p ((∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = emultiplicity p (x - y)
rw₁ : emultiplicity p (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) + emultiplicity p (x - y) = emultiplicity p (x - y)
rw₂ : 0 + emultiplicity p (x - y) = emultiplicity p (x - y)
rw₃ rw₄ : emultiplicity p (x - y) = emultiplicity p (x - y)
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y)

Tactic:
rw [← geom_sum₂_mul, emultiplicity_mul hp,
    emultiplicity_eq_zero.2 (not_dvd_geom_sum₂ hp hxy hx hn), zero_add]

Premises used: Iff.mpr, emultiplicity_eq_zero, zero_add, not_dvd_geom_sum₂, geom_sum₂_mul, emultiplicity_mul
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
rw : emultiplicity.{u_1} (α := R) (↑p : R) (∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i)) = 1
⊢ emultiplicity.{u_1} (α := R) (↑p : R) (∑ i ∈ range p, x ^ i * y ^ (p - 1 - i)) = 1

Tactic:
rw [← Nat.cast_one]

Premises used: Nat.cast_one
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
⊢ emultiplicity.{u_1} (α := R) (↑p : R) (∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i)) = 1

Tactic:
emultiplicity_eq_coe.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, WithTop.some, And.intro, emultiplicity_eq_coe
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
refine_1 : HPow.hPow (α := R) (β := ℕ) (↑p : R) 1 ∣ ∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i)
refine_2 : ¬HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 1 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i)
⊢ emultiplicity.{u_1} (α := R) (↑p : R) (∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i)) = 1

Tactic:
refine emultiplicity_eq_coe.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, emultiplicity_eq_coe
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
refine_1 : Dvd.dvd.{u_1} (α := R) (↑p : R) (∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i))
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 1 ∣ ∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i)

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
⊢ Dvd.dvd.{u_1} (α := R) (↑p : R) (∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i))

Tactic:
dvd_geom_sum₂_self hxy

Premises used: dvd_geom_sum₂_self
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
⊢ Dvd.dvd.{u_1} (α := R) (↑p : R) (∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i))

Tactic:
exact dvd_geom_sum₂_self hxy

Premises used: dvd_geom_sum₂_self
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
⊢ ¬(↑p : R) ∣ y

Tactic:
rw [dvd_iff_dvd_of_dvd_sub hxy] at hx

Premises used: dvd_iff_dvd_of_dvd_sub
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ y
refine_2 :
  ∀ (k : R) (hk : x - y = (↑p : R) * k),
    ¬HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 1 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i)
⊢ ¬HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 1 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i)

Tactic:
obtain ⟨k, hk⟩ := hxy
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hx : ¬(↑p : R) ∣ y
k : R
hk : x - y = (↑p : R) * k
refine_2 : ¬HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ ∑ i ∈ range p, (y + (↑p : R) * k) ^ i * y ^ (p - (↑1 : ℕ) - i)
⊢ ¬HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 1 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - (↑1 : ℕ) - i)

Tactic:
rw [one_add_one_eq_two, eq_add_of_sub_eq' hk]

Premises used: eq_add_of_sub_eq', one_add_one_eq_two
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hx : ¬(↑p : R) ∣ y
k : R
hk : x - y = (↑p : R) * k
⊢ ¬HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ ∑ i ∈ range p, (y + (↑p : R) * k) ^ i * y ^ (p - (↑1 : ℕ) - i)

Tactic:
mt (dvd_iff_dvd_of_dvd_sub (@odd_sq_dvd_geom_sum₂_sub _ _ y k _ hp1)).mp ?_

Premises used: mt, odd_sq_dvd_geom_sum₂_sub, dvd_iff_dvd_of_dvd_sub, Iff.mp
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hx : ¬(↑p : R) ∣ y
k : R
hk : x - y = (↑p : R) * k
refine_2 : ¬HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ (↑p : R) * y ^ (p - 1)
⊢ ¬HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ ∑ i ∈ range p, (y + (↑p : R) * k) ^ i * y ^ (p - (↑1 : ℕ) - i)

Tactic:
refine mt (dvd_iff_dvd_of_dvd_sub (@odd_sq_dvd_geom_sum₂_sub _ _ y k _ hp1)).mp ?_

Premises used: mt, odd_sq_dvd_geom_sum₂_sub, dvd_iff_dvd_of_dvd_sub, Iff.mp
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hx : ¬(↑p : R) ∣ y
k : R
hk : x - y = (↑p : R) * k
refine_2 : ¬(↑p : R) ∣ y ^ (p - 1)
⊢ ¬HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ (↑p : R) * y ^ (p - 1)

Tactic:
rw [pow_two, mul_dvd_mul_iff_left hp.ne_zero]

Premises used: pow_two, mul_dvd_mul_iff_left, Prime.ne_zero
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hx : ¬(↑p : R) ∣ y
k : R
hk : x - y = (↑p : R) * k
⊢ ¬(↑p : R) ∣ y ^ (p - 1)

Tactic:
mt hp.dvd_of_dvd_pow hx

Premises used: mt, Prime.dvd_of_dvd_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hx : ¬(↑p : R) ∣ y
k : R
hk : x - y = (↑p : R) * k
⊢ ¬(↑p : R) ∣ y ^ (p - 1)

Tactic:
exact mt hp.dvd_of_dvd_pow hx

Premises used: mt, Prime.dvd_of_dvd_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
rw : emultiplicity (↑p : R) ((∑ i ∈ range p, x ^ i * y ^ (p - 1 - i)) * (x - y)) = emultiplicity (↑p : R) (x - y) + 1
rw₁ :
  emultiplicity.{u_1} (α := R) (↑p : R) (∑ i ∈ range p, x ^ i * y ^ (p - 1 - i)) + emultiplicity (↑p : R) (x - y) =
    emultiplicity (↑p : R) (x - y) + 1
rw₂ : 1 + emultiplicity (↑p : R) (x - y) = emultiplicity (↑p : R) (x - y) + 1
rw₃ rw₄ : emultiplicity (↑p : R) (x - y) + 1 = emultiplicity (↑p : R) (x - y) + 1
⊢ emultiplicity (↑p : R) (x ^ p - y ^ p) = emultiplicity (↑p : R) (x - y) + 1

Tactic:
rw [← geom_sum₂_mul, emultiplicity_mul hp, emultiplicity_geom_sum₂_eq_one hp hp1 hxy hx, add_comm]

Premises used: add_comm, emultiplicity_geom_sum₂_eq_one, geom_sum₂_mul, emultiplicity_mul
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
zero :
  emultiplicity (↑p : R) (x ^ HPow.hPow (β := ℕ) p 0 - y ^ HPow.hPow (β := ℕ) p 0) = emultiplicity (↑p : R) (x - y) + 0
zero₁ :
  emultiplicity (↑p : R) (x ^ HPow.hPow (β := ℕ) p 0 - y ^ HPow.hPow (β := ℕ) p 0) = emultiplicity (↑p : R) (x - y)
zero₂ : emultiplicity (↑p : R) (HPow.hPow (β := ℕ) x 1 - HPow.hPow (β := ℕ) y 1) = emultiplicity (↑p : R) (x - y)
zero₃ : emultiplicity (↑p : R) (x - HPow.hPow (β := ℕ) y 1) = emultiplicity (↑p : R) (x - y)
zero₄ zero₅ : emultiplicity (↑p : R) (x - y) = emultiplicity (↑p : R) (x - y)
⊢ emultiplicity (↑p : R) (x ^ HPow.hPow (β := ℕ) p 0 - y ^ HPow.hPow (β := ℕ) p 0) =
    emultiplicity (↑p : R) (x - y) + (↑0 : ℕ∞)

Tactic:
rw [Nat.cast_zero, add_zero, pow_zero, pow_one, pow_one]

Premises used: pow_zero, pow_one, Nat.cast_zero, add_zero
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
a : ℕ
h_ind : emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p : R) (x - y) + (↑a : ℕ∞)
succ : emultiplicity (↑p : R) ((x ^ p ^ a) ^ p - (y ^ p ^ a) ^ p) = emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) + 1
⊢ emultiplicity (↑p : R) (x ^ p ^ (a + 1) - y ^ p ^ (a + 1)) = emultiplicity (↑p : R) (x - y) + (↑(a + 1) : ℕ∞)

Tactic:
rw [Nat.cast_add, Nat.cast_one, ← add_assoc, ← h_ind, pow_succ, pow_mul, pow_mul]

Premises used: pow_succ, add_assoc, pow_mul, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
a : ℕ
h_ind : emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p : R) (x - y) + (↑a : ℕ∞)
succ : (↑p : R) ∣ x ^ p ^ a - y ^ p ^ a
succ₁ : ¬(↑p : R) ∣ x ^ p ^ a
⊢ emultiplicity (↑p : R) ((x ^ p ^ a) ^ p - (y ^ p ^ a) ^ p) = emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) + 1

Tactic:
apply emultiplicity_pow_prime_sub_pow_prime hp hp1

Premises used: emultiplicity_pow_prime_sub_pow_prime
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
a : ℕ
h_ind : emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p : R) (x - y) + (↑a : ℕ∞)
succ : (↑p : R) ∣ (∑ i ∈ range (p ^ a), x ^ i * y ^ (p ^ a - 1 - i)) * (x - y)
⊢ (↑p : R) ∣ x ^ p ^ a - y ^ p ^ a

Tactic:
rw [← geom_sum₂_mul]

Premises used: geom_sum₂_mul
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
a : ℕ
h_ind : emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p : R) (x - y) + (↑a : ℕ∞)
⊢ (↑p : R) ∣ (∑ i ∈ range (p ^ a), x ^ i * y ^ (p ^ a - 1 - i)) * (x - y)

Tactic:
dvd_mul_of_dvd_right hxy _

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
a : ℕ
h_ind : emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p : R) (x - y) + (↑a : ℕ∞)
⊢ (↑p : R) ∣ (∑ i ∈ range (p ^ a), x ^ i * y ^ (p ^ a - 1 - i)) * (x - y)

Tactic:
exact dvd_mul_of_dvd_right hxy _

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
a : ℕ
h_ind : emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p : R) (x - y) + (↑a : ℕ∞)
⊢ ¬(↑p : R) ∣ x ^ p ^ a

Tactic:
fun h => hx (hp.dvd_of_dvd_pow h)

Premises used: Prime.dvd_of_dvd_pow, Not
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
a : ℕ
h_ind : emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p : R) (x - y) + (↑a : ℕ∞)
⊢ ¬(↑p : R) ∣ x ^ p ^ a

Tactic:
exact fun h => hx (hp.dvd_of_dvd_pow h)

Premises used: Prime.dvd_of_dvd_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
inst_1 : IsDomain R
hp : Prime.{u_1} (M := R) (↑p : R)
hp1 : Odd p
hxy : (↑p : R) ∣ x - y
hx : ¬(↑p : R) ∣ x
a : ℕ
zero :
  emultiplicity (↑p : R) (x ^ HPow.hPow (β := ℕ) p 0 - y ^ HPow.hPow (β := ℕ) p 0) =
    emultiplicity (↑p : R) (x - y) + (↑0 : ℕ∞)
succ :
  ∀ (a : ℕ) (h_ind : emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p : R) (x - y) + (↑a : ℕ∞)),
    emultiplicity (↑p : R) (x ^ p ^ (a + 1) - y ^ p ^ (a + 1)) = emultiplicity (↑p : R) (x - y) + (↑(a + 1) : ℕ∞)
⊢ emultiplicity (↑p : R) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p : R) (x - y) + (↑a : ℕ∞)

Tactic:
induction a with
  | zero => rw [Nat.cast_zero, add_zero, pow_zero, pow_one, pow_one]
  | succ a h_ind =>
    rw [Nat.cast_add, Nat.cast_one, ← add_assoc, ← h_ind, pow_succ, pow_mul, pow_mul]
    apply emultiplicity_pow_prime_sub_pow_prime hp hp1
    · rw [← geom_sum₂_mul]
      exact dvd_mul_of_dvd_right hxy _
    · exact fun h => hx (hp.dvd_of_dvd_pow h)

Premises used: dvd_mul_of_dvd_right, pow_succ, add_assoc, pow_mul, pow_zero, Nat.cast_add, pow_one, geom_sum₂_mul, emultiplicity_pow_prime_sub_pow_prime, Nat.cast_zero, Prime.dvd_of_dvd_pow, add_zero, Nat.cast_one
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
zero :
  emultiplicity (↑p : ℤ) (HPow.hPow (β := ℕ) x 0 - HPow.hPow (β := ℕ) y 0) =
    emultiplicity (↑p : ℤ) (x - y) + emultiplicity p 0
succ :
  ∀ (n : ℕ),
    emultiplicity (↑p : ℤ) (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)
⊢ emultiplicity (↑p : ℤ) (x ^ n - y ^ n) = emultiplicity (↑p : ℤ) (x - y) + emultiplicity p n

Tactic:
rcases n with - | n
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
⊢ emultiplicity (↑p : ℤ) (HPow.hPow (β := ℕ) x 0 - HPow.hPow (β := ℕ) y 0) =
    emultiplicity (↑p : ℤ) (x - y) + emultiplicity p 0

Tactic:
simp only [emultiplicity_zero, add_top, pow_zero, sub_self]

Premises used: add_top, sub_self, emultiplicity_zero, pow_zero
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
⊢ FiniteMultiplicity p n.succ

Tactic:
have h : FiniteMultiplicity _ _ := Nat.finiteMultiplicity_iff.mpr ⟨hp.ne_one, n.succ_pos⟩
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
succ :
  ∀ (hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1) (k : ℕ) (hk : n + 1 = p ^ multiplicity p (n + 1) * k),
    emultiplicity (↑p : ℤ) (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)
⊢ emultiplicity (↑p : ℤ) (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)

Tactic:
rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Iff.mp, emultiplicity_eq_coe
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
rw : emultiplicity (↑p : ℤ) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k)
| emultiplicity (↑p : ℤ) (x ^ (n + 1) - y ^ (n + 1))

Tactic:
rw [hk, pow_mul, pow_mul]

Premises used: pow_mul
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
succ :
  emultiplicity (↑p : ℤ) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)
⊢ emultiplicity (↑p : ℤ) (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)

Tactic:
conv_lhs => rw [hk, pow_mul, pow_mul]

Premises used: pow_mul