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.1308502
inst✝⁴ : CommRing R₁
K : Type ?u.1308508
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : NoZeroSMulDivisors R P
x y : P
⊢ { val := span R {x}, property := (_ : IsFractional S (span R {x})) } =
      { val := span R {y}, property := (_ : IsFractional S (span R {y})) } ↔
    span R {x} = span R {y}
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.1308502
inst✝⁴ : CommRing R₁
K : Type ?u.1308508
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : NoZeroSMulDivisors R P
x y : P
⊢ spanSingleton S x = spanSingleton S y ↔ ∃ z, z • x = y
rw [← Submodule.span_singleton_eq_span_singleton, spanSingleton, spanSingleton]
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.1308502
inst✝⁴ : CommRing R₁
K : Type ?u.1308508
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : NoZeroSMulDivisors R P
x y : P
⊢ { val := span R {x}, property := (_ : IsFractional S (span R {x})) } =
      { val := span R {y}, property := (_ : IsFractional S (span R {y})) } ↔
    span R {x} = span R {y}
exact Subtype.mk_eq_mk