-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : C
inst_2 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
inst_4 : HasRightDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
      (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Y
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
            (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷
            tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ◁
            f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
            𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (monoidalComp (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (monoidalComp (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
                Y)
              (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) Y
                (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y))
              (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Y) (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ▷
            @rightDual.{v₁, u₁} _ inst inst_1 X _)
          (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
            𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))))
have rw : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))
  (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
      (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
    (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (monoidalComp (X :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
        (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
      (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Y
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
          (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
      (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
        η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷
          tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
          𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))))
  (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
        (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (monoidalComp (X :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) Y)
            (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y))
            (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Y) (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ▷
          @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
          𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))))
Tactic: rw [← whisker_exchange]