-- Mathlib/RingTheory/Localization/BaseChange.lean
lemma IsLocalizedModule.map_lTensor (g : M →ₗ[A] M') [h : IsLocalizedModule S g] :
    IsLocalizedModule.map S (AlgebraTensorModule.rTensor R N g) (AlgebraTensorModule.rTensor R P g)
      (AlgebraTensorModule.lTensor A M f) = AlgebraTensorModule.lTensor A M' f

Proof state:
case h
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (map S ((AlgebraTensorModule.rTensor R N) g) ((AlgebraTensorModule.rTensor R P) g))
        ((AlgebraTensorModule.lTensor A M) f) ∘ₗ
      (AlgebraTensorModule.rTensor R N) g =
    (AlgebraTensorModule.lTensor A M') f ∘ₗ (AlgebraTensorModule.rTensor R N) g

Tactic:
rw [map_comp]

Result:
case h
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (AlgebraTensorModule.rTensor R P) g ∘ₗ (AlgebraTensorModule.lTensor A M) f =
    (AlgebraTensorModule.lTensor A M') f ∘ₗ (AlgebraTensorModule.rTensor R N) g

Proof state:
case h
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (AlgebraTensorModule.rTensor R P) g ∘ₗ (AlgebraTensorModule.lTensor A M) f =
    (AlgebraTensorModule.lTensor A M') f ∘ₗ (AlgebraTensorModule.rTensor R N) g

Tactic:
ext

Result:
case h.a.h.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry ((AlgebraTensorModule.rTensor R P) g ∘ₗ (AlgebraTensorModule.lTensor A M) f)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((AlgebraTensorModule.lTensor A M') f ∘ₗ (AlgebraTensorModule.rTensor R N) g)) x✝¹) x✝

Proof state:
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (map S ((AlgebraTensorModule.rTensor R N) g) ((AlgebraTensorModule.rTensor R P) g))
      ((AlgebraTensorModule.lTensor A M) f) =
    (AlgebraTensorModule.lTensor A M') f

Tactic:
apply linearMap_ext S (AlgebraTensorModule.rTensor R N g) (AlgebraTensorModule.rTensor R P g)

Result:
case h
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (map S ((AlgebraTensorModule.rTensor R N) g) ((AlgebraTensorModule.rTensor R P) g))
        ((AlgebraTensorModule.lTensor A M) f) ∘ₗ
      (AlgebraTensorModule.rTensor R N) g =
    (AlgebraTensorModule.lTensor A M') f ∘ₗ (AlgebraTensorModule.rTensor R N) g

Proof state:
case h.a.h.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry ((AlgebraTensorModule.rTensor R P) g ∘ₗ (AlgebraTensorModule.lTensor A M) f)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((AlgebraTensorModule.lTensor A M') f ∘ₗ (AlgebraTensorModule.rTensor R N) g)) x✝¹) x✝

Tactic:
simp

Result:
no goals