-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.pentagon_inv_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C)
  [inst_3 : X₁.HasTensor X₂] [inst_4 : X₂.HasTensor X₃] [inst_5 : X₃.HasTensor X₄]
  [inst_6 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃]
  [inst_7 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_8 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃).HasTensor X₄]
  [inst_9 : X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_10 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃).HasTensor
      X₄]
  [inst_11 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)).HasTensor
      X₄]
  [inst_12 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄)]
  [inst_13 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))]
  [inst_14 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_15 : X₁.HasGoodTensor₁₂Tensor X₂ X₃] [inst_16 : X₁.HasGoodTensorTensor₂₃ X₂ X₃]
  [inst_17 : X₁.HasGoodTensor₁₂Tensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄]
  [inst_18 : X₁.HasGoodTensorTensor₂₃ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄]
  [inst_19 : X₂.HasGoodTensor₁₂Tensor X₃ X₄] [inst_20 : X₂.HasGoodTensorTensor₂₃ X₃ X₄]
  [inst_21 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄]
  [inst_22 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄]
  [inst_23 : X₁.HasGoodTensor₁₂Tensor X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_24 : X₁.HasGoodTensorTensor₂₃ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [X₁.HasTensor₄ObjExt X₂ X₃ X₄] {Z : CategoryTheory.GradedObject I C}
  (h :
    CategoryTheory.GradedObject.Monoidal.tensorObj
        (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃) X₄ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X₁)
        (CategoryTheory.GradedObject.Monoidal.associator X₂ X₃ X₄).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.associator X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)
            X₄).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).inv
            (CategoryTheory.CategoryStruct.id X₄))
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.associator (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃
            X₄).inv
        h)