-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y X
inst_6 : HasTensor.{u_1, v_1, u_2} Y Z
inst_7 : HasTensor.{u_1, v_1, u_2} Z X
inst_8 : HasTensor.{u_1, v_1, u_2} X Z
inst_9 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z
inst_10 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Y Z)
inst_11 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y Z) X
inst_12 : HasTensor.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} Z X)
inst_13 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y X) Z
inst_14 : HasTensor.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} X Z)
inst_15 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Y Z
inst_16 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Y Z
inst_17 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Y Z X
inst_18 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Y Z X
inst_19 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Y X Z
inst_20 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Y X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
conv_rhs :
  Eq.{v_1 + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_2} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v_1, u_2} (𝒞 := inst_1) (X i₁) (Y i₂)) (Z i₃) ⟶
      tensorObj.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} Z X) k)
    (MonoidalCategoryStruct.whiskerRight (Iso.hom (β_ (X i₁) (Y i₂))) (Z i₃) ≫
      Iso.hom (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)) ≫
        MonoidalCategoryStruct.whiskerLeft (Y i₂) (Iso.hom (β_ (X i₁) (Z i₃))) ≫ ιTensorObj₃ Y Z X i₂ i₃ i₁ k ⋯)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z k)
      (ιTensorObj₃' X Y Z i₁ i₂ i₃ k h)
      (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y X) Z k)
        (whiskerRight
          (fun (k : I) ↦
            tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (X i) (Y j)) ≫ ιTensorObj Y X j i k ⋯)
          Z k)
        (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} X Z) k)
          (Iso.hom (associator Y X Z) k)
          (whiskerLeft Y
            (fun (k : I) ↦
              tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (X i) (Z j)) ≫ ιTensorObj Z X j i k ⋯)
            k))))
h₁ :
  Eq.{v_1 + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_2} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v_1, u_2} (𝒞 := inst_1) (X i₁) (Y i₂)) (Z i₃) ⟶
      tensorObj.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} Z X) k)
    (MonoidalCategoryStruct.whiskerRight (Iso.hom (β_ (X i₁) (Y i₂))) (Z i₃) ≫
      Iso.hom (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)) ≫
        MonoidalCategoryStruct.whiskerLeft (Y i₂) (Iso.hom (β_ (X i₁) (Z i₃))) ≫ ιTensorObj₃ Y Z X i₂ i₃ i₁ k ⋯)
    (MonoidalCategoryStruct.whiskerRight (Iso.hom (β_ (X i₁) (Y i₂))) (Z i₃) ≫
      Iso.hom (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)) ≫
        MonoidalCategoryStruct.whiskerLeft (Y i₂) (Iso.hom (β_ (X i₁) (Z i₃))) ≫ ιTensorObj₃ Y Z X i₂ i₃ i₁ k ⋯)
⊢ Eq.{v_1 + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_2} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v_1, u_2} (𝒞 := inst_1) (X i₁) (Y i₂)) (Z i₃) ⟶
      tensorObj.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} Z X) k)
    (MonoidalCategoryStruct.whiskerRight (Iso.hom (β_ (X i₁) (Y i₂))) (Z i₃) ≫
      Iso.hom (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)) ≫
        MonoidalCategoryStruct.whiskerLeft (Y i₂) (Iso.hom (β_ (X i₁) (Z i₃))) ≫ ιTensorObj₃ Y Z X i₂ i₃ i₁ k ⋯)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z k)
      (ιTensorObj₃' X Y Z i₁ i₂ i₃ k h)
      (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y X) Z k)
        (whiskerRight
          (fun (k : I) ↦
            tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (X i) (Y j)) ≫ ιTensorObj Y X j i k ⋯)
          Z k)
        (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} X Z) k)
          (Iso.hom (associator Y X Z) k)
          (whiskerLeft Y
            (fun (k : I) ↦
              tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (X i) (Z j)) ≫ ιTensorObj Z X j i k ⋯)
            k))))

Tactic:
conv_rhs => rw [ιTensorObj₃'_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc, ι_tensorHom_assoc,
    ← MonoidalCategory.tensorHom_id,
    MonoidalCategory.tensorHom_comp_tensorHom_assoc, id_comp, ι_tensorObjDesc,
    categoryOfGradedObjects_id, MonoidalCategory.comp_tensor_id, assoc,
    MonoidalCategory.tensorHom_id, MonoidalCategory.tensorHom_id,
    ← ιTensorObj₃'_eq_assoc Y X Z i₂ i₁ i₃ k
      (by rw [add_comm i₂ i₁, h]) (i₁ + i₂) (add_comm i₂ i₁),
    ιTensorObj₃'_associator_hom_assoc,
    ιTensorObj₃_eq Y X Z i₂ i₁ i₃ k (by rw [add_comm i₂ i₁, h]) _ rfl, assoc,
    ι_tensorHom, categoryOfGradedObjects_id, ← MonoidalCategory.tensorHom_id,
    ← MonoidalCategory.id_tensorHom,
    ← MonoidalCategory.id_tensor_comp_assoc,
    ι_tensorObjDesc, MonoidalCategory.id_tensor_comp, assoc,
    ← MonoidalCategory.id_tensor_comp_assoc, MonoidalCategory.tensorHom_id,
    MonoidalCategory.id_tensorHom, MonoidalCategory.whiskerLeft_comp, assoc,
    ← ιTensorObj₃_eq Y Z X i₂ i₃ i₁ k (by rw [add_comm _ i₁, ← add_assoc, h])
      (i₁ + i₃) (add_comm _ _)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.id_tensor_comp_assoc, CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc, add_comm, CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq, HAdd.hAdd, CategoryTheory.MonoidalCategory.comp_tensor_id, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq, CategoryTheory.GradedObject.Monoidal.ι_tensorHom_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom_assoc, CategoryTheory.GradedObject.Monoidal.ι_tensorHom, rfl, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.MonoidalCategory.id_tensor_comp, CategoryTheory.Category.id_comp