-- Mathlib/Data/Nat/Factorization/PrimePow.lean
theorem isPrimePow_iff_unique_prime_dvd {n : ℕ} : IsPrimePow n ↔ ∃! p : ℕ, p.Prime ∧ p ∣ n

Proof state:
case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p, Nat.Prime p ∧ p ∣ n

Tactic:
rintro ⟨p, k, hp, hk, rfl⟩

Result:
case mp.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃! p_1, Nat.Prime p_1 ∧ p_1 ∣ p ^ k

Proof state:
case mpr
n : ℕ
⊢ (∃! p, Nat.Prime p ∧ p ∣ n) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rintro ⟨p, ⟨hp, hn⟩, hq⟩

Result:
case mpr.intro.intro.intro
n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
case mpr.intro.intro.intro.inr.refl
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
hq' : Nat.Prime p ∧ p ∣ n
⊢ List.count p n.primeFactorsList ≤ List.count p (List.replicate (n.factorization p) p)

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.intro.inl
p : ℕ
hp : Nat.Prime p
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ 0) y → y = p
hn : p ∣ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = 0

Tactic:
cases (hq 2 ⟨Nat.prime_two, dvd_zero 2⟩).trans (hq 3 ⟨Nat.prime_three, dvd_zero 3⟩).symm

Result:
no goals

Proof state:
case mpr.intro.intro.intro.inr
n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
refine ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, ?_⟩

Result:
case mpr.intro.intro.intro.inr
n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ p ^ n.factorization p = n

Proof state:
case mp.intro.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ k
⊢ q = p

Tactic:
exact (Nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq')

Result:
no goals

Proof state:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ p ^ n.factorization p = n

Tactic:
apply Nat.dvd_antisymm (Nat.ordProj_dvd _ _)

Result:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n ∣ p ^ n.factorization p

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

Tactic:
constructor

Result:
case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p, Nat.Prime p ∧ p ∣ n

case mpr
n : ℕ
⊢ (∃! p, Nat.Prime p ∧ p ∣ n) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
case mpr.intro.intro.intro
n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn₀)

Result:
case mpr.intro.intro.intro.inl
p : ℕ
hp : Nat.Prime p
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ 0) y → y = p
hn : p ∣ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = 0

case mpr.intro.intro.intro.inr
n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ ∀ x ∈ n.primeFactorsList, List.count x n.primeFactorsList ≤ List.count x (List.replicate (n.factorization p) p)

Tactic:
intro q hq'

Result:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : q ∈ n.primeFactorsList
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)

Proof state:
case mp.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∀ (y : ℕ), (fun p_1 => Nat.Prime p_1 ∧ p_1 ∣ p ^ k) y → y = p

Tactic:
rintro q ⟨hq, hq'⟩

Result:
case mp.intro.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ k
⊢ q = p

Proof state:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n ∣ p ^ n.factorization p

Tactic:
apply Nat.dvd_of_primeFactorsList_subperm hn₀

Result:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n.primeFactorsList.Subperm (p ^ n.factorization p).primeFactorsList

Proof state:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : q ∈ n.primeFactorsList
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)

Tactic:
rw [Nat.mem_primeFactorsList hn₀] at hq'

Result:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : Nat.Prime q ∧ q ∣ n
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)

Proof state:
case mpr.intro.intro.intro.inr
n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ p ^ n.factorization p = n

Tactic:
simp only [and_imp] at hq

Result:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ p ^ n.factorization p = n

Proof state:
n : ℕ
⊢ IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n

Tactic:
rw [isPrimePow_nat_iff]

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

Proof state:
case mp.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃! p_1, Nat.Prime p_1 ∧ p_1 ∣ p ^ k

Tactic:
refine ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, ?_⟩

Result:
case mp.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∀ (y : ℕ), (fun p_1 => Nat.Prime p_1 ∧ p_1 ∣ p ^ k) y → y = p

Proof state:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : Nat.Prime q ∧ q ∣ n
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)

Tactic:
cases hq _ hq'.1 hq'.2

Result:
case mpr.intro.intro.intro.inr.refl
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
hq' : Nat.Prime p ∧ p ∣ n
⊢ List.count p n.primeFactorsList ≤ List.count p (List.replicate (n.factorization p) p)

Proof state:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n.primeFactorsList.Subperm (p ^ n.factorization p).primeFactorsList

Tactic:
rw [hp.primeFactorsList_pow, List.subperm_ext_iff]

Result:
case mpr.intro.intro.intro.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ ∀ x ∈ n.primeFactorsList, List.count x n.primeFactorsList ≤ List.count x (List.replicate (n.factorization p) p)