case H.h.h
R : Type u_4
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1235162
inst✝¹³ : Monoid R'
R'' : Type ?u.1235168
inst✝¹² : Semiring R''
M : Type u_1
N : Type u_2
P : Type u_5
Q : Type u_3
S : Type ?u.1235186
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : M
n : N
⊢ ↑(↑(compr₂ (TensorProduct.mk R M N) (lTensor M (comp g f))) m) n =
    ↑(↑(compr₂ (TensorProduct.mk R M N) (comp (lTensor M g) (lTensor M f))) m) n
R : Type u_4
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1235162
inst✝¹³ : Monoid R'
R'' : Type ?u.1235168
inst✝¹² : Semiring R''
M : Type u_1
N : Type u_2
P : Type u_5
Q : Type u_3
S : Type ?u.1235186
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
g : P →ₗ[R] Q
f : N →ₗ[R] P
⊢ lTensor M (comp g f) = comp (lTensor M g) (lTensor M f)
ext (m n)
no goals
case H.h.h
R : Type u_4
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1235162
inst✝¹³ : Monoid R'
R'' : Type ?u.1235168
inst✝¹² : Semiring R''
M : Type u_1
N : Type u_2
P : Type u_5
Q : Type u_3
S : Type ?u.1235186
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : M
n : N
⊢ ↑(↑(compr₂ (TensorProduct.mk R M N) (lTensor M (comp g f))) m) n =
    ↑(↑(compr₂ (TensorProduct.mk R M N) (comp (lTensor M g) (lTensor M f))) m) n
simp only [compr₂_apply, mk_apply, comp_apply, lTensor_tmul]