case zero
R : Type ?u.833926
n : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ multiplicity (↑p) (x ^ Nat.zero - y ^ Nat.zero) = multiplicity (↑p) (x - y) + multiplicity p Nat.zero

case succ
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
⊢ multiplicity (↑p) (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
⊢ multiplicity (↑p) (x ^ n - y ^ n) = multiplicity (↑p) (x - y) + multiplicity p n
cases' n with n
case succ
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
⊢ multiplicity (↑p) (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
case succ
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
⊢ multiplicity (↑p) (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
have h : (multiplicity _ _).Dom := finite_nat_iff.mpr ⟨hp.ne_one, n.succ_pos⟩
case succ.intro.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ multiplicity (↑p) (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
case succ
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
⊢ multiplicity (↑p) (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
rcases eq_coe_iff.mp (PartENat.natCast_get h).symm with ⟨⟨k, hk⟩, hpn⟩
case succ.intro.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ multiplicity (↑p)
      ((x ^ p ^ Part.get (multiplicity p (Nat.succ n)) h) ^ k -
        (y ^ p ^ Part.get (multiplicity p (Nat.succ n)) h) ^ k) =
    multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
case succ.intro.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ multiplicity (↑p) (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
conv_lhs => rw [hk, pow_mul, pow_mul]
case succ.intro.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ multiplicity (↑p)
      ((x ^ p ^ Part.get (multiplicity p (Nat.succ n)) h) ^ k -
        (y ^ p ^ Part.get (multiplicity p (Nat.succ n)) h) ^ k) =
    multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
case succ.intro.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ multiplicity (↑p)
      ((x ^ p ^ Part.get (multiplicity p (Nat.succ n)) h) ^ k -
        (y ^ p ^ Part.get (multiplicity p (Nat.succ n)) h) ^ k) =
    multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
rw [Nat.prime_iff_prime_int] at hp
case succ.intro.intro.hxy
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ↑p ∣ x ^ p ^ Part.get (multiplicity p (Nat.succ n)) h - y ^ p ^ Part.get (multiplicity p (Nat.succ n)) h

case succ.intro.intro.hx
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ¬↑p ∣ x ^ p ^ Part.get (multiplicity p (Nat.succ n)) h

case succ.intro.intro.hn
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ¬↑p ∣ ↑k
case succ.intro.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ multiplicity (↑p)
      ((x ^ p ^ Part.get (multiplicity p (Nat.succ n)) h) ^ k -
        (y ^ p ^ Part.get (multiplicity p (Nat.succ n)) h) ^ k) =
    multiplicity (↑p) (x - y) + multiplicity p (Nat.succ n)
rw [pow_sub_pow_of_prime hp, pow_prime_pow_sub_pow_prime_pow hp hp1 hxy hx, PartENat.natCast_get]
no goals
case zero
R : Type ?u.833926
n : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ multiplicity (↑p) (x ^ Nat.zero - y ^ Nat.zero) = multiplicity (↑p) (x - y) + multiplicity p Nat.zero
simp only [multiplicity.zero, add_top, pow_zero, sub_self, Nat.zero_eq]
case succ.intro.intro.hxy
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ↑p ∣
    (∑ i in range (p ^ Part.get (multiplicity p (Nat.succ n)) h),
        x ^ i * y ^ (p ^ Part.get (multiplicity p (Nat.succ n)) h - 1 - i)) *
      (x - y)
case succ.intro.intro.hxy
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ↑p ∣ x ^ p ^ Part.get (multiplicity p (Nat.succ n)) h - y ^ p ^ Part.get (multiplicity p (Nat.succ n)) h
rw [← geom_sum₂_mul]
no goals
case succ.intro.intro.hxy
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ↑p ∣
    (∑ i in range (p ^ Part.get (multiplicity p (Nat.succ n)) h),
        x ^ i * y ^ (p ^ Part.get (multiplicity p (Nat.succ n)) h - 1 - i)) *
      (x - y)
exact dvd_mul_of_dvd_right hxy _
no goals
case succ.intro.intro.hx
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ¬↑p ∣ x ^ p ^ Part.get (multiplicity p (Nat.succ n)) h
exact fun h => hx (hp.dvd_of_dvd_pow h)
case succ.intro.intro.hn
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ¬p ∣ k
case succ.intro.intro.hn
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ¬↑p ∣ ↑k
rw [Int.coe_nat_dvd]
case succ.intro.intro.hn.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
c : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * (p * c)
⊢ False
case succ.intro.intro.hn
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * k
⊢ ¬p ∣ k
rintro ⟨c, rfl⟩
case succ.intro.intro.hn.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
c : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * (p * c)
⊢ Nat.succ n = p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) * c
case succ.intro.intro.hn.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
c : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * (p * c)
⊢ False
refine' hpn ⟨c, _⟩
no goals
case succ.intro.intro.hn.intro
R : Type ?u.833926
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : (multiplicity p (Nat.succ n)).Dom
hpn : ¬p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) ∣ Nat.succ n
c : ℕ
hk : Nat.succ n = p ^ Part.get (multiplicity p (Nat.succ n)) h * (p * c)
⊢ Nat.succ n = p ^ (Part.get (multiplicity p (Nat.succ n)) h + 1) * c
rwa [pow_succ', mul_assoc]