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.1331786
inst✝³ : CommRing R₁
K : Type ?u.1331792
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x✝ : P
⊢ x✝ ∈ spanSingleton S 1 ↔ x✝ ∈ 1
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.1331786
inst✝³ : CommRing R₁
K : Type ?u.1331792
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
⊢ spanSingleton S 1 = 1
ext
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.1331786
inst✝³ : CommRing R₁
K : Type ?u.1331792
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x✝ : P
⊢ ∀ (a : R), a • 1 = x✝ ↔ ↑(algebraMap R P) a = x✝
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.1331786
inst✝³ : CommRing R₁
K : Type ?u.1331792
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x✝ : P
⊢ x✝ ∈ spanSingleton S 1 ↔ x✝ ∈ 1
refine' (mem_spanSingleton S).trans ((exists_congr _).trans (mem_one_iff S).symm)
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.1331786
inst✝³ : CommRing R₁
K : Type ?u.1331792
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x✝ : P
x' : R
⊢ x' • 1 = x✝ ↔ ↑(algebraMap R P) x' = x✝
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.1331786
inst✝³ : CommRing R₁
K : Type ?u.1331792
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x✝ : P
⊢ ∀ (a : R), a • 1 = x✝ ↔ ↑(algebraMap R P) a = x✝
intro x'
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.1331786
inst✝³ : CommRing R₁
K : Type ?u.1331792
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x✝ : P
x' : R
⊢ x' • 1 = x✝ ↔ ↑(algebraMap R P) x' = x✝
rw [Algebra.smul_def, mul_one]