case h
R : Type u_5
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1128882
inst✝¹³ : Monoid R'
R'' : Type ?u.1128888
inst✝¹² : Semiring R''
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
S : Type ?u.1128906
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
x✝ : (M ⊗[R] P) ⊗[R] N ⊗[R] Q
⊢ ↑(LinearEquiv.symm (tensorTensorTensorComm R M N P Q)) x✝ = ↑(tensorTensorTensorComm R M P N Q) x✝
R : Type u_5
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1128882
inst✝¹³ : Monoid R'
R'' : Type ?u.1128888
inst✝¹² : Semiring R''
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
S : Type ?u.1128906
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
⊢ LinearEquiv.symm (tensorTensorTensorComm R M N P Q) = tensorTensorTensorComm R M P N Q
ext
no goals
case h
R : Type u_5
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1128882
inst✝¹³ : Monoid R'
R'' : Type ?u.1128888
inst✝¹² : Semiring R''
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
S : Type ?u.1128906
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
x✝ : (M ⊗[R] P) ⊗[R] N ⊗[R] Q
⊢ ↑(LinearEquiv.symm (tensorTensorTensorComm R M N P Q)) x✝ = ↑(tensorTensorTensorComm R M P N Q) x✝
rfl