awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
inst_4 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃
j : I
A : C
f g : tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ j ⟶ A
H : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
apply :
  ∀ (i₁ i₂ i₃ : I) (h : r₁₂₃ (i₁, i₂, i₃) = j),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1}
          (Functor.obj (curriedTensor C)
            (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X₁ i₁)) (X₂ i₂)))
          (X₃ i₃) ⟶
        A)
      (ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f)
      (ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g)
⊢ f = g

Tactic:
apply mapBifunctor₁₂BifunctorMapObj_ext (H := H)

Premises used: CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext
-- 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₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
inst_4 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃
j : I
A : C
f g : tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ j ⟶ A
H : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
i₁ i₂ i₃ : I
hi : r₁₂₃ (i₁, i₂, i₃) = j
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (curriedTensor C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X₁ i₁)) (X₂ i₂)))
        (X₃ i₃) ⟶
      A)
    (ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f)
    (ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g)

Tactic:
h i₁ i₂ i₃ hi

Premises used: CategoryTheory.GradedObject.Monoidal.ιTensorObj₃', CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj, CategoryTheory.GradedObject.Monoidal.ιTensorObj
-- 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₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
inst_4 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃
j : I
A : C
f g : tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ j ⟶ A
H : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
i₁ i₂ i₃ : I
hi : r₁₂₃ (i₁, i₂, i₃) = j
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (curriedTensor C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X₁ i₁)) (X₂ i₂)))
        (X₃ i₃) ⟶
      A)
    (ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f)
    (ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g)

Tactic:
exact h i₁ i₂ i₃ hi
-- 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₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
inst_4 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃
inst_5 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_6 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
inst_7 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ X₂ X₃
inst_8 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ Eq.{v_1 + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (X₂ i₂)) (X₃ i₃) ⟶
      tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ j)
      (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) (Iso.hom (associator X₁ X₂ X₃) j))
    (Iso.hom (α_ (X₁ i₁) (X₂ i₂) (X₃ i₃)) ≫ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)

Tactic:
ι_mapBifunctorAssociator_hom (MonoidalCategory.curriedAssociatorNatIso C)
    ρ₁₂ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h

Premises used: CategoryTheory.GradedObject.Monoidal.ρ₂₃, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃', CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj, CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom, CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj, CategoryTheory.GradedObject.Monoidal.ιTensorObj, CategoryTheory.GradedObject.Monoidal.ρ₁₂, CategoryTheory.MonoidalCategory.curriedAssociatorNatIso
-- 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₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
inst_4 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃
inst_5 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_6 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
inst_7 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ X₂ X₃
inst_8 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ Eq.{v_1 + 1} (α :=
    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} X₁ X₂) X₃ j)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j)
      (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (Iso.inv (associator X₁ X₂ X₃) j))
    (Iso.inv (α_ (X₁ i₁) (X₂ i₂) (X₃ i₃)) ≫ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)

Tactic:
ι_mapBifunctorAssociator_inv (MonoidalCategory.curriedAssociatorNatIso C)
    ρ₁₂ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h

Premises used: CategoryTheory.GradedObject.Monoidal.ρ₂₃, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃', CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj, CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj, CategoryTheory.GradedObject.Monoidal.ιTensorObj, CategoryTheory.GradedObject.Monoidal.ρ₁₂, CategoryTheory.MonoidalCategory.curriedAssociatorNatIso, CategoryTheory.GradedObject.ι_mapBifunctorAssociator_inv
-- 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₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
j : I
A Z : C
f g :
  MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) Z
      (tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j) ⟶
    A
H : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
hZ : HasLeftTensor₃ObjExt.{u, v_1, u_1} Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
⊢ f = g

Tactic:
(@isColimitOfPreserves C _ C _ _ _ _ ((curriedTensor C).obj Z) _
      (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj (H := H) (j := j)) hZ).hom_ext ?_

Premises used: CategoryTheory.GradedObject.mapBifunctorMapObj, CategoryTheory.Limits.IsColimit.hom_ext, setOf, CategoryTheory.Discrete.functor, CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj, CategoryTheory.Limits.colimit, Set.preimage, CategoryTheory.GradedObject.mapObj, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.MonoidalCategory.curriedTensor
-- 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₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
j : I
A Z : C
f g :
  MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) Z
      (tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j) ⟶
    A
H : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
hZ : HasLeftTensor₃ObjExt.{u, v_1, u_1} Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
refine :
  ∀ (j_1 : Discrete (↑(r₁₂₃ ⁻¹' {j}) : Type u)),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{u, v_1, u, u_1}
          (Discrete.functor
              ((Functor.obj
                    (Functor.obj
                      (Functor.obj (mapTrifunctor (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)) I I I) X₁) X₂)
                    X₃).mapObjFun
                r₁₂₃ j) ⋙
            Functor.obj (curriedTensor C) Z)
          j_1 ⟶
        A)
      (NatTrans.app
          (Cocone.ι
            (Functor.mapCocone (Functor.obj (curriedTensor C) Z)
              (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)))
          j_1 ≫
        f)
      (NatTrans.app
          (Cocone.ι
            (Functor.mapCocone (Functor.obj (curriedTensor C) Z)
              (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)))
          j_1 ≫
        g)
⊢ f = g

Tactic:
refine (@isColimitOfPreserves C _ C _ _ _ _ ((curriedTensor C).obj Z) _
      (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj (H := H) (j := j)) hZ).hom_ext ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.MonoidalCategory.curriedTensor
-- 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₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
j : I
A Z : C
f g :
  MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) Z
      (tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j) ⟶
    A
H : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
hZ : HasLeftTensor₃ObjExt.{u, v_1, u_1} Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
i₁ i₂ i₃ : I
hi : Membership.mem (γ := Set (I × I × I)) (r₁₂₃ ⁻¹' {j}) (i₁, i₂, i₃)
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{u, v_1, u, u_1}
        (Discrete.functor
            ((Functor.obj
                  (Functor.obj
                    (Functor.obj (mapTrifunctor (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)) I I I) X₁) X₂)
                  X₃).mapObjFun
              r₁₂₃ j) ⋙
          Functor.obj (curriedTensor C) Z)
        {
          as :=
            Subtype.mk (p := fun (x : I × I × I) ↦ Membership.mem (γ := Set (I × I × I)) (r₁₂₃ ⁻¹' {j}) x) (i₁, i₂, i₃)
              hi :
          Discrete (↑(r₁₂₃ ⁻¹' {j}) : Type u) } ⟶
      A)
    (NatTrans.app
        (Cocone.ι
          (Functor.mapCocone (Functor.obj (curriedTensor C) Z)
            (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)))
        {
          as :=
            Subtype.mk (p := fun (x : I × I × I) ↦ Membership.mem (γ := Set (I × I × I)) (r₁₂₃ ⁻¹' {j}) x) (i₁, i₂, i₃)
              hi } ≫
      f)
    (NatTrans.app
        (Cocone.ι
          (Functor.mapCocone (Functor.obj (curriedTensor C) Z)
            (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)))
        {
          as :=
            Subtype.mk (p := fun (x : I × I × I) ↦ Membership.mem (γ := Set (I × I × I)) (r₁₂₃ ⁻¹' {j}) x) (i₁, i₂, i₃)
              hi } ≫
      g)

Tactic:
h _ _ _ hi

Premises used: CategoryTheory.GradedObject.mapBifunctorMapObj, setOf, CategoryTheory.Discrete.functor, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj, CategoryTheory.GradedObject.Monoidal.ιTensorObj, Set.preimage, CategoryTheory.GradedObject.mapObj
-- 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₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
j : I
A Z : C
f g :
  MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) Z
      (tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j) ⟶
    A
H : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
hZ : HasLeftTensor₃ObjExt.{u, v_1, u_1} Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
i₁ i₂ i₃ : I
hi : Membership.mem (γ := Set (I × I × I)) (r₁₂₃ ⁻¹' {j}) (i₁, i₂, i₃)
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{u, v_1, u, u_1}
        (Discrete.functor
            ((Functor.obj
                  (Functor.obj
                    (Functor.obj (mapTrifunctor (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)) I I I) X₁) X₂)
                  X₃).mapObjFun
              r₁₂₃ j) ⋙
          Functor.obj (curriedTensor C) Z)
        {
          as :=
            Subtype.mk (p := fun (x : I × I × I) ↦ Membership.mem (γ := Set (I × I × I)) (r₁₂₃ ⁻¹' {j}) x) (i₁, i₂, i₃)
              hi :
          Discrete (↑(r₁₂₃ ⁻¹' {j}) : Type u) } ⟶
      A)
    (NatTrans.app
        (Cocone.ι
          (Functor.mapCocone (Functor.obj (curriedTensor C) Z)
            (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)))
        {
          as :=
            Subtype.mk (p := fun (x : I × I × I) ↦ Membership.mem (γ := Set (I × I × I)) (r₁₂₃ ⁻¹' {j}) x) (i₁, i₂, i₃)
              hi } ≫
      f)
    (NatTrans.app
        (Cocone.ι
          (Functor.mapCocone (Functor.obj (curriedTensor C) Z)
            (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)))
        {
          as :=
            Subtype.mk (p := fun (x : I × I × I) ↦ Membership.mem (γ := Set (I × I × I)) (r₁₂₃ ⁻¹' {j}) x) (i₁, i₂, i₃)
              hi } ≫
      g)

Tactic:
exact h _ _ _ hi
-- 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₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
rw : i₁ + (i₂ + i₃ + i₄) = i₁ + i₂ + i₃ + i₄
rw₁ : i₁ + (i₂ + i₃) + i₄ = i₁ + i₂ + i₃ + i₄
rw₂ rw₃ : i₁ + i₂ + i₃ + i₄ = i₁ + i₂ + i₃ + i₄
⊢ i₁ + (i₂ + i₃ + i₄) = j

Tactic:
rw [← h, ← add_assoc, ← add_assoc]

Premises used: add_assoc
-- 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₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
rw : i₁ + (i₂ + i₃ + i₄) = j
rw₁ : i₁ + (i₂ + i₃) + i₄ = j
rw₂ : i₁ + i₂ + i₃ + i₄ = j
rw₃ rw₄ : j = j
⊢ i₁ + i₂₃₄ = j

Tactic:
rw [← hi, ← add_assoc, ← add_assoc, h]

Premises used: add_assoc
-- 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₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
subst :
  Eq.{v_1 + 1} (α :=
    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} 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)
    (X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ (i₂ + i₃ + i₄) ⋯ ≫
      ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) i₁ (i₂ + i₃ + i₄) j ⋯)
⊢ Eq.{v_1 + 1} (α :=
    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} 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)
    (X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ hi ≫
      ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) i₁ i₂₃₄ j ⋯)

Tactic:
subst hi
-- 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₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ Eq.{v_1 + 1} (α :=
    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} 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)
    (X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ (i₂ + i₃ + i₄) ⋯ ≫
      ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) i₁ (i₂ + i₃ + i₄) j ⋯)

Tactic:
rfl
-- 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₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
j : I
A : C
f g : tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) j ⟶ A
inst_6 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₂ X₃ X₄
H : HasTensor₄ObjExt.{u, v_1, u_1} X₁ X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
h₁ :
  ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j),
    ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) i₁ i₂ j hi ≫ f =
      ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) i₁ i₂ j hi ≫ g
⊢ f = g

Tactic:
apply tensorObj_ext

Premises used: CategoryTheory.GradedObject.Monoidal.tensorObj_ext
-- 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₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
j : I
A : C
f g : tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) j ⟶ A
inst_6 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₂ X₃ X₄
H : HasTensor₄ObjExt.{u, v_1, u_1} X₁ X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
h₁ :
  ∀ (i₁_1 i₂ i₃ : I) (h : i₁_1 + i₂ + i₃ = i₂₃₄),
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₁_1 i₂ i₃ i₂₃₄ h ≫
        ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
      X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₁_1 i₂ i₃ i₂₃₄ h ≫
        ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) i₁ i₂₃₄ j h' ≫ g
⊢ ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
    ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) i₁ i₂₃₄ j h' ≫ g

Tactic:
apply left_tensor_tensorObj₃_ext

Premises used: CategoryTheory.GradedObject.Monoidal.left_tensor_tensorObj₃_ext
-- 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₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
j : I
A : C
f g : tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) j ⟶ A
inst_6 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₂ X₃ X₄
H : HasTensor₄ObjExt.{u, v_1, u_1} X₁ X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ i₄ : I
h'' : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + i₂ + i₃ + i₄ = j

Tactic:
simp only [← h', ← h'', add_assoc]

Premises used: add_assoc
-- 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₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
j : I
A : C
f g : tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)) j ⟶ A
inst_6 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₂ X₃ X₄
H : HasTensor₄ObjExt.{u, v_1, u_1} X₁ X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ i₄ : I
h'' : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + i₂ + i₃ + i₄ = j

Tactic:
have hj : i₁ + i₂ + i₃ + i₄ = j := by simp only [← h', ← h'', add_assoc]