case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.160993
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ ∃ r m, z = r • ↑(↑(toInvSubmonoid M S) m)
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.160993
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
⊢ ∃ r m, z = r • ↑(↑(toInvSubmonoid M S) m)
rcases IsLocalization.surj M z with ⟨⟨r, m⟩, e : z * _ = algebraMap R S r⟩
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.160993
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ z = r • ↑(↑(toInvSubmonoid M S) m)
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.160993
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ ∃ r m, z = r • ↑(↑(toInvSubmonoid M S) m)
refine' ⟨r, m, _⟩
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.160993
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ z = z * (↑(algebraMap R S) ↑(r, m).snd * ↑(↑(toInvSubmonoid M S) m))
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.160993
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ z = r • ↑(↑(toInvSubmonoid M S) m)
rw [Algebra.smul_def, ← e, mul_assoc]
no goals
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.160993
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ z = z * (↑(algebraMap R S) ↑(r, m).snd * ↑(↑(toInvSubmonoid M S) m))
simp