R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp (LocalizedModule.lift S g h) ↑(LinearEquiv.symm (iso S f)) = l
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ lift S f g h = l
dsimp only [IsLocalizedModule.lift]
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp ↑(iso S f) ↑(LinearEquiv.symm (iso S f)) = LinearMap.id

R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp (LinearMap.comp l ↑(iso S f)) (LocalizedModule.mkLinearMap S M) = g
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp (LocalizedModule.lift S g h) ↑(LinearEquiv.symm (iso S f)) = l
rw [LocalizedModule.lift_unique S g h (l.comp (iso S f).toLinearMap), LinearMap.comp_assoc,
  show (iso S f).toLinearMap.comp (iso S f).symm.toLinearMap = LinearMap.id from _,
  LinearMap.comp_id]
no goals
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp ↑(iso S f) ↑(LinearEquiv.symm (iso S f)) = LinearMap.id
rw [LinearEquiv.comp_toLinearMap_symm_eq, LinearMap.id_comp]
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp l (LinearMap.comp (↑(iso S f)) (LocalizedModule.mkLinearMap S M)) = LinearMap.comp l f
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp (LinearMap.comp l ↑(iso S f)) (LocalizedModule.mkLinearMap S M) = g
rw [LinearMap.comp_assoc, ← hl]
case e_g
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp (↑(iso S f)) (LocalizedModule.mkLinearMap S M) = f
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp l (LinearMap.comp (↑(iso S f)) (LocalizedModule.mkLinearMap S M)) = LinearMap.comp l f
congr 1
case e_g.h
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
x : M
⊢ ↑(LinearMap.comp (↑(iso S f)) (LocalizedModule.mkLinearMap S M)) x = ↑f x
case e_g
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
⊢ LinearMap.comp (↑(iso S f)) (LocalizedModule.mkLinearMap S M) = f
ext x
no goals
case e_g.h
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_4
M'' : Type u_3
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
g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : LinearMap.comp l f = g
x : M
⊢ ↑(LinearMap.comp (↑(iso S f)) (LocalizedModule.mkLinearMap S M)) x = ↑f x
erw [fromLocalizedModule_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, one_smul]