R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1296088
inst✝³ : CommRing R₁
K : Type ?u.1296094
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : P
⊢ ↑{ val := span R {x}, property := (_ : IsFractional S (span R {x})) } = span R {x}
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1296088
inst✝³ : CommRing R₁
K : Type ?u.1296094
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : P
⊢ ↑(spanSingleton S x) = span R {x}
rw [spanSingleton]
no goals
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1296088
inst✝³ : CommRing R₁
K : Type ?u.1296094
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : P
⊢ ↑{ val := span R {x}, property := (_ : IsFractional S (span R {x})) } = span R {x}
rfl