R : Type u_1
A : Type u_2
K : Type ?u.1163688
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : Field K
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1164225
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : IsDedekindDomain B
L✝ : Ideal B
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝³ : DecidableEq (Ideal R)
inst✝² : DecidableEq (Ideal A)
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ multiplicity
      (↑(↑(idealFactorsEquivOfQuotEquiv f)
          { val := ↑{ val := L, property := hL }, property := (_ : ↑{ val := L, property := hL } ∣ I) }))
      J =
    multiplicity L I
R : Type u_1
A : Type u_2
K : Type ?u.1163688
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : Field K
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1164225
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : IsDedekindDomain B
L✝ : Ideal B
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝³ : DecidableEq (Ideal R)
inst✝² : DecidableEq (Ideal A)
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ multiplicity (↑(↑(normalizedFactorsEquivOfQuotEquiv f hI hJ) { val := L, property := hL })) J = multiplicity L I
rw [normalizedFactorsEquivOfQuotEquiv, Equiv.coe_fn_mk, Subtype.coe_mk]
R : Type u_1
A : Type u_2
K : Type ?u.1163688
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : Field K
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1164225
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : IsDedekindDomain B
L✝ : Ideal B
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝³ : DecidableEq (Ideal R)
inst✝² : DecidableEq (Ideal A)
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ ∀ (l l' : { l // l ∣ I }),
    ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv l) ∣ ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv l') ↔ ↑l ∣ ↑l'
R : Type u_1
A : Type u_2
K : Type ?u.1163688
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : Field K
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1164225
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : IsDedekindDomain B
L✝ : Ideal B
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝³ : DecidableEq (Ideal R)
inst✝² : DecidableEq (Ideal A)
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ multiplicity
      (↑(↑(idealFactorsEquivOfQuotEquiv f)
          { val := ↑{ val := L, property := hL }, property := (_ : ↑{ val := L, property := hL } ∣ I) }))
      J =
    multiplicity L I
refine multiplicity_factor_dvd_iso_eq_multiplicity_of_mem_normalizedFactors hI hJ hL
  (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_
no goals
R : Type u_1
A : Type u_2
K : Type ?u.1163688
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : Field K
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1164225
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : IsDedekindDomain B
L✝ : Ideal B
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝³ : DecidableEq (Ideal R)
inst✝² : DecidableEq (Ideal A)
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ ∀ (l l' : { l // l ∣ I }),
    ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv l) ∣ ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv l') ↔ ↑l ∣ ↑l'
exact fun ⟨l, hl⟩ ⟨l', hl'⟩ => idealFactorsEquivOfQuotEquiv_is_dvd_iso f hl hl'