-- 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₂ X₃ Y₁ Y₂ Y₃ : C
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst) X₂
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₁) Y₂)
            Y₃)))
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃)))
      (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) X₃ Y₂))
            Y₃))
        (X₁ ◁ X₂ ◁ Iso.hom (β_ X₃ Y₁) ▷ Y₂ ▷ Y₃)
        (X₁ ◁
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁ ◁ Iso.hom (β_ X₃ Y₂) ≫
                Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ X₃) ▷
              Y₃ ⊗≫
          𝟙
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
                (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃))))) =
    (Iso.hom (α_ X₁ X₂ X₃) ⊗ₘ Iso.hom (α_ Y₁ Y₂ Y₃)) ≫
      (Iso.hom
            (α_ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
              (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃))) ≫
          X₁ ◁ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
            X₁ ◁ Iso.hom (β_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃ ≫
              X₁ ◁ Iso.hom (α_ Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
                Iso.inv
                  (α_ X₁ Y₁
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
                      (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)))) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁
          (Iso.hom (α_ X₂ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
            X₂ ◁ Iso.inv (α_ X₃ Y₂ Y₃) ≫
              X₂ ◁ Iso.hom (β_ X₃ Y₂) ▷ Y₃ ≫
                X₂ ◁ Iso.hom (α_ Y₂ X₃ Y₃) ≫ Iso.inv (α_ X₂ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)))
have rw : monoidalComp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁
      (tensorObj.{v₁, u₁} (𝒞 := inst) X₂
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₁) Y₂) Y₃)))
    (𝟙
      (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃)))
    (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) X₃ Y₂))
          Y₃))
      (X₁ ◁ X₂ ◁ Iso.hom (β_ X₃ Y₁) ▷ Y₂ ▷ Y₃)
      (X₁ ◁
          (Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₂ ≫
              tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ X₂ ◁ Iso.hom (β_ X₃ Y₂)) ▷
            Y₃ ⊗≫
        𝟙
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁)
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃))))) =
  (Iso.hom (α_ X₁ X₂ X₃) ⊗ₘ Iso.hom (α_ Y₁ Y₂ Y₃)) ≫
    (Iso.hom
          (α_ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
            (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃))) ≫
        X₁ ◁ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
          X₁ ◁
              (Iso.hom (α_ X₂ X₃ Y₁) ≫
                  X₂ ◁ Iso.hom (β_ X₃ Y₁) ≫ Iso.inv (α_ X₂ Y₁ X₃) ≫ Iso.hom (β_ X₂ Y₁) ▷ X₃ ≫ Iso.hom (α_ Y₁ X₂ X₃)) ▷
                tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃ ≫
            X₁ ◁ Iso.hom (α_ Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
              Iso.inv
                (α_ X₁ Y₁
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
                    (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁
        (Iso.hom (α_ X₂ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
          X₂ ◁ Iso.inv (α_ X₃ Y₂ Y₃) ≫
            X₂ ◁ Iso.hom (β_ X₃ Y₂) ▷ Y₃ ≫
              X₂ ◁ Iso.hom (α_ Y₂ X₃ Y₃) ≫ Iso.inv (α_ X₂ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)))
Tactic: rw [whisker_exchange, braiding_tensor_left_hom]