-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
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
| CategoryStruct.comp (Y :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁)
      (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄) (i₂ + i₃ + i₄)))
    (X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ (i₂ + i₃ + i₄) ⋯)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁)
        (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₂ X₃) X₄ (i₂ + i₃ + i₄)))
      (𝟙 X₁ i₁ ⊗ₘ Iso.inv (associator X₂ X₃ X₄) (i₂ + i₃ + i₄))
      (CategoryStruct.comp (Y :=
        tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₂ X₃) X₄) j)
        (ιTensorObj X₁ (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₂ X₃) X₄) i₁ (i₂ + i₃ + i₄) j ⋯)
        (CategoryStruct.comp (Y :=
          tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)) X₄ j)
          (Iso.inv (associator X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) X₄) j)
          (tensorHom (Iso.inv (associator X₁ X₂ X₃)) (𝟙 X₄) j))))
have dsimp : CategoryStruct.comp (Y :=
  MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁)
    (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄) (i₂ + i₃ + i₄)))
  (X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ (i₂ + i₃ + i₄) sorry)
  (CategoryStruct.comp (Y :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁)
      (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₂ X₃) X₄ (i₂ + i₃ + i₄)))
    (𝟙 (X₁ i₁) ⊗ₘ Iso.inv (associator X₂ X₃ X₄) (i₂ + i₃ + i₄))
    (CategoryStruct.comp (Y :=
      tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₂ X₃) X₄) j)
      (ιTensorObj X₁ (tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₂ X₃) X₄) i₁ (i₂ + i₃ + i₄) j sorry)
      (CategoryStruct.comp (Y :=
        tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)) X₄ j)
        (Iso.inv (associator X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) X₄) j)
        (tensorHom (Iso.inv (associator X₁ X₂ X₃)) (𝟙 X₄) j))))
Tactic: dsimp only [categoryOfGradedObjects_id, id_eq, eq_mpr_eq_cast, cast_eq]