-- 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
⊢ (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₂))) ▷
        tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ≫
      (Iso.hom
            (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
              (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₁ Z₂) ≫
            tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁
                (Iso.hom (α_ X₂ Y₂ Z₁) ≫
                    X₂ ◁ Iso.hom (β_ Y₂ Z₁) ≫ Iso.inv (α_ X₂ Z₁ Y₂) ≫ Iso.hom (β_ X₂ Z₁) ▷ Y₂ ≫ Iso.hom (α_ Z₁ X₂ Y₂)) ▷
                  Z₂ ≫
              tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁ Iso.hom (α_ Z₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₂) ≫
                Iso.inv
                  (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) Z₁
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₂))) ≫
        (Iso.hom (α_ X₁ Y₁ Z₁) ⊗ₘ Iso.hom (α_ X₂ 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 _ : (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₂))) ▷
      tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ≫
    (Iso.hom
          (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
            (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₁ Z₂) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁
              (Iso.hom (α_ X₂ Y₂ Z₁) ≫
                  X₂ ◁ Iso.hom (β_ Y₂ Z₁) ≫ Iso.inv (α_ X₂ Z₁ Y₂) ≫ Iso.hom (β_ X₂ Z₁) ▷ Y₂ ≫ Iso.hom (α_ Z₁ X₂ Y₂)) ▷
                Z₂ ≫
            tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁ Iso.hom (α_ Z₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₂) ≫
              Iso.inv
                (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) Z₁
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₂))) ≫
      (Iso.hom (α_ X₁ Y₁ Z₁) ⊗ₘ Iso.hom (α_ X₂ Y₂ Z₂)) =
  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₂)))))
Tactic: calc
    _ = 𝟙 _ ⊗≫
      X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 _ := by monoidal
    _ = _ := by rw [← whisker_exchange]; monoidal