case hl
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_4
M' : Type u_3
M'' : Type u_2
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
map_unit : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : LinearMap.comp j f = LinearMap.comp k f
⊢ LinearMap.comp k f = LinearMap.comp k f
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_4
M' : Type u_3
M'' : Type u_2
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
map_unit : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : LinearMap.comp j f = LinearMap.comp k f
⊢ j = k
rw [← lift_unique S f (k.comp f) map_unit j h, lift_unique]
no goals
case hl
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_4
M' : Type u_3
M'' : Type u_2
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
map_unit : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : LinearMap.comp j f = LinearMap.comp k f
⊢ LinearMap.comp k f = LinearMap.comp k f
rfl