no goals
R : Type u_1
A : Type ?u.1418572
K : Type ?u.1418575
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : IsDomain A
inst✝⁶ : IsDomain R
inst✝⁵ : IsPrincipalIdealRing R
inst✝⁴ : DecidableEq R
inst✝³ : DecidableEq (Ideal R)
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
r d : R
hr : r ≠ 0
hd : d ∈ normalizedFactors r
⊢ multiplicity d r =
    multiplicity (↑(↑(normalizedFactorsEquivSpanNormalizedFactors hr) { val := d, property := hd })) (span {r})
simp only [normalizedFactorsEquivSpanNormalizedFactors, multiplicity_eq_multiplicity_span,
  Subtype.coe_mk, Equiv.ofBijective_apply]