-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem dvd_prime_pow [CancelCommMonoidWithZero M] {p q : M} (hp : Prime p) (n : ℕ) :
    q ∣ p ^ n ↔ ∃ i ≤ n, Associated q (p ^ i)

Proof state:
case succ.inl.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ p * p ^ i ~ᵤ p ^ (i + 1)

Tactic:
rw [pow_succ']

Result:
no goals

Proof state:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
⊢ ∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

Tactic:
rcases h with ⟨i, hi, hq⟩

Result:
case succ.inl.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

Proof state:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)

Result:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : p * q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

case succ.inr
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Proof state:
case succ.inr
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
obtain ⟨i, hi, hq⟩ := ih.mp hno

Result:
case succ.inr.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Proof state:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : p * q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

Tactic:
rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h

Result:
case succ.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
⊢ ∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

Proof state:
case succ.inl.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

Tactic:
refine ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩

Result:
case succ.inl.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ p * p ^ i ~ᵤ p ^ (i + 1)

Proof state:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
⊢ q ∣ p ^ (n + 1) ↔ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
refine ⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩

Result:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p ^ (n + 1)
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Proof state:
case succ.inr.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
exact ⟨i, hi.trans n.le_succ, hq⟩

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p ^ (n + 1)
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
rw [pow_succ'] at h

Result:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Proof state:
case zero
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
q : M
⊢ q ∣ p ^ 0 ↔ ∃ i, i ≤ 0 ∧ q ~ᵤ p ^ i

Tactic:
simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]

Result:
no goals