-- 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 (α :=
    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) _))))
⊢ 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)ᘁ))
have 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) _))))
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]