case h.e'_2.h.e
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.131549
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
⊢ HSMul.hSMul m = HMul.hMul (↑(algebraMap R 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.131549
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
⊢ m • ↑(↑(toInvSubmonoid M S) m) = 1
convert mul_toInvSubmonoid M S m
case h.e'_2.h.e.h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.131549
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
x✝ : S
⊢ m • x✝ = ↑(algebraMap R S) ↑m * x✝
case h.e'_2.h.e
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.131549
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
⊢ HSMul.hSMul m = HMul.hMul (↑(algebraMap R S) ↑m)
ext
case h.e'_2.h.e.h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.131549
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
x✝ : S
⊢ m • x✝ = ↑m • x✝
case h.e'_2.h.e.h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.131549
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
x✝ : S
⊢ m • x✝ = ↑(algebraMap R S) ↑m * x✝
rw [← Algebra.smul_def]
no goals
case h.e'_2.h.e.h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.131549
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
x✝ : S
⊢ m • x✝ = ↑m • x✝
rfl