R : Type u_1
A : Type u_2
K : Type ?u.1117270
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Field K
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1117807
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDedekindDomain B
L✝ : Ideal B
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
⊢ ↑(idealFactorsEquivOfQuotEquiv f) { val := M, property := hM } ≤
      ↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := hL } ↔
    { val := M, property := hM } ≤ { val := L, property := hL }
R : Type u_1
A : Type u_2
K : Type ?u.1117270
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Field K
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1117807
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDedekindDomain B
L✝ : Ideal B
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := hL }) ∣
      ↑(↑(idealFactorsEquivOfQuotEquiv f) { val := M, property := hM }) ↔
    L ∣ M
suffices
  idealFactorsEquivOfQuotEquiv f ⟨M, hM⟩ ≤ idealFactorsEquivOfQuotEquiv f ⟨L, hL⟩ ↔
    (⟨M, hM⟩ : { p : Ideal R | p ∣ I }) ≤ ⟨L, hL⟩
  by rw [dvd_iff_le, dvd_iff_le, Subtype.coe_le_coe, this, Subtype.mk_le_mk]
no goals
R : Type u_1
A : Type u_2
K : Type ?u.1117270
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Field K
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1117807
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDedekindDomain B
L✝ : Ideal B
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
⊢ ↑(idealFactorsEquivOfQuotEquiv f) { val := M, property := hM } ≤
      ↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := hL } ↔
    { val := M, property := hM } ≤ { val := L, property := hL }
exact (idealFactorsEquivOfQuotEquiv f).le_iff_le
no goals
R : Type u_1
A : Type u_2
K : Type ?u.1117270
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Field K
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1117807
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDedekindDomain B
L✝ : Ideal B
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this :
  ↑(idealFactorsEquivOfQuotEquiv f) { val := M, property := hM } ≤
      ↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := hL } ↔
    { val := M, property := hM } ≤ { val := L, property := hL }
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := hL }) ∣
      ↑(↑(idealFactorsEquivOfQuotEquiv f) { val := M, property := hM }) ↔
    L ∣ M
rw [dvd_iff_le, dvd_iff_le, Subtype.coe_le_coe, this, Subtype.mk_le_mk]