-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this :
  LE.le.{u_2} (α := (↑{p : Ideal A | p ∣ J} : Type u_2))
      ((idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM) :
        (↑{p : Ideal A | p ∣ J} : Type u_2))
      ((idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL) :
        (↑{p : Ideal A | p ∣ J} : Type u_2)) ↔
    LE.le (α := { x : Ideal R // Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x })
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM)
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL)
rw :
  LE.le.{u_2} (α := Ideal A)
      (↑((idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM)) :
        Ideal A)
      (↑((idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL)) :
        Ideal A) ↔
    L ∣ M
rw₁ :
  LE.le.{u_2} (α := Ideal A)
      (↑((idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM)) :
        Ideal A)
      (↑((idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL)) :
        Ideal A) ↔
    M ≤ L
rw₂ :
  LE.le.{u_2} (α := { x : Ideal A // Membership.mem (γ := Set (Ideal A)) {p : Ideal A | p ∣ J} x })
      ((idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM) :
        (↑{p : Ideal A | p ∣ J} : Type u_2))
      ((idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL) :
        (↑{p : Ideal A | p ∣ J} : Type u_2)) ↔
    M ≤ L
rw₃ :
  LE.le (α := { x : Ideal R // Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x })
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM)
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL) ↔
    M ≤ L
rw₄ rw₅ : M ≤ L ↔ M ≤ L
⊢ Dvd.dvd.{u_2} (α := Ideal A)
      (↑((idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL)) :
        Ideal A)
      (↑((idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM)) :
        Ideal A) ↔
    L ∣ M

Tactic:
rw [dvd_iff_le, dvd_iff_le, Subtype.coe_le_coe, this, Subtype.mk_le_mk]

Premises used: Ideal.dvd_iff_le, Subtype.coe_le_coe, Subtype.mk_le_mk