-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : IsCancelMulZero N
m : M
n : N
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
a : Associates M
ha : Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) a
b : Associates M
hb : Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) b
⊢ LE.le.{u_2} (α := (↑(Set.Iic (Associates.mk n)) : Type u_2))
      (({
              toFun := fun (l : (↑(Set.Iic (Associates.mk m)) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Associates N) ↦
                  Membership.mem (γ := Set (Associates N)) (Set.Iic (Associates.mk n)) x)
                  (Associates.mk
                    (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
                          (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
                            ((associatesEquivOfUniqueUnits : (a : Associates M) → M) (↑l : Associates M)) ⋯)) :
                      N))
                  ⋯,
              invFun := fun (l : (↑(Set.Iic (Associates.mk n)) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Associates M) ↦
                  Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
                  (Associates.mk
                    (↑((d.symm : (a : { l : N // l ∣ n }) → { l : M // l ∣ m })
                          (Subtype.mk (p := fun (l : N) ↦ l ∣ n)
                            ((associatesEquivOfUniqueUnits : (a : Associates N) → N) (↑l : Associates N)) ⋯)) :
                      M))
                  ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x) a ha) :
        (↑(Set.Iic (Associates.mk n)) : Type u_2))
      (({
              toFun := fun (l : (↑(Set.Iic (Associates.mk m)) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Associates N) ↦
                  Membership.mem (γ := Set (Associates N)) (Set.Iic (Associates.mk n)) x)
                  (Associates.mk
                    (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
                          (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
                            ((associatesEquivOfUniqueUnits : (a : Associates M) → M) (↑l : Associates M)) ⋯)) :
                      N))
                  ⋯,
              invFun := fun (l : (↑(Set.Iic (Associates.mk n)) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Associates M) ↦
                  Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
                  (Associates.mk
                    (↑((d.symm : (a : { l : N // l ∣ n }) → { l : M // l ∣ m })
                          (Subtype.mk (p := fun (l : N) ↦ l ∣ n)
                            ((associatesEquivOfUniqueUnits : (a : Associates N) → N) (↑l : Associates N)) ⋯)) :
                      M))
                  ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x) b hb) :
        (↑(Set.Iic (Associates.mk n)) : Type u_2)) ↔
    Subtype.mk (p := fun (x : Associates M) ↦ Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x) a
        ha ≤
      Subtype.mk (p := fun (x : Associates M) ↦ Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
        b hb

Tactic:
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Associates.mk_le_mk_iff_dvd, hd,
        associatesEquivOfUniqueUnits_apply, out_dvd_iff, mk_out]

Premises used: Associates.mk_out, Associates.out_dvd_iff, Associates.mk_le_mk_iff_dvd, associatesEquivOfUniqueUnits_apply, Equiv.coe_fn_mk, Subtype.mk_le_mk