-- Mathlib/Algebra/Prime/Lemmas.lean
theorem Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd [CancelCommMonoidWithZero M] {p a b : M}
    {n : ℕ} (hp : Prime p) (hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n) (hb : ¬p ^ 2 ∣ b) : p ∣ a

Proof state:
case inr.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ∣ a

Tactic:
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]

Result:
case inr.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
⊢ p ∣ a

Proof state:
case inr.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
hdvdx : p ∣ x ^ n
⊢ p ^ 2 ∣ p * x

Tactic:
obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx

Result:
case inr.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p ^ 2 ∣ p * (p * z)

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
⊢ p ∣ a

Tactic:
rcases hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H | hbdiv

Result:
case inl
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
H : p ∣ a ^ n.succ
⊢ p ∣ a

case inr
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
hbdiv : p ∣ b ^ n
⊢ p ∣ a

Proof state:
case inr.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
⊢ p ∣ a

Tactic:
refine hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right fun hdvdx => hb ?_)

Result:
case inr.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
hdvdx : p ∣ x ^ n
⊢ p ^ 2 ∣ p * x

Proof state:
case inr.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p * p ∣ p * p * z

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
case inr.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p ^ 2 ∣ p * (p * z)

Tactic:
rw [pow_two, ← mul_assoc]

Result:
case inr.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p * p ∣ p * p * z

Proof state:
case inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hpow : p ^ n.succ ∣ a ^ n.succ * (p * x) ^ n
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
⊢ p ∣ a

Tactic:
obtain ⟨y, hy⟩ := hpow

Result:
case inr.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ∣ a

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ a ^ n.succ * x ^ n = p * y

Tactic:
refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)

Proof state:
case inr
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
hbdiv : p ∣ b ^ n
⊢ p ∣ a

Tactic:
obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv

Result:
case inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hpow : p ^ n.succ ∣ a ^ n.succ * (p * x) ^ n
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
⊢ p ∣ a

Proof state:
case inl
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
H : p ∣ a ^ n.succ
⊢ p ∣ a

Tactic:
exact hp.dvd_of_dvd_pow H

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)

Tactic:
rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
  mul_assoc]

Result:
no goals