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