no goals
p : ℕ
hp : Prime p
⊢ Part.get (multiplicity ↑p ↑p) (_ : multiplicity.Finite ↑p ↑p) % 2 = 1
simp [multiplicity.multiplicity_self
  (mt isUnit_iff_dvd_one.1 (mt Int.coe_nat_dvd.1 hp.not_dvd_one))]