case inl
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a b : α
n : ℕ
hp : Prime p
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * b ^ n
hb : ¬p ^ 2 ∣ b
H : p ∣ a ^ Nat.succ n
⊢ p ∣ a

case inr
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a b : α
n : ℕ
hp : Prime p
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * b ^ n
hb : ¬p ^ 2 ∣ b
hbdiv : p ∣ b ^ n
⊢ p ∣ a
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a b : α
n : ℕ
hp : Prime p
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * b ^ n
hb : ¬p ^ 2 ∣ b
⊢ p ∣ a
cases' hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H hbdiv
case inr.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * (p * x) ^ n
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
⊢ p ∣ a
case inr
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a b : α
n : ℕ
hp : Prime p
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * b ^ n
hb : ¬p ^ 2 ∣ b
hbdiv : p ∣ b ^ n
⊢ p ∣ a
obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv
case inr.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
⊢ p ∣ a
case inr.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * (p * x) ^ n
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
⊢ p ∣ a
obtain ⟨y, hy⟩ := hpow
case inr.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * x ^ n = p * y
⊢ p ∣ a
case inr.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
⊢ p ∣ a
have : a ^ n.succ * x ^ n = p * y := by
  refine' mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) _
  rw [← mul_assoc _ p, ← pow_succ', ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
    mul_assoc]
case inr.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * x ^ n = p * y
hdvdx : p ∣ x ^ n
⊢ p ^ 2 ∣ p * x
case inr.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * x ^ n = p * y
⊢ p ∣ a
refine' hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right fun hdvdx => hb _)
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
y z : α
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ Nat.succ n * (p * (p * z)) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p ^ 2 ∣ p * (p * z)
case inr.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * x ^ n = p * y
hdvdx : p ∣ x ^ n
⊢ p ^ 2 ∣ p * x
obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
y z : α
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ Nat.succ n * (p * (p * z)) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p * p ∣ p * p * z
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
y z : α
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ Nat.succ n * (p * (p * z)) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p ^ 2 ∣ p * (p * z)
rw [pow_two, ← mul_assoc]
no goals
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
y z : α
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ Nat.succ n * (p * (p * z)) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p * p ∣ p * p * z
exact dvd_mul_right _ _
no goals
case inl
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a b : α
n : ℕ
hp : Prime p
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * b ^ n
hb : ¬p ^ 2 ∣ b
H : p ∣ a ^ Nat.succ n
⊢ p ∣ a
exact hp.dvd_of_dvd_pow H
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
⊢ p ^ n * (a ^ Nat.succ n * x ^ n) = p ^ n * (p * y)
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
⊢ a ^ Nat.succ n * x ^ n = p * y
refine' mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) _
no goals
α : Type u_1
β : Type ?u.44629
γ : Type ?u.44632
δ : Type ?u.44635
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
⊢ p ^ n * (a ^ Nat.succ n * x ^ n) = p ^ n * (p * y)
rw [← mul_assoc _ p, ← pow_succ', ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
  mul_assoc]