C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
X X' Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ Z ⊗ Y'
⊢ (f ≫ g ⊗ 𝟙 Y) ≫ (α_ Z Y' Y).hom ≫ (𝟙 Z ⊗ ε_ Y Y') ≫ (ρ_ Z).hom =
    (f ⊗ 𝟙 Y) ≫ (g ⊗ 𝟙 Y) ≫ (α_ Z Y' Y).hom ≫ (𝟙 Z ⊗ ε_ Y Y') ≫ (ρ_ Z).hom
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
X X' Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ Z ⊗ Y'
⊢ ↑(tensorRightHomEquiv X Y Y' Z).symm (f ≫ g) = (f ⊗ 𝟙 Y) ≫ ↑(tensorRightHomEquiv X' Y Y' Z).symm g
dsimp [tensorRightHomEquiv]
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
X X' Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ Z ⊗ Y'
⊢ (f ≫ g ⊗ 𝟙 Y) ≫ (α_ Z Y' Y).hom ≫ (𝟙 Z ⊗ ε_ Y Y') ≫ (ρ_ Z).hom =
    (f ⊗ 𝟙 Y) ≫ (g ⊗ 𝟙 Y) ≫ (α_ Z Y' Y).hom ≫ (𝟙 Z ⊗ ε_ Y Y') ≫ (ρ_ Z).hom
simp only [comp_tensor_id, Category.assoc]