awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
inst_3 : ∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p
X₁ X₂ : GradedObject I C₁
φ : X₁ ⟶ X₂
Y₁ Y₂ : GradedObject J C₂
ψ : Y₁ ⟶ Y₂
⊢ Eq (α := mapBifunctorMapObj F p X₁ Y₁ ⟶ mapBifunctorMapObj F p X₂ Y₂)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₂)
      (mapMap (((mapBifunctor F I J).map (𝟙 X₁)).app Y₁ ≫ ((mapBifunctor F I J).obj X₁).map ψ) p)
      (mapMap (((mapBifunctor F I J).map φ).app Y₂ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₂)) p))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₁)
      (mapMap (((mapBifunctor F I J).map φ).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₁)) p)
      (mapMap (((mapBifunctor F I J).map (𝟙 X₂)).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map ψ) p))

Tactic:
simp only [Functor.map_id, NatTrans.id_app, id_comp, comp_id,
          ← mapMap_comp, NatTrans.naturality]

Premises used: CategoryTheory.GradedObject.mapMap_comp, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.id_app, CategoryTheory.Category.id_comp
-- 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₂ Y₁ Y₂ : GradedObject I C
e₁ : X₁ ≅ Y₁
e₂ : X₂ ≅ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
e : Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂ ≅
  Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) Y₁) Y₂ :=
  (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).isoMk
    (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) Y₁) Y₂) fun (x : I × I) ↦
    match (motive :=
      (x : I × I) →
        Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂ x ≅
          Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) Y₁) Y₂ x)
      x with
    | (i, j) => Functor.mapIso (eval i) e₁ ⊗ᵢ Functor.mapIso (eval j) e₂
⊢ HasTensor.{u, v_1, u_1} Y₁ Y₂

Tactic:
hasMap_of_iso e _

Premises used: CategoryTheory.GradedObject.hasMap_of_iso
-- 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₂ Y₁ Y₂ : GradedObject I C
e₁ : X₁ ≅ Y₁
e₂ : X₂ ≅ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
e : Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂ ≅
  Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) Y₁) Y₂ :=
  (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).isoMk
    (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) Y₁) Y₂) fun (x : I × I) ↦
    match (motive :=
      (x : I × I) →
        Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂ x ≅
          Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) Y₁) Y₂ x)
      x with
    | (i, j) => Functor.mapIso (eval i) e₁ ⊗ᵢ Functor.mapIso (eval j) e₂
⊢ HasTensor.{u, v_1, u_1} Y₁ Y₂

Tactic:
exact hasMap_of_iso e _

Premises used: CategoryTheory.GradedObject.hasMap_of_iso
-- 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₂ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
A : C
j : I
f g : tensorObj.{u, v_1, u_1} X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
hfg :
  ∀ (i : I × I)
    (hij :
      (match (motive := I × I → I) i with
        | (i, j) => i + j) =
        j),
    (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).ιMapObj
          (fun (x : I × I) ↦
            match (motive := I × I → I) x with
            | (i, j) => i + j)
          i j hij ≫
        f =
      (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).ιMapObj
          (fun (x : I × I) ↦
            match (motive := I × I → I) x with
            | (i, j) => i + j)
          i j hij ≫
        g
⊢ f = g

Tactic:
apply mapObj_ext

Premises used: CategoryTheory.GradedObject.mapObj_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₂ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
A : C
j : I
f g : tensorObj.{u, v_1, u_1} X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
i₁ i₂ : I
hi :
  (match (motive := I × I → I) (i₁, i₂) with
    | (i, j) => i + j) =
    j
⊢ Eq (α := Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂ (i₁, i₂) ⟶ A)
    ((Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).ιMapObj
        (fun (x : I × I) ↦
          match (motive := I × I → I) x with
          | (i, j) => i + j)
        (i₁, i₂) j hi ≫
      f)
    ((Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).ιMapObj
        (fun (x : I × I) ↦
          match (motive := I × I → I) x with
          | (i, j) => i + j)
        (i₁, i₂) j hi ≫
      g)

Tactic:
h i₁ i₂ hi

Premises used: CategoryTheory.GradedObject.ιMapBifunctorMapObj, CategoryTheory.GradedObject.mapBifunctorMapObj, 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₂ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
A : C
j : I
f g : tensorObj.{u, v_1, u_1} X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
i₁ i₂ : I
hi :
  (match (motive := I × I → I) (i₁, i₂) with
    | (i, j) => i + j) =
    j
⊢ Eq (α := Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂ (i₁, i₂) ⟶ A)
    ((Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).ιMapObj
        (fun (x : I × I) ↦
          match (motive := I × I → I) x with
          | (i, j) => i + j)
        (i₁, i₂) j hi ≫
      f)
    ((Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).ιMapObj
        (fun (x : I × I) ↦
          match (motive := I × I → I) x with
          | (i, j) => i + j)
        (i₁, i₂) j hi ≫
      g)

Tactic:
exact h 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₂ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
A : C
k : I
f : (i₁ i₂ : I) → i₁ + i₂ = k → (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (X₂ i₂) ⟶ A)
i₁ i₂ : I
hi : i₁ + i₂ = k
⊢ CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ X₂ k) (ιTensorObj X₁ X₂ i₁ i₂ k hi) (tensorObjDesc f) =
    f i₁ i₂ hi

Tactic:
apply ι_mapBifunctorMapObjDesc

Premises used: CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc
-- 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₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
i₁ i₂ i₁₂ : I
h : i₁ + i₂ = i₁₂
rw :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (Y₁ i₂) ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂ i₁₂)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ i₁₂) (ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h) (tensorHom f g i₁₂))
    (f i₁ ▷ Y₁ i₂ ≫ X₂ i₁ ◁ g i₂ ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (Y₁ i₂) ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂ i₁₂)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ i₁₂) (ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h) (tensorHom f g i₁₂))
    ((f i₁ ⊗ₘ g i₂) ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)

Tactic:
rw [tensorHom_def, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.tensorHom_def
-- 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₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
i₁ i₂ i₁₂ : I
h : i₁ + i₂ = i₁₂
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (Y₁ i₂) ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂ i₁₂)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ i₁₂) (ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h) (tensorHom f g i₁₂))
    (f i₁ ▷ Y₁ i₂ ≫ X₂ i₁ ◁ g i₂ ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)

Tactic:
apply ι_mapBifunctorMapMap

Premises used: CategoryTheory.GradedObject.ι_mapBifunctorMapMap
-- 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 Y : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X Y
simp :
  Eq (α := tensorObj.{u, v_1, u_1} X Y ⟶ tensorObj.{u, v_1, u_1} X Y)
    (𝟙
      (mapObj.{u, u, v_1, u_1} (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X) Y) fun (x : I × I) ↦
        x.1 + x.2))
    (𝟙 (tensorObj.{u, v_1, u_1} X Y))
⊢ (mapMap
      (NatTrans.app (Functor.map (mapBifunctor (curriedTensor C) I I) (𝟙 X)) Y ≫
        Functor.map (Functor.obj (mapBifunctor (curriedTensor C) I I) X) (𝟙 Y))
      fun (x : I × I) ↦ x.1 + x.2) =
    𝟙 (tensorObj.{u, v_1, u_1} X Y)

Tactic:
simp only [Functor.map_id, NatTrans.id_app, comp_id, mapMap_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.GradedObject.mapMap_id, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app
-- 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 Y : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X Y
⊢ Eq (α := tensorObj.{u, v_1, u_1} X Y ⟶ tensorObj.{u, v_1, u_1} X Y)
    (𝟙
      (mapObj.{u, u, v_1, u_1} (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X) Y) fun (x : I × I) ↦
        x.1 + x.2))
    (𝟙 (tensorObj.{u, v_1, u_1} X Y))

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₃ Y₁ Y₂ Y₃ : GradedObject I C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
inst_5 : HasTensor.{u, v_1, u_1} X₃ Y₃
h :
  ∀ (x i₁ i₂ : I) (hi : i₁ + i₂ = x),
    Eq (α :=
      MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (Y₁ i₂) ⟶ tensorObj.{u, v_1, u_1} X₃ Y₃ x)
      (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ x) (ιTensorObj X₁ Y₁ i₁ i₂ x hi)
        (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f₁ g₁) (tensorHom f₂ g₂) x))
      (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ x) (ιTensorObj X₁ Y₁ i₁ i₂ x hi)
        (tensorHom (f₁ ≫ f₂) (g₁ ≫ g₂) x))
⊢ Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₃ Y₃)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f₁ g₁) (tensorHom f₂ g₂))
    (tensorHom (f₁ ≫ f₂) (g₁ ≫ g₂))

Tactic:
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₃ Y₁ Y₂ Y₃ : GradedObject I C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
inst_5 : HasTensor.{u, v_1, u_1} X₃ Y₃
x i₁ i₂ : I
hi : i₁ + i₂ = x
⊢ Eq (α := MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (Y₁ i₂) ⟶ tensorObj.{u, v_1, u_1} X₃ Y₃ x)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ x) (ιTensorObj X₁ Y₁ i₁ i₂ x hi)
      (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f₁ g₁) (tensorHom f₂ g₂) x))
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ x) (ιTensorObj X₁ Y₁ i₁ i₂ x hi)
      (tensorHom (f₁ ≫ f₂) (g₁ ≫ g₂) 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
X₁ X₂ Y₁ Y₂ : GradedObject I C
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
⊢ CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom e.hom e'.hom) (tensorHom e.inv e'.inv) =
    𝟙 (tensorObj.{u, v_1, u_1} X₁ Y₁)

Tactic:
simp [tensorHom_comp_tensorHom]

Premises used: CategoryTheory.GradedObject.Monoidal.tensorHom_comp_tensorHom
-- 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₂ Y₁ Y₂ : GradedObject I C
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
⊢ CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁) (tensorHom e.inv e'.inv) (tensorHom e.hom e'.hom) =
    𝟙 (tensorObj.{u, v_1, u_1} X₂ Y₂)

Tactic:
simp [tensorHom_comp_tensorHom]

Premises used: CategoryTheory.GradedObject.Monoidal.tensorHom_comp_tensorHom
-- 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₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
inst_5 : HasTensor.{u, v_1, u_1} X₂ Y₁
rw :
  Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g)
    (tensorHom (f ≫ 𝟙 X₂) (𝟙 Y₁ ≫ g))
rw₁ : Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g) (tensorHom (f ≫ 𝟙 X₂) g)
rw₂ rw₃ : Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g) (tensorHom f g)
⊢ Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₁) (whiskerRight f Y₁) (whiskerLeft X₂ g))

Tactic:
rw [tensorHom_comp_tensorHom, id_comp, comp_id]

Premises used: CategoryTheory.GradedObject.Monoidal.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- 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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : 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} Y₂ Y₃
inst_6 : HasTensor.{u, v_1, u_1} Y₁ (tensorObj.{u, v_1, u_1} Y₂ Y₃)
i₁ i₂ i₃ j : I
h rw : i₁ + i₂ + i₃ = j
rw₁ rw₂ : j = j
⊢ 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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : 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} Y₂ Y₃
inst_6 : HasTensor.{u, v_1, u_1} Y₁ (tensorObj.{u, v_1, u_1} Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
rw : i₁ + (i₂ + i₃) = j
rw₁ : i₁ + i₂ + i₃ = j
rw₂ rw₃ : j = j
⊢ i₁ + i₂₃ = j

Tactic:
rw [← h', ← 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₃ : 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₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : 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₂) (X₃ i₃)) ⟶
      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)
    (X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ≫ ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) 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} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j)
    (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h' ≫ ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) i₁ i₂₃ j ⋯)

Tactic:
subst h'
-- 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₃)
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} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j)
    (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ≫ ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) 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₃ : 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 : C
f g : 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₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ 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) (X₁ i₁))
          (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X₂ i₂)) (X₃ i₃)) ⟶
        A)
      (ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f)
      (ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g)
⊢ f = g

Tactic:
apply mapBifunctorBifunctor₂₃MapObj_ext (H := H)

Premises used: CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_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} 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₂ X₃) j ⟶ A
H : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ 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) (X₁ i₁))
        (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X₂ i₂)) (X₃ i₃)) ⟶
      A)
    (ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f)
    (ιMapBifunctorBifunctor₂₃MapObj (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.ιMapBifunctorBifunctor₂₃MapObj, 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} 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₂ X₃) j ⟶ A
H : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ 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) (X₁ i₁))
        (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X₂ i₂)) (X₃ i₃)) ⟶
      A)
    (ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f)
    (ιMapBifunctorBifunctor₂₃MapObj (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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : 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} Y₁ Y₂
inst_6 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} Y₁ Y₂) Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
rw : i₁ + i₂ + i₃ = j
rw₁ rw₂ : j = j
⊢ i₁₂ + i₃ = j

Tactic:
rw [← h', h]
-- 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₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
subst :
  Eq (α :=
    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} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ j)
    (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ X₃ i₃ ≫ ιTensorObj (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ (i₁ + i₂) i₃ j ⋯)
⊢ Eq (α :=
    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} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ j)
    (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h' ▷ X₃ i₃ ≫ ιTensorObj (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ i₁₂ i₃ j ⋯)

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

Tactic:
rfl