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
R₁ : Type ?u.1304874
inst✝³ : CommRing R₁
K : Type ?u.1304880
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : P
I : FractionalIdeal S P
⊢ spanSingleton S x ≤ I ↔ x ∈ I
rw [← coe_le_coe, coe_spanSingleton, Submodule.span_singleton_le_iff_mem, mem_coe]