R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n✝ p : R
k n m : ℕ
hn : ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n✝ p : R
k n m : ℕ
hn : IsPrimePow n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ IsPrimePow m
rw [isPrimePow_nat_iff] at hn⊢
case intro.intro.intro.intro
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ m : ℕ
hm₁ : m ≠ 1
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hm : m ∣ p ^ k
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n✝ p : R
k n m : ℕ
hn : ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
rcases hn with ⟨p, k, hp, _hk, rfl⟩
case intro.intro.intro.intro.intro.intro
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ i
case intro.intro.intro.intro
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ m : ℕ
hm₁ : m ≠ 1
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hm : m ∣ p ^ k
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
obtain ⟨i, hik, rfl⟩ := (Nat.dvd_prime_pow hp).1 hm
case intro.intro.intro.intro.intro.intro
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ 0 < i
case intro.intro.intro.intro.intro.intro
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ i
refine' ⟨p, i, hp, _, rfl⟩
case intro.intro.intro.intro.intro.intro.a
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ i ≠ 0
case intro.intro.intro.intro.intro.intro
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ 0 < i
apply Nat.pos_of_ne_zero
case intro.intro.intro.intro.intro.intro.a
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hik : 0 ≤ k
hm₁ : p ^ 0 ≠ 1
hm : p ^ 0 ∣ p ^ k
⊢ False
case intro.intro.intro.intro.intro.intro.a
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ i ≠ 0
rintro rfl
no goals
case intro.intro.intro.intro.intro.intro.a
R : Type ?u.83807
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hik : 0 ≤ k
hm₁ : p ^ 0 ≠ 1
hm : p ^ 0 ∣ p ^ k
⊢ False
simp only [pow_zero, ne_eq] at hm₁