case inl
R : Type ?u.706
inst✝ : CommMonoidWithZero R
n p : R
k : ℕ
h : Nat.minFac 0 ^ ↑(Nat.factorization 0) (Nat.minFac 0) = 0
hn : 0 ≠ 1
⊢ IsPrimePow 0

case inr
R : Type ?u.706
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n
R : Type ?u.706
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
⊢ IsPrimePow n
rcases eq_or_ne n 0 with (rfl | hn')
case inr
R : Type ?u.706
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ 0 < ↑(Nat.factorization n) (Nat.minFac n)
case inr
R : Type ?u.706
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n
refine' ⟨_, _, (Nat.minFac_prime hn).prime, _, h⟩
case inr
R : Type ?u.706
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ Nat.minFac n ∣ n
case inr
R : Type ?u.706
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ 0 < ↑(Nat.factorization n) (Nat.minFac n)
rw [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.factor_iff_mem_factorization,
  Nat.mem_factors_iff_dvd hn' (Nat.minFac_prime hn)]
no goals
case inr
R : Type ?u.706
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ Nat.minFac n ∣ n
apply Nat.minFac_dvd
no goals
case inl
R : Type ?u.706
inst✝ : CommMonoidWithZero R
n p : R
k : ℕ
h : Nat.minFac 0 ^ ↑(Nat.factorization 0) (Nat.minFac 0) = 0
hn : 0 ≠ 1
⊢ IsPrimePow 0
simp_all