no goals
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : FractionalIdeal S P
⊢ 1 ≤ I ↔ 1 ∈ I
rw [← coe_le_coe, coe_one, Submodule.one_le, mem_coe]