{R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [IsFractionRing R K] →
            [IsDedekindDomain R] →
              (I J I' J' : FractionalIdeal (nonZeroDivisors R) K) →
                I * J' = I' * J →
                  J ≤ I →
                    J' ≤ I' →
                      J' ≠ 0 →
                        I ≠ 0 → (↥↑I ⧸ Submodule.comap (↑I).subtype ↑J) ≃ₗ[R] ↥↑I' ⧸ Submodule.comap (↑I').subtype ↑J'