case H
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
⊢ ∀ (x : X₁) (y : X₂) (z : X₃),
    ↑(LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
⊢ LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃) = LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)
apply TensorProduct.ext_threefold
case H
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
x : X₁
y : X₂
z : X₃
⊢ ↑(LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
case H
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
⊢ ∀ (x : X₁) (y : X₂) (z : X₃),
    ↑(LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
intro x y z
no goals
case H
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
x : X₁
y : X₂
z : X₃
⊢ ↑(LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
rfl