p a k : ℕ
hp : Prime p
h : a ^ k = p
⊢ a = p ∧ k = 1
p a k : ℕ
hp : Prime p
⊢ a ^ k = p ↔ a = p ∧ k = 1
refine' ⟨fun h => _, fun h => by rw [h.1, h.2, pow_one]⟩
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = p ∧ k = 1
p a k : ℕ
hp : Prime p
h : a ^ k = p
⊢ a = p ∧ k = 1
rw [← h] at hp
no goals
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = p ∧ k = 1
rw [← h, hp.eq_one_of_pow, eq_self_iff_true, and_true_iff, pow_one]
no goals
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ a ^ k = p
rw [h.1, h.2, pow_one]