-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (goal)
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) _))
⊢ 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)))
have 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) _))
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]