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.1312152
inst✝⁴ : CommRing R₁
K : Type ?u.1312158
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal S P
inst✝ : IsPrincipal ↑I
⊢ I = spanSingleton S (generator ↑I)
rw [spanSingleton, ← coeToSubmodule_inj, coe_mk, span_singleton_generator]