-- Mathlib/Data/Nat/Factorization/PrimePow.lean
theorem isPrimePow_iff_factorization_eq_single {n : ℕ} :
    IsPrimePow n ↔ ∃ p k : ℕ, 0 < k ∧ n.factorization = Finsupp.single p k

Proof state:
case mp
n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n → 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
rintro ⟨hp, hk, hn⟩

Result:
case mp.intro.intro
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ 0 < k ∧ n.factorization = Finsupp.single p k

Proof state:
p k : ℕ
hk : 0 < k
hn : Nat.factorization 0 = Finsupp.single p k
⊢ False

Tactic:
simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']

Result:
no goals

Proof state:
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ n.factorization p ≠ 0

Tactic:
simp [hn, hk.ne']

Result:
no goals

Proof state:
case mpr.intro
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k

Tactic:
exact ⟨Nat.prime_of_mem_primeFactors <|
  Finsupp.mem_support_iff.2 (by simp [hn, hk.ne'] : n.factorization p ≠ 0), hk, rfl⟩

Result:
no goals

Proof state:
n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n ↔ 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
constructor

Result:
case mp
n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n → 0 < k ∧ n.factorization = Finsupp.single p k

case mpr
n p k : ℕ
⊢ 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
p k : ℕ
hk : 0 < k
hn : Nat.factorization 0 = Finsupp.single p k
⊢ False

Proof state:
case mp.intro.intro
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
exact ⟨hk, by rw [← hn, Nat.Prime.factorization_pow hp]⟩

Result:
no goals

Proof state:
case mpr.intro
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
have hn0 : n ≠ 0 := by
  rintro rfl
  simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']

Result:
case mpr.intro
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
case mpr.intro
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]

Result:
case mpr.intro
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k

Proof state:
case mpr
n p k : ℕ
⊢ 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rintro ⟨hk, hn⟩

Result:
case mpr.intro
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ n.factorization = Finsupp.single p k

Tactic:
rw [← hn, Nat.Prime.factorization_pow hp]

Result:
no goals

Proof state:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
refine exists₂_congr fun p k => ?_

Result:
n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n ↔ 0 < k ∧ n.factorization = Finsupp.single p k

Proof state:
n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
rw [isPrimePow_nat_iff]

Result:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k