R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.262567
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ ⊤ ≤ Submodule.span R ↑(invSubmonoid M S)
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.262567
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ Submodule.span R ↑(invSubmonoid M S) = ⊤
rw [eq_top_iff]
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.262567
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : S
⊢ x ∈ Submodule.span R ↑(invSubmonoid M S)
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.262567
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ ⊤ ≤ Submodule.span R ↑(invSubmonoid M S)
rintro x -
case intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.262567
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
r : R
m : { x // x ∈ M }
⊢ r • ↑(↑(toInvSubmonoid M S) m) ∈ Submodule.span R ↑(invSubmonoid M S)
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.262567
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : S
⊢ x ∈ Submodule.span R ↑(invSubmonoid M S)
rcases IsLocalization.surj'' M x with ⟨r, m, rfl⟩
no goals
case intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.262567
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
r : R
m : { x // x ∈ M }
⊢ r • ↑(↑(toInvSubmonoid M S) m) ∈ Submodule.span R ↑(invSubmonoid M S)
exact Submodule.smul_mem _ _ (Submodule.subset_span (toInvSubmonoid M S m).prop)