case intro
R : Type u_1
A : Type ?u.1422103
K : Type ?u.1422106
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 : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
x : ↑{d | d ∈ normalizedFactors r}
hx : ↑(normalizedFactorsEquivSpanNormalizedFactors hr) x = I
⊢ multiplicity (↑(↑(normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑I) (span {r})
R : Type u_1
A : Type ?u.1422103
K : Type ?u.1422106
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 : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
⊢ multiplicity (↑(↑(normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑I) (span {r})
obtain ⟨x, hx⟩ := (normalizedFactorsEquivSpanNormalizedFactors hr).surjective I
case intro.mk
R : Type u_1
A : Type ?u.1422103
K : Type ?u.1422106
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 : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
hx : ↑(normalizedFactorsEquivSpanNormalizedFactors hr) { val := a, property := ha } = I
⊢ multiplicity (↑(↑(normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑I) (span {r})
case intro
R : Type u_1
A : Type ?u.1422103
K : Type ?u.1422106
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 : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
x : ↑{d | d ∈ normalizedFactors r}
hx : ↑(normalizedFactorsEquivSpanNormalizedFactors hr) x = I
⊢ multiplicity (↑(↑(normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑I) (span {r})
obtain ⟨a, ha⟩ := x
no goals
case intro.mk
R : Type u_1
A : Type ?u.1422103
K : Type ?u.1422106
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 : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
hx : ↑(normalizedFactorsEquivSpanNormalizedFactors hr) { val := a, property := ha } = I
⊢ multiplicity (↑(↑(normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑I) (span {r})
rw [hx.symm, Equiv.symm_apply_apply, Subtype.coe_mk,
  multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity hr ha, hx]