case H
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
⊢ ∀ (w : W) (x : X) (y : Y) (z : Z),
    ↑(LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1))
        (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
⊢ LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1) =
    LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)
apply TensorProduct.ext_fourfold
case H
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
w : W
x : X
y : Y
z : Z
⊢ ↑(LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1))
      (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
case H
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
⊢ ∀ (w : W) (x : X) (y : Y) (z : Z),
    ↑(LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1))
        (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
intro w x y z
no goals
case H
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
w : W
x : X
y : Y
z : Z
⊢ ↑(LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1))
      (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
rfl