case inl
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n p : R
k : ℕ
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ ↑(Nat.factorization 0) p = 1

case inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : IsPrimePow n
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
rcases eq_or_ne n 0 with (rfl | hn0)
case inr.intro.intro.intro
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
case inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
rcases isPrimePow_iff_factorization_eq_single.mp h with ⟨p, k, hk0, h1⟩
case inr.intro.intro.intro.inl
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1

case inr.intro.intro.intro.inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
case inr.intro.intro.intro
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
rcases em' p.Prime with (pp | pp)
case inr.intro.intro.intro.inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ n / p ^ ↑(Nat.factorization n) p = 1
case inr.intro.intro.intro.inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
refine' ⟨p, pp, _⟩
case inr.intro.intro.intro.inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ ↑(Nat.factorization (n / p ^ ↑(Nat.factorization n) p)) q = ↑(Nat.factorization 1) q
case inr.intro.intro.intro.inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ n / p ^ ↑(Nat.factorization n) p = 1
refine' Nat.eq_of_factorization_eq (Nat.ord_compl_pos p hn0).ne' (by simp) fun q => _
case inr.intro.intro.intro.inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ ↑(Finsupp.erase p (Finsupp.single p k)) q = ↑(Nat.factorization 1) q
case inr.intro.intro.intro.inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ ↑(Nat.factorization (n / p ^ ↑(Nat.factorization n) p)) q = ↑(Nat.factorization 1) q
rw [Nat.factorization_ord_compl n p, h1]
no goals
case inr.intro.intro.intro.inr
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ ↑(Finsupp.erase p (Finsupp.single p k)) q = ↑(Nat.factorization 1) q
simp
no goals
case inl
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n p : R
k : ℕ
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ ↑(Nat.factorization 0) p = 1
cases not_isPrimePow_zero h
case inr.intro.intro.intro.inl
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ k = 0
case inr.intro.intro.intro.inl
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
refine' absurd _ hk0.ne'
no goals
case inr.intro.intro.intro.inl
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ k = 0
simp [← Nat.factorization_eq_zero_of_non_prime n pp, h1]
no goals
R : Type ?u.4264
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ 1 ≠ 0
simp