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