case H
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑X₁ ↑X₂) (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)) =
    LinearMap.compr₂ (TensorProduct.mk R ↑X₁ ↑X₂) (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂
apply TensorProduct.ext
no goals
case H
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑X₁ ↑X₂) (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)) =
    LinearMap.compr₂ (TensorProduct.mk R ↑X₁ ↑X₂) (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
rfl