-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₁))
          Z₂))
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂))
          (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Z₁) Y₂)
              Z₂)))
        (X₁ ◁
          (Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₁ ≫
              tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ X₂ ◁ Iso.hom (β_ Y₂ Z₁)) ▷
            Z₂)
        (X₁ ◁ Y₁ ◁ Iso.hom (β_ X₂ Z₁) ▷ Y₂ ▷ Z₂ ⊗≫
          𝟙
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁))
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))))) =
    Iso.hom
        (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)
          (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁
          (Iso.hom (α_ Y₁ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)) ≫
            Y₁ ◁ Iso.inv (α_ Y₂ Z₁ Z₂) ≫
              Y₁ ◁ Iso.hom (β_ Y₂ Z₁) ▷ Z₂ ≫
                Y₁ ◁ Iso.hom (α_ Z₁ Y₂ Z₂) ≫ Iso.inv (α_ Y₁ Z₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))) ≫
        Iso.hom
            (α_ X₁ X₂
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁)
                (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))) ≫
          X₁ ◁ Iso.inv (α_ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)) ≫
            X₁ ◁
                (Iso.inv (α_ X₂ Y₁ Z₁) ≫
                    Iso.hom (β_ X₂ Y₁) ▷ Z₁ ≫ Iso.hom (α_ Y₁ X₂ Z₁) ≫ Y₁ ◁ Iso.hom (β_ X₂ Z₁) ≫ Iso.inv (α_ Y₁ Z₁ X₂)) ▷
                  tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂ ≫
              X₁ ◁ Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)) ≫
                Iso.inv
                  (α_ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁)
                    (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)))
have rw : monoidalComp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁
      (tensorObj.{v₁, u₁} (𝒞 := inst)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₁))
        Z₂))
    (𝟙
      (tensorObj.{v₁, u₁} (𝒞 := inst)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂))
        (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Z₁) Y₂)
            Z₂)))
      (X₁ ◁
        (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁ ◁ Iso.hom (β_ Y₂ Z₁) ≫
            Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Y₂) ▷
          Z₂)
      (X₁ ◁ Y₁ ◁ Iso.hom (β_ X₂ Z₁) ▷ Y₂ ▷ Z₂ ⊗≫
        𝟙
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))))) =
  Iso.hom
      (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)
        (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)) ≫
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁
        (Iso.hom (α_ Y₁ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)) ≫
          Y₁ ◁ Iso.inv (α_ Y₂ Z₁ Z₂) ≫
            Y₁ ◁ Iso.hom (β_ Y₂ Z₁) ▷ Z₂ ≫
              Y₁ ◁ Iso.hom (α_ Z₁ Y₂ Z₂) ≫ Iso.inv (α_ Y₁ Z₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))) ≫
      Iso.hom
          (α_ X₁ X₂
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))) ≫
        X₁ ◁ Iso.inv (α_ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)) ≫
          X₁ ◁
              (Iso.inv (α_ X₂ Y₁ Z₁) ≫
                  Iso.hom (β_ X₂ Y₁) ▷ Z₁ ≫ Iso.hom (α_ Y₁ X₂ Z₁) ≫ Y₁ ◁ Iso.hom (β_ X₂ Z₁) ≫ Iso.inv (α_ Y₁ Z₁ X₂)) ▷
                tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂ ≫
            X₁ ◁ Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)) ≫
              Iso.inv
                (α_ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁)
                  (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)))
Tactic: rw [← whisker_exchange]