-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₁ :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (inv (F.map f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₂ :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      ((𝟙 (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) ⊗ₘ F.map f) ≫
        (inv (F.map f)ᘁ ⊗ₘ 𝟙 (F.obj Y)))
      (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₃ :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    ((𝟙 (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) ⊗ₘ F.map f) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
        (inv (F.map f)ᘁ ⊗ₘ 𝟙 (F.obj Y)) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₄ :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _ ◁ F.map f ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
        (inv (F.map f)ᘁ ⊗ₘ 𝟙 (F.obj Y)) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₅ :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _ ◁ F.map f ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
        (inv (F.map f)ᘁ ▷ F.obj Y) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₆ :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _ ◁ F.map f ≫
      @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _ ◁ inv (F.map f) ≫
        ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₇ :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _ ◁ (F.map f ≫ inv (F.map f)) ≫
      ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₈ :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _ ◁ 𝟙 (F.obj X) ≫
      ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₉ :
  𝟙 (tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X)) ≫
      ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) =
    ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)
rw₁₀ rw₁₁ :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
⊢ Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) ≫
      𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)))

Tactic:
rw [Category.comp_id, Functor.map_inv, ← id_tensor_comp_tensor_id, Category.assoc,
              id_tensorHom, tensorHom_id,
              rightAdjointMate_comp_evaluation, ← MonoidalCategory.whiskerLeft_comp_assoc,
              IsIso.hom_inv_id, MonoidalCategory.whiskerLeft_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id, CategoryTheory.Functor.map_inv, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.rightAdjointMate_comp_evaluation, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_comp