no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : HasRightDual X
⊢ 𝟙 Xᘁ = 𝟙 Xᘁ
simp only [rightAdjointMate, MonoidalCategory.tensor_id, Category.id_comp,
  coevaluation_evaluation_assoc, Category.comp_id, Iso.inv_hom_id]