-- 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 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
inst_4 : HasLeftDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) Y))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ◁
            η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f) ▷
            tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y)
        (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ Y ⊗≫
          @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g)))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f)
        (monoidalComp (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y))
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁
            (Y ◁ η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ⊗≫ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ Y))
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g))))
have rw : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
  (monoidalComp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
      (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) Y))
      ((@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Y ◁
          η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y)
      (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ Y ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g)))
  (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
    (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
        (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f)
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y))
        (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁
          (Y ◁ η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ⊗≫ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ Y))
        (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g))))
Tactic: rw [whisker_exchange]