R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.663918
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : { x // x ∈ S }
eq1 : (m, s).snd • x = ↑f (m, s).fst
⊢ (m, s).snd • x = ↑s • x
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.663918
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : { x // x ∈ S }
eq1 : (m, s).snd • x = ↑f (m, s).fst
⊢ ↑(fromLocalizedModule S f) (LocalizedModule.mk m s) = x
rw [fromLocalizedModule_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← eq1]
no goals
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.663918
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : { x // x ∈ S }
eq1 : (m, s).snd • x = ↑f (m, s).fst
⊢ (m, s).snd • x = ↑s • x
rfl