case h
p : ℕ
hp : Prime p
q : ℕ
⊢ ↑(Nat.factorization p) q = ↑(single p 1) q
p : ℕ
hp : Prime p
⊢ Nat.factorization p = single p 1
ext q
no goals
case h
p : ℕ
hp : Prime p
q : ℕ
⊢ ↑(Nat.factorization p) q = ↑(single p 1) q
rw [← factors_count_eq, factors_prime hp, single_apply, count_singleton', if_congr eq_comm] <;>
  rfl