-- Mathlib/Algebra/Prime/Lemmas.lean
theorem prime_pow_succ_dvd_mul {M : Type*} [CancelCommMonoidWithZero M] {p x y : M} (h : Prime p)
    {i : ℕ} (hxy : p ^ (i + 1) ∣ x * y) : p ^ (i + 1) ∣ x ∨ p ∣ y

Proof state:
case succ
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : M}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x : M
hxy : p ^ (i + 1 + 1) ∣ x * y
⊢ p ^ (i + 1 + 1) ∣ x

Tactic:
rw [pow_succ'] at hxy ⊢

Result:
case succ
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : M}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x : M
hxy : p * p ^ (i + 1) ∣ x * y
⊢ p * p ^ (i + 1) ∣ x

Proof state:
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
hy : ¬p ∣ y
⊢ p ^ (i + 1) ∣ x

Tactic:
induction i generalizing x with
| zero => rw [pow_one] at hxy ⊢; exact (h.dvd_or_dvd hxy).resolve_right hy
| succ i ih =>
  rw [pow_succ'] at hxy ⊢
  obtain ⟨x', rfl⟩ := (h.dvd_or_dvd (dvd_of_mul_right_dvd hxy)).resolve_right hy
  rw [mul_assoc] at hxy
  exact mul_dvd_mul_left p (ih ((mul_dvd_mul_iff_left h.ne_zero).mp hxy))

Result:
no goals

Proof state:
case succ
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : M}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x : M
hxy : p * p ^ (i + 1) ∣ x * y
⊢ p * p ^ (i + 1) ∣ x

Tactic:
obtain ⟨x', rfl⟩ := (h.dvd_or_dvd (dvd_of_mul_right_dvd hxy)).resolve_right hy

Result:
case succ.intro
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : M}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : M
hxy : p * p ^ (i + 1) ∣ p * x' * y
⊢ p * p ^ (i + 1) ∣ p * x'

Proof state:
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ p ^ (i + 1) ∣ x ∨ p ∣ y

Tactic:
rw [or_iff_not_imp_right]

Result:
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x

Proof state:
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x

Tactic:
intro hy

Result:
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
hy : ¬p ∣ y
⊢ p ^ (i + 1) ∣ x

Proof state:
case zero
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
x : M
hxy : p ^ (0 + 1) ∣ x * y
⊢ p ^ (0 + 1) ∣ x

Tactic:
rw [pow_one] at hxy ⊢

Result:
case zero
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
x : M
hxy : p ∣ x * y
⊢ p ∣ x

Proof state:
case succ.intro
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : M}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : M
hxy : p * p ^ (i + 1) ∣ p * x' * y
⊢ p * p ^ (i + 1) ∣ p * x'

Tactic:
rw [mul_assoc] at hxy

Result:
case succ.intro
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : M}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : M
hxy : p * p ^ (i + 1) ∣ p * (x' * y)
⊢ p * p ^ (i + 1) ∣ p * x'

Proof state:
case succ.intro
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : M}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : M
hxy : p * p ^ (i + 1) ∣ p * (x' * y)
⊢ p * p ^ (i + 1) ∣ p * x'

Tactic:
exact mul_dvd_mul_left p (ih ((mul_dvd_mul_iff_left h.ne_zero).mp hxy))

Result:
no goals

Proof state:
case zero
M : Type u_3
inst✝ : CancelCommMonoidWithZero M
p y : M
h : Prime p
hy : ¬p ∣ y
x : M
hxy : p ∣ x * y
⊢ p ∣ x

Tactic:
exact (h.dvd_or_dvd hxy).resolve_right hy

Result:
no goals