R : Type u_1
K : Type ?u.318539
L : Type ?u.318542
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ (∃ i,
      ↑(MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I * ↑(toPrincipalIdeal R (FractionRing R)) i =
        ↑(MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) J) ↔
    ∃ x, I * ↑(toPrincipalIdeal R (FractionRing R)) x = J
R : Type u_1
K : Type ?u.318539
L : Type ?u.318542
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ↑mk I = ↑mk J ↔ ∃ x, I * ↑(toPrincipalIdeal R (FractionRing R)) x = J
erw [QuotientGroup.mk'_eq_mk', canonicalEquiv_self, Units.map_id, Set.exists_range_iff]
no goals
R : Type u_1
K : Type ?u.318539
L : Type ?u.318542
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ (∃ i,
      ↑(MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I * ↑(toPrincipalIdeal R (FractionRing R)) i =
        ↑(MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) J) ↔
    ∃ x, I * ↑(toPrincipalIdeal R (FractionRing R)) x = J
rfl