R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type ?u.503966
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✝ g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
r : R
m : LocalizedModule S M
a : M
b : { x // x ∈ S }
⊢ r • lift' S g h (Quotient.mk (r.setoid S M) (a, b)) = lift' S g h (r • Quotient.mk (r.setoid S M) (a, b))
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type ?u.503966
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✝ g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
r : R
m : LocalizedModule S M
⊢ ∀ (a : M × { x // x ∈ S }),
    r • lift' S g h (Quotient.mk (r.setoid S M) a) = lift' S g h (r • Quotient.mk (r.setoid S M) a)
intro ⟨a, b⟩
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type ?u.503966
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✝ g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
r : R
m : LocalizedModule S M
a : M
b : { x // x ∈ S }
⊢ r • ↑↑(IsUnit.unit (_ : IsUnit (↑(algebraMap R (Module.End R M'')) ↑b)))⁻¹ (↑g a) =
    ↑↑(IsUnit.unit (_ : IsUnit (↑(algebraMap R (Module.End R M'')) ↑b)))⁻¹ (↑g (r • a))
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type ?u.503966
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✝ g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
r : R
m : LocalizedModule S M
a : M
b : { x // x ∈ S }
⊢ r • lift' S g h (Quotient.mk (r.setoid S M) (a, b)) = lift' S g h (r • Quotient.mk (r.setoid S M) (a, b))
erw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk]
no goals
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type ?u.503966
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✝ g : M →ₗ[R] M''
h : ∀ (x : { x // x ∈ S }), IsUnit (↑(algebraMap R (Module.End R M'')) ↑x)
r : R
m : LocalizedModule S M
a : M
b : { x // x ∈ S }
⊢ r • ↑↑(IsUnit.unit (_ : IsUnit (↑(algebraMap R (Module.End R M'')) ↑b)))⁻¹ (↑g a) =
    ↑↑(IsUnit.unit (_ : IsUnit (↑(algebraMap R (Module.End R M'')) ↑b)))⁻¹ (↑g (r • a))
erw [← map_smul, ← g.map_smul]