C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ ((ρ_ Yᘁ).inv ≫ (𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (α_ Yᘁ Y Xᘁ).inv ≫ (ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom) ≫ g =
    (ρ_ Yᘁ).inv ≫ (𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Yᘁ ⊗ f ⊗ g) ≫ (α_ Yᘁ Y Z).inv ≫ (ε_ Y Yᘁ ⊗ 𝟙 Z) ≫ (λ_ Z).hom
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ fᘁ ≫ g = (ρ_ Yᘁ).inv ≫ (𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Yᘁ ⊗ f ⊗ g) ≫ (α_ Yᘁ Y Z).inv ≫ (ε_ Y Yᘁ ⊗ 𝟙 Z) ≫ (λ_ Z).hom
dsimp only [rightAdjointMate]
no goals
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ ((ρ_ Yᘁ).inv ≫ (𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (α_ Yᘁ Y Xᘁ).inv ≫ (ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom) ≫ g =
    (ρ_ Yᘁ).inv ≫ (𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Yᘁ ⊗ f ⊗ g) ≫ (α_ Yᘁ Y Z).inv ≫ (ε_ Y Yᘁ ⊗ 𝟙 Z) ≫ (λ_ Z).hom
rw [Category.assoc, Category.assoc, associator_inv_naturality_assoc,
  associator_inv_naturality_assoc, ← tensor_id_comp_id_tensor g, Category.assoc, Category.assoc,
  Category.assoc, Category.assoc, id_tensor_comp_tensor_id_assoc, ← leftUnitor_naturality,
  tensor_id_comp_id_tensor_assoc]