C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
X X' Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ Y ⊗ Z
⊢ (𝟙 Y' ⊗ f ≫ g) ≫ (α_ Y' Y Z).inv ≫ (ε_ Y Y' ⊗ 𝟙 Z) ≫ (λ_ Z).hom =
    (𝟙 Y' ⊗ f) ≫ (𝟙 Y' ⊗ g) ≫ (α_ Y' Y Z).inv ≫ (ε_ Y Y' ⊗ 𝟙 Z) ≫ (λ_ 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' ⟶ Y ⊗ Z
⊢ ↑(tensorLeftHomEquiv X Y Y' Z).symm (f ≫ g) = (𝟙 Y' ⊗ f) ≫ ↑(tensorLeftHomEquiv X' Y Y' Z).symm g
dsimp [tensorLeftHomEquiv]
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' ⟶ Y ⊗ Z
⊢ (𝟙 Y' ⊗ f ≫ g) ≫ (α_ Y' Y Z).inv ≫ (ε_ Y Y' ⊗ 𝟙 Z) ≫ (λ_ Z).hom =
    (𝟙 Y' ⊗ f) ≫ (𝟙 Y' ⊗ g) ≫ (α_ Y' Y Z).inv ≫ (ε_ Y Y' ⊗ 𝟙 Z) ≫ (λ_ Z).hom
simp only [id_tensor_comp, Category.assoc]