case H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ ∀ (x : ↑X₁) (y : ↑X₂), ↑((f ⊗ g) ≫ (braiding Y₁ Y₂).hom) (x ⊗ₜ[R] y) = ↑((braiding X₁ X₂).hom ≫ (g ⊗ f)) (x ⊗ₜ[R] y)
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (f ⊗ g) ≫ (braiding Y₁ Y₂).hom = (braiding X₁ X₂).hom ≫ (g ⊗ f)
apply TensorProduct.ext'
case H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : ↑X₁
y : ↑X₂
⊢ ↑((f ⊗ g) ≫ (braiding Y₁ Y₂).hom) (x ⊗ₜ[R] y) = ↑((braiding X₁ X₂).hom ≫ (g ⊗ f)) (x ⊗ₜ[R] y)
case H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ ∀ (x : ↑X₁) (y : ↑X₂), ↑((f ⊗ g) ≫ (braiding Y₁ Y₂).hom) (x ⊗ₜ[R] y) = ↑((braiding X₁ X₂).hom ≫ (g ⊗ f)) (x ⊗ₜ[R] y)
intro x y
no goals
case H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : ↑X₁
y : ↑X₂
⊢ ↑((f ⊗ g) ≫ (braiding Y₁ Y₂).hom) (x ⊗ₜ[R] y) = ↑((braiding X₁ X₂).hom ≫ (g ⊗ f)) (x ⊗ₜ[R] y)
rfl