-- 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) _))
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) _))
⊢ 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.{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) _))
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]