-- Module: Mathlib.CategoryTheory.GradedObject.Monoidal
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ X₄ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
inst_4 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_5 : HasTensor.{u, v_1, u_1} X₃ X₄
inst_6 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃
inst_7 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
inst_8 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₂ X₃) X₄
inst_9 : HasTensor.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_10 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃) X₄
inst_11 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)) X₄
inst_12 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₂ X₃) X₄)
inst_13 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
inst_14 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_15 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ X₂ X₃
inst_16 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
inst_17 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) X₄
inst_18 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) X₄
inst_19 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₂ X₃ X₄
inst_20 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₂ X₃ X₄
inst_21 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ X₄
inst_22 : HasGoodTensorTensor₂₃.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ X₄
inst_23 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_24 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_25 : HasTensor₄ObjExt.{u, v_1, u_1} X₁ X₂ X₃ X₄
j i₁ i₂ i₃ i₄ : I
h : i₁ + i₂ + i₃ + i₄ = j
conv_rhs :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁)
        (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₂ i₂)
          (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₃ i₃) (X₄ i₄))) ⟶
      tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃) X₄ j)
    (Iso.inv (α_ (X₁ i₁) (X₂ i₂) (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₃ i₃) (X₄ i₄))) ≫
      Iso.inv (α_ (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (X₂ i₂)) (X₃ i₃) (X₄ i₄)) ≫
        ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ (i₁ + i₂ + i₃) ⋯ ▷ X₄ i₄ ≫
          ιTensorObj (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃) X₄ (i₁ + i₂ + i₃) i₄ j ⋯)
    (CategoryStruct.comp (Y :=
      tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) j)
      (ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h)
      (CategoryStruct.comp (Y :=
        tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) (tensorObj.{u, v_1, u_1} X₃ X₄) j)
        (Iso.inv (associator X₁ X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) j)
        (Iso.inv (associator (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ X₄) j)))
h₁ :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁)
        (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₂ i₂)
          (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₃ i₃) (X₄ i₄))) ⟶
      tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃) X₄ j)
    (Iso.inv (α_ (X₁ i₁) (X₂ i₂) (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₃ i₃) (X₄ i₄))) ≫
      Iso.inv (α_ (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (X₂ i₂)) (X₃ i₃) (X₄ i₄)) ≫
        ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ (i₁ + i₂ + i₃) ⋯ ▷ X₄ i₄ ≫
          ιTensorObj (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃) X₄ (i₁ + i₂ + i₃) i₄ j ⋯)
    (Iso.inv (α_ (X₁ i₁) (X₂ i₂) (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₃ i₃) (X₄ i₄))) ≫
      Iso.inv (α_ (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (X₂ i₂)) (X₃ i₃) (X₄ i₄)) ≫
        ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ (i₁ + i₂ + i₃) ⋯ ▷ X₄ i₄ ≫
          ιTensorObj (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃) X₄ (i₁ + i₂ + i₃) i₄ j ⋯)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁)
        (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₂ i₂)
          (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₃ i₃) (X₄ i₄))) ⟶
      tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃) X₄ j)
    (Iso.inv (α_ (X₁ i₁) (X₂ i₂) (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₃ i₃) (X₄ i₄))) ≫
      Iso.inv (α_ (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (X₂ i₂)) (X₃ i₃) (X₄ i₄)) ≫
        ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ (i₁ + i₂ + i₃) ⋯ ▷ X₄ i₄ ≫
          ιTensorObj (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃) X₄ (i₁ + i₂ + i₃) i₄ j ⋯)
    (CategoryStruct.comp (Y :=
      tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) j)
      (ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h)
      (CategoryStruct.comp (Y :=
        tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) (tensorObj.{u, v_1, u_1} X₃ X₄) j)
        (Iso.inv (associator X₁ X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) j)
        (Iso.inv (associator (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ X₄) j)))

Tactic:
conv_rhs =>
    rw [ιTensorObj₄_eq X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ _ _ _ rfl,
      ιTensorObj₃_eq X₂ X₃ X₄ i₂ i₃ i₄ _ rfl _ rfl, assoc,
      MonoidalCategory.whiskerLeft_comp_assoc,
      ← ιTensorObj₃_eq_assoc X₁ X₂ (tensorObj X₃ X₄) i₁ i₂ (i₃ + i₄) j
        (by rw [← add_assoc, h]) (i₂ + i₃ + i₄) (by rw [add_assoc]),
      ιTensorObj₃_associator_inv_assoc, associator_inv_naturality_right_assoc,
      ιTensorObj₃'_eq_assoc X₁ X₂ (tensorObj X₃ X₄) i₁ i₂ (i₃ + i₄) j
        (by rw [← add_assoc, h]) _ rfl, whisker_exchange_assoc,
      ← ιTensorObj₃_eq_assoc (tensorObj X₁ X₂) X₃ X₄ (i₁ + i₂) i₃ i₄ j h _ rfl,
      ιTensorObj₃_associator_inv, whiskerRight_tensor_assoc, Iso.hom_inv_id_assoc,
      ιTensorObj₃'_eq (tensorObj X₁ X₂) X₃ X₄ (i₁ + i₂) i₃ i₄ j h _ rfl,
      ← MonoidalCategory.comp_whiskerRight_assoc,
      ← ιTensorObj₃'_eq X₁ X₂ X₃ i₁ i₂ i₃ _ rfl _ rfl]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv_assoc, CategoryTheory.GradedObject.Monoidal.tensorObj, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq, HAdd.hAdd, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₄_eq, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq_assoc, CategoryTheory.MonoidalCategory.whiskerRight_tensor_assoc, rfl