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