R : Type ?u.1213100
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1213307
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J✝ I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ { val := ↑J / ↑J', property := (_ : IsFractional R₁⁰ (↑J / ↑J')) } ↔ I * J' ≤ J
R : Type ?u.1213100
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1213307
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J✝ I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ J / J' ↔ I * J' ≤ J
rw [div_nonzero hJ']
R : Type ?u.1213100
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1213307
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J✝ I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ { val := ↑J / ↑J', property := (_ : IsFractional R₁⁰ (↑J / ↑J')) } ↔ ↑I * ↑J' ≤ ↑J
R : Type ?u.1213100
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1213307
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J✝ I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ { val := ↑J / ↑J', property := (_ : IsFractional R₁⁰ (↑J / ↑J')) } ↔ I * J' ≤ J
rw [← coe_le_coe (I := I * J') (J := J), coe_mul]
no goals
R : Type ?u.1213100
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1213307
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J✝ I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ { val := ↑J / ↑J', property := (_ : IsFractional R₁⁰ (↑J / ↑J')) } ↔ ↑I * ↑J' ≤ ↑J
exact Submodule.le_div_iff_mul_le