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₃ 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₂₃₄
hj : i₁ + i₂ + i₃ + i₄ = j
⊢ X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ 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₂ 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

Tactic:
simpa only [assoc, ιTensorObj₄_eq X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j hj i₂₃₄ h''] using h i₁ i₂ i₃ i₄ hj

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₄_eq
-- 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
⊢ i₁ + (i₂ + i₃) + i₄ = j

Tactic:
simp only [← 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₂ 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
rw rw₁ : i₁ + (i₂ + i₃) = i₁ + (i₂ + i₃)
⊢ i₁ + (i₂ + i₃) = i₁ + i₂ + i₃

Tactic:
rw [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₂ 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 rw : i₁ + i₂ + i₃ + i₄ = j
rw₁ rw₂ : j = j
⊢ i₁ + i₂ + (i₃ + i₄) = j

Tactic:
rw [← 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₂ 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
rw rw₁ : i₂ + (i₃ + i₄) = i₂ + (i₃ + i₄)
⊢ i₂ + (i₃ + i₄) = i₂ + i₃ + i₄

Tactic:
rw [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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
X X' : GradedObject I C
⊢ HasTensor.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X

Tactic:
mapBifunctorLeftUnitor_hasMap _ _ (leftUnitorNatIso C) _ zero_add _

Premises used: CategoryTheory.MonoidalCategory.leftUnitorNatIso, CategoryTheory.GradedObject.mapBifunctorLeftUnitor_hasMap, CategoryTheory.GradedObject.Monoidal.tensorUnit
-- 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
X X' : GradedObject I C
⊢ HasMap.{u, u, v_1, u_1} (J := I)
    (Functor.obj
      (Functor.obj (mapBifunctor (curriedTensor C) I I)
        (Functor.obj (single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst_1))))
      X)
    fun (x : I × I) ↦
    match (motive := I × I → I) x with
    | (i₁, i₂) => i₁ + i₂

Tactic:
inferInstanceAs <| HasTensor tensorUnit X

Premises used: _private.0.CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit._proof_1
-- 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
X : GradedObject I C
i : I
⊢ Eq.{v_1 + 1} (α := X i ⟶ tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X i)
    (Iso.inv (leftUnitor X) i : X i ⟶ tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X i)
    (Iso.inv (λ_ (X i)) ≫ Iso.inv tensorUnit₀ ▷ X i ≫ ιTensorObj tensorUnit.{u, v_1, u_1} X 0 i i ⋯ :
      X i ⟶ tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X i)

Tactic:
rfl

Premises used: CategoryTheory.GradedObject.ιMapBifunctorMapObj, CategoryTheory.GradedObject.mapBifunctorMapObj, CategoryTheory.GradedObject.ιMapObj, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.Monoidal.ιTensorObj, CategoryTheory.GradedObject.mapObj, CategoryTheory.GradedObject.Monoidal.tensorUnit, rfl, CategoryTheory.Limits.colimit.ι
-- 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
X X' : GradedObject I C
φ : X ⟶ X'
⊢ Eq (α := tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X ⟶ X')
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X')
        (tensorHom (𝟙 tensorUnit.{u, v_1, u_1}) φ :
          tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X ⟶ tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X')
        (Iso.hom (leftUnitor X') : tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X' ⟶ X') :
      tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X ⟶ X')
    (Iso.hom (leftUnitor X) ≫ φ : tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X ⟶ X')

Tactic:
apply mapBifunctorLeftUnitor_naturality

Premises used: CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality
-- 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
X X' : GradedObject I C
⊢ HasTensor.{u, v_1, u_1} X tensorUnit.{u, v_1, u_1}

Tactic:
mapBifunctorRightUnitor_hasMap (curriedTensor C) _
    (rightUnitorNatIso C) _ add_zero _

Premises used: CategoryTheory.MonoidalCategory.rightUnitorNatIso, CategoryTheory.GradedObject.mapBifunctorRightUnitor_hasMap, CategoryTheory.GradedObject.Monoidal.tensorUnit, 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
X X' : GradedObject I C
⊢ HasMap.{u, u, v_1, u_1} (J := I)
    (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X)
      (Functor.obj (single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst_1))))
    fun (x : I × I) ↦
    match (motive := I × I → I) x with
    | (i₁, i₂) => i₁ + i₂

Tactic:
inferInstanceAs <| HasTensor X tensorUnit

Premises used: _private.0.CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1._proof_1
-- 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
X : GradedObject I C
i : I
⊢ Eq.{v_1 + 1} (α := X i ⟶ tensorObj.{u, v_1, u_1} X tensorUnit.{u, v_1, u_1} i)
    (Iso.inv (rightUnitor X) i : X i ⟶ tensorObj.{u, v_1, u_1} X tensorUnit.{u, v_1, u_1} i)
    (Iso.inv (ρ_ (X i)) ≫ X i ◁ Iso.inv tensorUnit₀ ≫ ιTensorObj X tensorUnit.{u, v_1, u_1} i 0 i ⋯ :
      X i ⟶ tensorObj.{u, v_1, u_1} X tensorUnit.{u, v_1, u_1} i)

Tactic:
rfl

Premises used: CategoryTheory.GradedObject.ιMapBifunctorMapObj, CategoryTheory.GradedObject.mapBifunctorMapObj, CategoryTheory.GradedObject.ιMapObj, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.Monoidal.ιTensorObj, CategoryTheory.GradedObject.mapObj, CategoryTheory.GradedObject.Monoidal.tensorUnit, rfl, CategoryTheory.Limits.colimit.ι
-- 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
X X' : GradedObject I C
φ : X ⟶ X'
⊢ Eq (α := tensorObj.{u, v_1, u_1} X tensorUnit.{u, v_1, u_1} ⟶ X')
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X' tensorUnit.{u, v_1, u_1})
        (tensorHom φ (𝟙 tensorUnit.{u, v_1, u_1}) :
          tensorObj.{u, v_1, u_1} X tensorUnit.{u, v_1, u_1} ⟶ tensorObj.{u, v_1, u_1} X' tensorUnit.{u, v_1, u_1})
        (Iso.hom (rightUnitor X') : tensorObj.{u, v_1, u_1} X' tensorUnit.{u, v_1, u_1} ⟶ X') :
      tensorObj.{u, v_1, u_1} X tensorUnit.{u, v_1, u_1} ⟶ X')
    (Iso.hom (rightUnitor X) ≫ φ : tensorObj.{u, v_1, u_1} X tensorUnit.{u, v_1, u_1} ⟶ X')

Tactic:
apply mapBifunctorRightUnitor_naturality

Premises used: CategoryTheory.GradedObject.mapBifunctorRightUnitor_naturality
-- 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_6 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
X₁ X₃ : GradedObject I C
inst_7 : HasTensor.{u, v_1, u_1} X₁ X₃
inst_8 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1}) X₃
inst_9 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X₃)
inst_10 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1} X₃
inst_11 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1} X₃
⊢ ∀ (X₁ X₃ : C),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1}
          (Functor.obj (Functor.obj (bifunctorComp₁₂ (curriedTensor C) (curriedTensor C)) X₁)
            (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
          X₃ ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X₃))
      (NatTrans.app
            (NatTrans.app (NatTrans.app (Iso.hom (curriedAssociatorNatIso C)) X₁)
              (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
            X₃ ≫
          Functor.map (Functor.obj (curriedTensor C) X₁) (NatTrans.app (Iso.hom (leftUnitorNatIso C)) X₃) :
        Functor.obj.{v_1, v_1, u_1, u_1}
            (Functor.obj (Functor.obj (bifunctorComp₁₂ (curriedTensor C) (curriedTensor C)) X₁)
              (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
            X₃ ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁)
            (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X₃))
      (NatTrans.app (Functor.map (curriedTensor C) (NatTrans.app (Iso.hom (rightUnitorNatIso C)) X₁)) X₃ :
        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 (Functor.flip (curriedTensor C))
                  (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
                X₁))
            X₃ ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X₁))
            X₃)

Tactic:
simp
-- 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_6 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
X₁ X₃ : GradedObject I C
inst_7 : HasTensor.{u, v_1, u_1} X₁ X₃
inst_8 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1}) X₃
inst_9 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X₃)
inst_10 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1} X₃
inst_11 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1} X₃
convert_3 :
  HasGoodTrifunctor₁₂Obj.{v_1, u_1, v_1, u_1, v_1, u_1, v_1, u_1, v_1, u_1, u, u, u, u, u} (curriedTensor C)
    (curriedTensor C) (r := r₁₂₃) (TriangleIndexData.ρ₁₂ (triangleIndexData I)) X₁
    (Functor.obj (single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) X₃
convert_4 :
  HasGoodTrifunctor₂₃Obj.{v_1, u_1, v_1, u_1, v_1, u_1, v_1, u_1, v_1, u_1, u, u, u, u, u} (curriedTensor C)
    (curriedTensor C) (r := r₁₂₃) (TriangleIndexData.ρ₂₃ (triangleIndexData I)) X₁
    (Functor.obj (single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) X₃
⊢ Eq (α :=
    tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1}) X₃ ⟶ tensorObj.{u, v_1, u_1} X₁ X₃)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X₃))
        (Iso.hom (associator X₁ tensorUnit.{u, v_1, u_1} X₃) :
          tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1}) X₃ ⟶
            tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X₃))
        (tensorHom (𝟙 X₁) (Iso.hom (leftUnitor X₃)) :
          tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X₃) ⟶
            tensorObj.{u, v_1, u_1} X₁ X₃) :
      tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1}) X₃ ⟶ tensorObj.{u, v_1, u_1} X₁ X₃)
    (tensorHom (Iso.hom (rightUnitor X₁)) (𝟙 X₃) :
      tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1}) X₃ ⟶ tensorObj.{u, v_1, u_1} X₁ X₃)

Tactic:
convert!
    mapBifunctor_triangle (curriedAssociatorNatIso C) (𝟙_ C) (rightUnitorNatIso C)
      (leftUnitorNatIso C) (triangleIndexData I) X₁ X₃ (by simp)
-- 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
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
inst_5 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_6 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
X₁ X₃ : GradedObject I C
inst_7 : HasTensor.{u, v_1, u_1} X₁ X₃
inst_8 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1}) X₃
inst_9 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} tensorUnit.{u, v_1, u_1} X₃)
inst_10 : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1} X₃
inst_11 : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ tensorUnit.{u, v_1, u_1} X₃
⊢ HasGoodTrifunctor₁₂Obj.{v_1, u_1, v_1, u_1, v_1, u_1, v_1, u_1, v_1, u_1, u, u, u, u, u} (curriedTensor C)
    (curriedTensor C) (r := r₁₂₃) (TriangleIndexData.ρ₁₂ (triangleIndexData I)) X₁
    (Functor.obj (single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) X₃

Tactic:
assumption