-- Mathlib/Data/Nat/Factorization/PrimePow.lean
theorem IsPrimePow.exists_ordCompl_eq_one {n : ℕ} (h : IsPrimePow n) :
    ∃ p : ℕ, p.Prime ∧ ordCompl[p] n = 1

Proof state:
case inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
rcases isPrimePow_iff_factorization_eq_single.mp h with ⟨p, k, hk0, h1⟩

Result:
case inr.intro.intro.intro
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Proof state:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ 1 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro.intro.intro.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ n / p ^ n.factorization p = 1

Tactic:
refine Nat.eq_of_factorization_eq (Nat.ordCompl_pos p hn0).ne' (by simp) fun q => ?_

Result:
case inr.intro.intro.intro.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ (n / p ^ n.factorization p).factorization q = (Nat.factorization 1) q

Proof state:
case inr.intro.intro.intro.inl
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
refine absurd ?_ hk0.ne'

Result:
case inr.intro.intro.intro.inl
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ k = 0

Proof state:
case inr.intro.intro.intro
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
rcases em' p.Prime with (pp | pp)

Result:
case inr.intro.intro.intro.inl
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

case inr.intro.intro.intro.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Proof state:
case inr.intro.intro.intro.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
refine ⟨p, pp, ?_⟩

Result:
case inr.intro.intro.intro.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ n / p ^ n.factorization p = 1

Proof state:
case inr.intro.intro.intro.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ (n / p ^ n.factorization p).factorization q = (Nat.factorization 1) q

Tactic:
rw [Nat.factorization_ordCompl n p, h1]

Result:
case inr.intro.intro.intro.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ (Finsupp.erase p (Finsupp.single p k)) q = (Nat.factorization 1) q

Proof state:
case inr.intro.intro.intro.inl
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ k = 0

Tactic:
simp [← Nat.factorization_eq_zero_of_non_prime n pp, h1]

Result:
no goals

Proof state:
case inl
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ (Nat.factorization 0) p = 1

Tactic:
cases not_isPrimePow_zero h

Result:
no goals

Proof state:
case inr.intro.intro.intro.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ (Finsupp.erase p (Finsupp.single p k)) q = (Nat.factorization 1) q

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
h : IsPrimePow n
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
rcases eq_or_ne n 0 with (rfl | hn0)

Result:
case inl
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ (Nat.factorization 0) p = 1

case inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1