case zero
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
q : α
⊢ q ∣ p ^ Nat.zero ↔ ∃ i, i ≤ Nat.zero ∧ q ~ᵤ p ^ i

case succ
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
⊢ q ∣ p ^ Nat.succ n ↔ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q : α
hp : Prime p
n : ℕ
⊢ q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
induction' n with n ih generalizing q
case succ
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p ^ Nat.succ n
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
case succ
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
⊢ q ∣ p ^ Nat.succ n ↔ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
refine' ⟨fun h => _, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩
case succ
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p * p ^ n
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
case succ
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p ^ Nat.succ n
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
rw [pow_succ] at h
case succ.inl.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : p * q ∣ p * p ^ n
⊢ ∃ i, i ≤ Nat.succ n ∧ p * q ~ᵤ p ^ i

case succ.inr
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
case succ
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p * p ^ n
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
no goals
case zero
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
q : α
⊢ q ∣ p ^ Nat.zero ↔ ∃ i, i ≤ Nat.zero ∧ q ~ᵤ p ^ i
simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]
case succ.inl.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
⊢ ∃ i, i ≤ Nat.succ n ∧ p * q ~ᵤ p ^ i
case succ.inl.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : p * q ∣ p * p ^ n
⊢ ∃ i, i ≤ Nat.succ n ∧ p * q ~ᵤ p ^ i
rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h
case succ.inl.intro.intro.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ Nat.succ n ∧ p * q ~ᵤ p ^ i
case succ.inl.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
⊢ ∃ i, i ≤ Nat.succ n ∧ p * q ~ᵤ p ^ i
rcases h with ⟨i, hi, hq⟩
case succ.inl.intro.intro.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ p * p ^ i ~ᵤ p ^ (i + 1)
case succ.inl.intro.intro.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ Nat.succ n ∧ p * q ~ᵤ p ^ i
refine' ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans _⟩
case succ.inl.intro.intro.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ p * p ^ i ~ᵤ p * p ^ i
case succ.inl.intro.intro.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ p * p ^ i ~ᵤ p ^ (i + 1)
rw [pow_succ]
no goals
case succ.inl.intro.intro.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ p * p ^ i ~ᵤ p * p ^ i
rfl
case succ.inr.intro.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
case succ.inr
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
obtain ⟨i, hi, hq⟩ := ih.mp hno
no goals
case succ.inr.intro.intro
α : Type u_1
β : Type ?u.362813
γ : Type ?u.362816
δ : Type ?u.362819
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
exact ⟨i, hi.trans n.le_succ, hq⟩