awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} Y Z
inst_5 : HasTensor.{u_1, v_1, u_2} Z Y
inst_6 : HasTensor.{u_1, v_1, u_2} X Z
inst_7 : HasTensor.{u_1, v_1, u_2} Z X
f : X ⟶ Y
dsimp :
  Eq (α := tensorObj.{u_1, v_1, u_2} X Z ⟶ tensorObj.{u_1, v_1, u_2} Z Y)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y Z) (whiskerRight f Z) fun (k : I) ↦
      tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (Y i) (Z j)) ≫ ιTensorObj Z Y j i k ⋯)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Z X)
      (fun (k : I) ↦ tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (X i) (Z j)) ≫ ιTensorObj Z X j i k ⋯)
      (whiskerLeft Z f))
⊢ Eq (α := tensorObj.{u_1, v_1, u_2} X Z ⟶ tensorObj.{u_1, v_1, u_2} Z Y)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y Z) (whiskerRight f Z) (Iso.hom (braiding Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Z X) (Iso.hom (braiding X Z)) (whiskerLeft Z f))

Tactic:
dsimp [braiding]

Premises used: CategoryTheory.GradedObject.Monoidal.braiding
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y X
inst_6 : HasTensor.{u_1, v_1, u_2} Y Z
inst_7 : HasTensor.{u_1, v_1, u_2} Z X
inst_8 : HasTensor.{u_1, v_1, u_2} X Z
inst_9 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z
inst_10 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Y Z)
inst_11 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y Z) X
inst_12 : HasTensor.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} Z X)
inst_13 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y X) Z
inst_14 : HasTensor.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} X Z)
inst_15 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Y Z
inst_16 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Y Z
inst_17 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Y Z X
inst_18 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Y Z X
inst_19 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Y X Z
inst_20 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Y X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
rw : i₁ + (i₂ + i₃) = k
rw₁ : i₁ + i₂ + i₃ = k
rw₂ rw₃ : k = k
⊢ i₂ + i₃ + i₁ = k

Tactic:
rw [add_comm _ i₁, ← add_assoc, h]

Premises used: add_assoc, add_comm
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y X
inst_6 : HasTensor.{u_1, v_1, u_2} Y Z
inst_7 : HasTensor.{u_1, v_1, u_2} Z X
inst_8 : HasTensor.{u_1, v_1, u_2} X Z
inst_9 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z
inst_10 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Y Z)
inst_11 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y Z) X
inst_12 : HasTensor.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} Z X)
inst_13 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y X) Z
inst_14 : HasTensor.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} X Z)
inst_15 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Y Z
inst_16 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Y Z
inst_17 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Y Z X
inst_18 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Y Z X
inst_19 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Y X Z
inst_20 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Y X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
rw :
  MonoidalCategoryStruct.whiskerRight (Iso.hom (β_ (X i₁) (Y i₂))) (Z i₃) ≫
    Iso.hom (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)) ≫
      MonoidalCategoryStruct.whiskerLeft (Y i₂) (Iso.hom (β_ (X i₁) (Z i₃))) ≫ ιTensorObj₃ Y Z X i₂ i₃ i₁ k ⋯
| CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z k)
    (ιTensorObj₃' X Y Z i₁ i₂ i₃ k h)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Y Z) k)
      (Iso.hom (associator X Y Z) k)
      (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y Z) X k)
        (tensorObjDesc fun (i j : I) (hij : i + j = k) ↦
          Iso.hom (β_ (X i) (tensorObj.{u_1, v_1, u_2} Y Z j)) ≫ ιTensorObj (tensorObj.{u_1, v_1, u_2} Y Z) X j i k ⋯)
        (Iso.hom (associator Y Z X) k)))

Tactic:
rw [ιTensorObj₃'_associator_hom_assoc, ιTensorObj₃_eq X Y Z i₁ i₂ i₃ k h _ rfl,
    assoc, ι_tensorObjDesc_assoc, assoc, ← MonoidalCategory.id_tensorHom,
    BraidedCategory.braiding_naturality_assoc,
    BraidedCategory.braiding_tensor_right_hom, assoc, assoc, assoc, assoc, Iso.hom_inv_id_assoc,
    MonoidalCategory.tensorHom_id,
    ← ιTensorObj₃'_eq_assoc Y Z X i₂ i₃ i₁ k (by rw [add_comm _ i₁, ← add_assoc, h]) _ rfl,
    ιTensorObj₃'_associator_hom, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.BraidedCategory.braiding_tensor_right_hom, CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc_assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.BraidedCategory.braiding_naturality_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom_assoc, rfl, CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y X
inst_6 : HasTensor.{u_1, v_1, u_2} Y Z
inst_7 : HasTensor.{u_1, v_1, u_2} Z X
inst_8 : HasTensor.{u_1, v_1, u_2} X Z
inst_9 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z
inst_10 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Y Z)
inst_11 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y Z) X
inst_12 : HasTensor.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} Z X)
inst_13 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Y X) Z
inst_14 : HasTensor.{u_1, v_1, u_2} Y (tensorObj.{u_1, v_1, u_2} X Z)
inst_15 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Y Z
inst_16 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Y Z
inst_17 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Y Z X
inst_18 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Y Z X
inst_19 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Y X Z
inst_20 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Y X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
rw : i₁ + i₂ + i₃ = k
rw₁ rw₂ : k = k
⊢ i₂ + i₁ + i₃ = k

Tactic:
rw [add_comm i₂ i₁, h]

Premises used: add_comm
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y Z
inst_6 : HasTensor.{u_1, v_1, u_2} Z X
inst_7 : HasTensor.{u_1, v_1, u_2} Z Y
inst_8 : HasTensor.{u_1, v_1, u_2} X Z
inst_9 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z
inst_10 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Y Z)
inst_11 : HasTensor.{u_1, v_1, u_2} Z (tensorObj.{u_1, v_1, u_2} X Y)
inst_12 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Z X) Y
inst_13 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Z Y)
inst_14 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Z) Y
inst_15 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Y Z
inst_16 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Y Z
inst_17 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Z X Y
inst_18 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Z X Y
inst_19 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Z Y
inst_20 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
rw : i₃ + (i₁ + i₂) = k
rw₁ : i₁ + i₂ + i₃ = k
rw₂ rw₃ : k = k
⊢ i₃ + i₁ + i₂ = k

Tactic:
rw [add_assoc, add_comm i₃, h]

Premises used: add_assoc, add_comm
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y Z
inst_6 : HasTensor.{u_1, v_1, u_2} Z X
inst_7 : HasTensor.{u_1, v_1, u_2} Z Y
inst_8 : HasTensor.{u_1, v_1, u_2} X Z
inst_9 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z
inst_10 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Y Z)
inst_11 : HasTensor.{u_1, v_1, u_2} Z (tensorObj.{u_1, v_1, u_2} X Y)
inst_12 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Z X) Y
inst_13 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Z Y)
inst_14 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Z) Y
inst_15 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Y Z
inst_16 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Y Z
inst_17 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Z X Y
inst_18 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Z X Y
inst_19 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Z Y
inst_20 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
rw :
  MonoidalCategoryStruct.whiskerLeft (X i₁) (Iso.hom (β_ (Y i₂) (Z i₃))) ≫
    Iso.inv (MonoidalCategoryStruct.associator (X i₁) (Z i₃) (Y i₂)) ≫
      MonoidalCategoryStruct.whiskerRight (Iso.hom (β_ (X i₁) (Z i₃))) (Y i₂) ≫ ιTensorObj₃' Z X Y i₃ i₁ i₂ k ⋯
| CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Y Z) k)
    (ιTensorObj₃ X Y Z i₁ i₂ i₃ k h)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z k)
      (Iso.inv (associator X Y Z) k)
      (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Z (tensorObj.{u_1, v_1, u_2} X Y) k)
        (tensorObjDesc fun (i j : I) (hij : i + j = k) ↦
          Iso.hom (β_ (tensorObj.{u_1, v_1, u_2} X Y i) (Z j)) ≫ ιTensorObj Z (tensorObj.{u_1, v_1, u_2} X Y) j i k ⋯)
        (Iso.inv (associator Z X Y) k)))

Tactic:
rw [ιTensorObj₃_associator_inv_assoc, ιTensorObj₃'_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc,
    ι_tensorObjDesc_assoc, assoc, ← MonoidalCategory.tensorHom_id,
    BraidedCategory.braiding_naturality_assoc,
    BraidedCategory.braiding_tensor_left_hom, assoc, assoc, assoc, assoc, Iso.inv_hom_id_assoc,
    MonoidalCategory.id_tensorHom,
    ← ιTensorObj₃_eq_assoc Z X Y i₃ i₁ i₂ k (by rw [add_assoc, add_comm i₃, h]) _ rfl,
    ιTensorObj₃_associator_inv, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.BraidedCategory.braiding_tensor_left_hom, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv, CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv_assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.BraidedCategory.braiding_naturality_assoc, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq_assoc, CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq, rfl, CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y Z
inst_6 : HasTensor.{u_1, v_1, u_2} Z X
inst_7 : HasTensor.{u_1, v_1, u_2} Z Y
inst_8 : HasTensor.{u_1, v_1, u_2} X Z
inst_9 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Y) Z
inst_10 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Y Z)
inst_11 : HasTensor.{u_1, v_1, u_2} Z (tensorObj.{u_1, v_1, u_2} X Y)
inst_12 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} Z X) Y
inst_13 : HasTensor.{u_1, v_1, u_2} X (tensorObj.{u_1, v_1, u_2} Z Y)
inst_14 : HasTensor.{u_1, v_1, u_2} (tensorObj.{u_1, v_1, u_2} X Z) Y
inst_15 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Y Z
inst_16 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Y Z
inst_17 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} Z X Y
inst_18 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} Z X Y
inst_19 : HasGoodTensor₁₂Tensor.{u_1, v_1, u_2} X Z Y
inst_20 : HasGoodTensorTensor₂₃.{u_1, v_1, u_2} X Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
rw : i₁ + (i₃ + i₂) = k
rw₁ : i₁ + (i₂ + i₃) = k
rw₂ : i₁ + i₂ + i₃ = k
rw₃ rw₄ : k = k
⊢ i₁ + i₃ + i₂ = k

Tactic:
rw [add_assoc, add_comm i₃, ← add_assoc, h]

Premises used: add_assoc, add_comm
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y : GradedObject I C
inst_3 : SymmetricCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y X
dsimp :
  Eq (α := tensorObj.{u_1, v_1, u_2} X Y ⟶ tensorObj.{u_1, v_1, u_2} X Y)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y X)
      (fun (k : I) ↦ tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (X i) (Y j)) ≫ ιTensorObj Y X j i k ⋯)
      fun (k : I) ↦ tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (Y i) (X j)) ≫ ιTensorObj X Y j i k ⋯)
    (𝟙 (tensorObj.{u_1, v_1, u_2} X Y))
⊢ CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y X) (Iso.hom (braiding X Y)) (Iso.hom (braiding Y X)) =
    𝟙 (tensorObj.{u_1, v_1, u_2} X Y)

Tactic:
dsimp [braiding]

Premises used: CategoryTheory.GradedObject.Monoidal.braiding
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
X : C
e : F.obj X ≅ 𝟭 D
inst_5 : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp_1 : ∀ (j : J), p (0, j) = j
Y_1 Y' : GradedObject J D
φ : Y_1 ⟶ Y'
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
j : J
a : I × J
ha_1 : p a = j
ha : a.1 = 0
⊢ Y a.2 = Y j

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
X : C
e : F.obj X ≅ 𝟭 D
inst_5 : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
j : J
⊢ Eq (α :=
    (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) ⋯) ⟶
      Cocone.pt (F := Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
        (mapBifunctorLeftUnitorCofan F X e p hp Y j))
    (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j)
      (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) ⋯))
    (NatTrans.app (F.map (Iso.hom (singleObjApplyIso 0 X))) (Y j) ≫ e.hom.app (Y j))

Tactic:
simp [mapBifunctorLeftUnitorCofan]

Premises used: CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
X : C
e : F.obj X ≅ 𝟭 D
inst_5 : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)
i : I
j' : J
h : (i, j') ∈ p ⁻¹' {j}
hi : i = 0
pos :
  ∀ (h : (0, j') ∈ p ⁻¹' {j}),
    Eq (α :=
      (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j
          (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j') h) ⟶
        s.pt)
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
          (mapBifunctorLeftUnitorCofan F X e p hp Y j))
        (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j)
          (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j') h))
        ((fun (s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)) ↦
            (e.inv.app (Y j) ≫
                CategoryStruct.comp (Y := (F.obj (Functor.obj (single 0) X 0)).obj (Y j))
                  (NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y j))
                  (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) ⋯)) :
              Cocone.pt (F :=
                  Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
                  (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟶
                s.pt))
          s))
      (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j') h))
⊢ Eq (α :=
    (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h) ⟶
      s.pt)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
        (mapBifunctorLeftUnitorCofan F X e p hp Y j))
      (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j)
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))
      ((fun (s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)) ↦
          (e.inv.app (Y j) ≫
              CategoryStruct.comp (Y := (F.obj (Functor.obj (single 0) X 0)).obj (Y j))
                (NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y j))
                (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) ⋯)) :
            Cocone.pt (F :=
                Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
                (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟶
              s.pt))
        s))
    (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))

Tactic:
subst hi
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
X : C
e : F.obj X ≅ 𝟭 D
inst_5 : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)
j' : J
h : (0, j') ∈ p ⁻¹' {j}
⊢ j' = j

Tactic:
simp only [Set.mem_preimage, hp, Set.mem_singleton_iff] at h

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
X : C
e : F.obj X ≅ 𝟭 D
inst_5 : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j' : J
s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j')
h : (0, j') ∈ p ⁻¹' {j'}
⊢ Eq (α :=
    (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j'
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j'}) (0, j') h) ⟶
      s.pt)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j'))
        (mapBifunctorLeftUnitorCofan F X e p hp Y j'))
      (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j')
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j'}) (0, j') h))
      ((fun (s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j')) ↦
          (e.inv.app (Y j') ≫
              CategoryStruct.comp (Y := (F.obj (Functor.obj (single 0) X 0)).obj (Y j'))
                (NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y j'))
                (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j'}) (0, j') ⋯)) :
            Cocone.pt (F :=
                Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j'))
                (mapBifunctorLeftUnitorCofan F X e p hp Y j') ⟶
              s.pt))
        s))
    (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j'}) (0, j') h))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
X : C
e : F.obj X ≅ 𝟭 D
inst_5 : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)
i : I
j' : J
h : (i, j') ∈ p ⁻¹' {j}
hi : ¬i = 0
neg :
  IsInitial.{v_2, u_2}
    ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j
      (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))
⊢ Eq (α :=
    (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h) ⟶
      s.pt)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
        (mapBifunctorLeftUnitorCofan F X e p hp Y j))
      (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j)
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))
      ((fun (s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)) ↦
          (e.inv.app (Y j) ≫
              CategoryStruct.comp (Y := (F.obj (Functor.obj (single 0) X 0)).obj (Y j))
                (NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y j))
                (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) ⋯)) :
            Cocone.pt (F :=
                Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
                (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟶
              s.pt))
        s))
    (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))

Tactic:
apply IsInitial.hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext