case a
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.1321354
inst✝³ : CommRing R₁
K : Type ?u.1321360
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x✝ : P
⊢ x✝ ∈ spanSingleton S 0 ↔ x✝ ∈ 0
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.1321354
inst✝³ : CommRing R₁
K : Type ?u.1321360
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
⊢ spanSingleton S 0 = 0
ext
no goals
case a
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.1321354
inst✝³ : CommRing R₁
K : Type ?u.1321360
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x✝ : P
⊢ x✝ ∈ spanSingleton S 0 ↔ x✝ ∈ 0
simp [Submodule.mem_span_singleton, eq_comm]