-- 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 (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
      η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := 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) _)) (F.map f ⊗ₘ inv (F.map f)ᘁ))
rw₁ :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := 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) _)) (F.map f ⊗ₘ inv (F.map f)ᘁ))
rw₂ :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := 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) _))
      ((𝟙 (F.obj X) ⊗ₘ inv (F.map f)ᘁ) ≫
        (F.map f ⊗ₘ 𝟙 (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))))
rw₃ :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := 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) _))
      (F.obj X ◁ inv (F.map f)ᘁ ≫ (F.map f ⊗ₘ 𝟙 (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))))
rw₄ :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := 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) _))
      (F.obj X ◁ inv (F.map f)ᘁ ≫ F.map f ▷ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
rw₅ :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    (CategoryStruct.comp (Y :=
        tensorObj.{v_1, u_2} (𝒞 := 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) _)) (F.obj X ◁ inv (F.map f)ᘁ) ≫
      F.map f ▷ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)
rw₆ :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    ((η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) ≫
        inv (F.map f) ▷ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) ≫
      F.map f ▷ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)
rw₇ :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    (η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) ≫
      inv (F.map f) ▷ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _ ≫
        F.map f ▷ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)
rw₈ :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    (η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) ≫
      (inv (F.map f) ≫ F.map f) ▷ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)
rw₉ :
  Eq.{v_1 + 1} (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    (η_ (F.obj Y) (@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 Y) _)
rw₁₀ :
  η_ (F.obj Y) (@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 Y) _) ≫
      𝟙 (tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
rw₁₁ rw₁₂ :
  Eq.{v_1 + 1} (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@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 Y) _))
    (η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
⊢ Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
      η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := 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) _)) (F.map f ⊗ₘ F.map (inv f)ᘁ))

Tactic:
rw [Functor.map_inv, Category.id_comp, ← id_tensor_comp_tensor_id,
              id_tensorHom, tensorHom_id, ← Category.assoc,
              coevaluation_comp_rightAdjointMate, Category.assoc, ← comp_whiskerRight,
              IsIso.inv_hom_id, id_whiskerRight, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Functor.map_inv, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.coevaluation_comp_rightAdjointMate, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_comp