n : ℕ
⊢ Squarefree n ∧ IsPrimePow n → Prime n
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n ↔ Prime n
refine' ⟨_, fun hn => ⟨hn.squarefree, hn.isPrimePow⟩⟩
n : ℕ
⊢ (Squarefree n ∧ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n → Prime n
rw [isPrimePow_nat_iff]
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree (p ^ k)
⊢ Prime (p ^ k)
n : ℕ
⊢ (Squarefree n ∧ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n
rintro ⟨h, p, k, hp, hk, rfl⟩
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree (p ^ k)
⊢ Prime (p ^ k)
rw [squarefree_pow_iff hp.ne_one hk.ne'] at h
no goals
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)
rwa [h.2, pow_one]