no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : HasLeftDual X
⊢ (ᘁ𝟙 X) = 𝟙 ᘁX
simp only [leftAdjointMate, MonoidalCategory.tensor_id, Category.id_comp,
  evaluation_coevaluation_assoc, Category.comp_id, Iso.inv_hom_id]