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
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
-- 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
n : ℕ
x : (↑(Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) : Type)
i₁ i₂ : ℕ
hi : i₁ + i₂ = n
⊢ i₁ < n + 1

Tactic:
lia
-- 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
n : ℕ
x : (↑(Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) : Type)
i₁ i₂ : ℕ
hi : i₁ + i₂ = n
⊢ i₂ < n + 1

Tactic:
lia
-- 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
n : ℕ
refine :
  Function.Injective (β := Fin (n + 1) × Fin (n + 1))
    fun (x : (↑(Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) : Type)) ↦
    match (motive := (↑(Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) : Type) → Fin (n + 1) × Fin (n + 1))
      x with
    | ⟨(i₁, i₂), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩)
⊢ Finite (↑(Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) : Type)

Tactic:
refine Finite.of_injective (fun ⟨⟨i₁, i₂⟩, (hi : i₁ + i₂ = n)⟩ =>
    ((⟨i₁, by lia⟩, ⟨i₂, by lia⟩) : Fin (n + 1) × Fin (n + 1))) ?_

Premises used: Finite.of_injective
-- 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
n fst snd : ℕ
property : Membership.mem (γ := Set (ℕ × ℕ)) (Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) (fst, snd)
fst_1 snd_1 : ℕ
property_1 : Membership.mem (γ := Set (ℕ × ℕ)) (Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) (fst_1, snd_1)
h :
  Eq (α := Fin (n + 1) × Fin (n + 1))
    ((fun (x : (↑(Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) : Type)) ↦
        (match (motive :=
            (↑(Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) : Type) → Fin (n + 1) × Fin (n + 1)) x with
          | ⟨(i₁, i₂), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩) :
          Fin (n + 1) × Fin (n + 1)))
      (Subtype.mk (p := fun (x : ℕ × ℕ) ↦
        Membership.mem (γ := Set (ℕ × ℕ)) (Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) x) (fst, snd)
        property))
    ((fun (x : (↑(Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) : Type)) ↦
        (match (motive :=
            (↑(Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) : Type) → Fin (n + 1) × Fin (n + 1)) x with
          | ⟨(i₁, i₂), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩) :
          Fin (n + 1) × Fin (n + 1)))
      (Subtype.mk (p := fun (x : ℕ × ℕ) ↦
        Membership.mem (γ := Set (ℕ × ℕ)) (Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) x) (fst_1, snd_1)
        property_1))
⊢ Subtype.mk (p := fun (x : ℕ × ℕ) ↦
      Membership.mem (γ := Set (ℕ × ℕ)) (Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) x) (fst, snd)
      property =
    Subtype.mk (p := fun (x : ℕ × ℕ) ↦
      Membership.mem (γ := Set (ℕ × ℕ)) (Set.preimage (β := ℕ) (fun (i : ℕ × ℕ) ↦ i.1 + i.2) {n}) x) (fst_1, snd_1)
      property_1

Tactic:
simpa using 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
n : ℕ
x : (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type)
i₁ i₂ i₃ : ℕ
hi : i₁ + i₂ + i₃ = n
⊢ i₁ < n + 1

Tactic:
lia
-- 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
n : ℕ
x : (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type)
i₁ i₂ i₃ : ℕ
hi : i₁ + i₂ + i₃ = n
⊢ i₂ < n + 1

Tactic:
lia
-- 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
n : ℕ
x : (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type)
i₁ i₂ i₃ : ℕ
hi : i₁ + i₂ + i₃ = n
⊢ i₃ < n + 1

Tactic:
lia
-- 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
n : ℕ
refine :
  Function.Injective (β := Fin (n + 1) × Fin (n + 1) × Fin (n + 1))
    fun (x : (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type)) ↦
    match (motive := (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type) → Fin (n + 1) × Fin (n + 1) × Fin (n + 1))
      x with
    | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩)
⊢ Finite (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type)

Tactic:
refine Finite.of_injective (fun ⟨⟨i₁, i₂, i₃⟩, (hi : i₁ + i₂ + i₃ = n)⟩ =>
    (⟨⟨i₁, by lia⟩, ⟨i₂, by lia⟩, ⟨i₃, by lia⟩⟩ :
      Fin (n + 1) × Fin (n + 1) × Fin (n + 1))) ?_

Premises used: Finite.of_injective
-- 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
n fst fst_1 snd : ℕ
property : Membership.mem (γ := Set (ℕ × ℕ × ℕ)) {i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} (fst, fst_1, snd)
fst_2 fst_3 snd_1 : ℕ
property_1 : Membership.mem (γ := Set (ℕ × ℕ × ℕ)) {i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} (fst_2, fst_3, snd_1)
h :
  Eq (α := Fin (n + 1) × Fin (n + 1) × Fin (n + 1))
    ((fun (x : (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type)) ↦
        (match (motive := (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type) → Fin (n + 1) × Fin (n + 1) × Fin (n + 1))
            x with
          | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩) :
          Fin (n + 1) × Fin (n + 1) × Fin (n + 1)))
      (Subtype.mk (p := fun (x : ℕ × ℕ × ℕ) ↦
        Membership.mem (γ := Set (ℕ × ℕ × ℕ)) {i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} x) (fst, fst_1, snd) property))
    ((fun (x : (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type)) ↦
        (match (motive := (↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} : Type) → Fin (n + 1) × Fin (n + 1) × Fin (n + 1))
            x with
          | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩) :
          Fin (n + 1) × Fin (n + 1) × Fin (n + 1)))
      (Subtype.mk (p := fun (x : ℕ × ℕ × ℕ) ↦
        Membership.mem (γ := Set (ℕ × ℕ × ℕ)) {i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} x) (fst_2, fst_3, snd_1)
        property_1))
⊢ Subtype.mk (p := fun (x : ℕ × ℕ × ℕ) ↦
      Membership.mem (γ := Set (ℕ × ℕ × ℕ)) {i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} x) (fst, fst_1, snd) property =
    Subtype.mk (p := fun (x : ℕ × ℕ × ℕ) ↦
      Membership.mem (γ := Set (ℕ × ℕ × ℕ)) {i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n} x) (fst_2, fst_3, snd_1)
      property_1

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
X₁ X₂ : C
f : X₁ ⟶ X₂
i : J
h : ¬i = j
dsimp : (if i = j then X₁ else initial.{v_1, u_2} C) = if i = j then X₂ else initial.{v_1, u_2} C
⊢ Eq.{u_2 + 1} (α := (fun (x : J) ↦ C) i) ((fun (i : J) ↦ if i = j then X₁ else initial.{v_1, u_2} C) i)
    ((fun (i : J) ↦ if i = j then X₂ else initial.{v_1, u_2} C) i)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
X₁ X₂ : C
f : X₁ ⟶ X₂
i : J
h : ¬i = j
rw : initial.{v_1, u_2} C = if i = j then X₂ else initial.{v_1, u_2} C
rw₁ rw₂ : initial.{v_1, u_2} C = initial.{v_1, u_2} C
⊢ (if i = j then X₁ else initial.{v_1, u_2} C) = if i = j then X₂ else initial.{v_1, u_2} C

Tactic:
rw [if_neg h, if_neg h]

Premises used: if_neg
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
X : C
i : J
h : i ≠ j
dsimp : IsInitial.{v_1, u_2} (if i = j then X else initial.{v_1, u_2} C)
⊢ IsInitial.{v_1, u_2} (Functor.obj (single j) X i)

Tactic:
dsimp [single]

Premises used: CategoryTheory.GradedObject.single
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
X : C
i : J
h : i ≠ j
rw : IsInitial.{v_1, u_2} (initial.{v_1, u_2} C)
⊢ IsInitial.{v_1, u_2} (if i = j then X else initial.{v_1, u_2} C)

Tactic:
rw [if_neg h]

Premises used: if_neg
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
X : C
i : J
h : i ≠ j
⊢ IsInitial.{v_1, u_2} (initial.{v_1, u_2} C)

Tactic:
exact initialIsInitial

Premises used: CategoryTheory.Limits.initialIsInitial
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
i : J
h : i = j
subst :
  Eq (α := X ⟶ Functor.obj (single i) Y i)
    (CategoryStruct.comp (Y := Functor.obj (single i) X i) (Iso.inv (singleObjApplyIsoOfEq i X i ⋯))
      (Functor.map (single i) f i))
    (f ≫ Iso.inv (singleObjApplyIsoOfEq i Y i ⋯))
⊢ Eq (α := X ⟶ Functor.obj (single j) Y i)
    (CategoryStruct.comp (Y := Functor.obj (single j) X i) (Iso.inv (singleObjApplyIsoOfEq j X i h))
      (Functor.map (single j) f i))
    (f ≫ Iso.inv (singleObjApplyIsoOfEq j Y i h))

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ Eq (α := X ⟶ Functor.obj (single i) Y i)
    (CategoryStruct.comp (Y := Functor.obj (single i) X i) (Iso.inv (singleObjApplyIsoOfEq i X i ⋯))
      (Functor.map (single i) f i))
    (f ≫ Iso.inv (singleObjApplyIsoOfEq i Y i ⋯))

Tactic:
simp [singleObjApplyIsoOfEq, single]

Premises used: CategoryTheory.GradedObject.single, CategoryTheory.GradedObject.singleObjApplyIsoOfEq
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
i : J
h : i = j
subst :
  Eq.{v_1 + 1} (α := Functor.obj (single i) X i ⟶ Y)
    (CategoryStruct.comp (Y := Functor.obj (single i) Y i) (Functor.map (single i) f i)
        (Iso.hom (singleObjApplyIsoOfEq i Y i ⋯)) :
      Functor.obj (single i) X i ⟶ Y)
    (Iso.hom (singleObjApplyIsoOfEq i X i ⋯) ≫ f : Functor.obj (single i) X i ⟶ Y)
⊢ Eq.{v_1 + 1} (α := Functor.obj (single j) X i ⟶ Y)
    (CategoryStruct.comp (Y := Functor.obj (single j) Y i) (Functor.map (single j) f i)
        (Iso.hom (singleObjApplyIsoOfEq j Y i h)) :
      Functor.obj (single j) X i ⟶ Y)
    (Iso.hom (singleObjApplyIsoOfEq j X i h) ≫ f : Functor.obj (single j) X i ⟶ Y)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ Eq.{v_1 + 1} (α := Functor.obj (single i) X i ⟶ Y)
    (CategoryStruct.comp (Y := Functor.obj (single i) Y i) (Functor.map (single i) f i)
        (Iso.hom (singleObjApplyIsoOfEq i Y i ⋯)) :
      Functor.obj (single i) X i ⟶ Y)
    (Iso.hom (singleObjApplyIsoOfEq i X i ⋯) ≫ f : Functor.obj (single i) X i ⟶ Y)

Tactic:
simp [singleObjApplyIsoOfEq, single]

Premises used: CategoryTheory.GradedObject.single, CategoryTheory.GradedObject.singleObjApplyIsoOfEq
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
⊢ Eq (α := X ⟶ Functor.obj (single j) Y j)
    (CategoryStruct.comp (Y := Functor.obj (single j) X j) (Iso.inv (singleObjApplyIso j X))
      (Functor.map (single j) f j))
    (f ≫ Iso.inv (singleObjApplyIso j Y))

Tactic:
apply singleObjApplyIsoOfEq_inv_single_map

Premises used: CategoryTheory.GradedObject.singleObjApplyIsoOfEq_inv_single_map
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
⊢ Eq.{v_1 + 1} (α := Functor.obj (single j) X j ⟶ Y)
    (CategoryStruct.comp (Y := Functor.obj (single j) Y j) (Functor.map (single j) f j)
        (Iso.hom (singleObjApplyIso j Y)) :
      Functor.obj (single j) X j ⟶ Y)
    (Iso.hom (singleObjApplyIso j X) ≫ f : Functor.obj (single j) X j ⟶ Y)

Tactic:
apply single_map_singleObjApplyIsoOfEq_hom

Premises used: CategoryTheory.GradedObject.single_map_singleObjApplyIsoOfEq_hom
-- Module: Mathlib.CategoryTheory.GradedObject.Single
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : HasInitial.{v_1, u_2} C
inst_2 : DecidableEq J
j : J
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    Eq (α := Functor.obj.{v_1, v_1, u_2, u_2} (single j ⋙ eval j) X ⟶ Functor.obj.{v_1, v_1, u_2, u_2} (𝟭 C) Y)
      (Functor.map (single j ⋙ eval j) f ≫ Iso.hom (singleObjApplyIso j Y))
      (Iso.hom (singleObjApplyIso j X) ≫ Functor.map (𝟭 C) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
w :
  ∀ (X₃ : GradedObject I₃ C₃) (x : I₁ × I₂ × I₃),
    Eq.{v_4 + 1}
      (NatTrans.app
        ((mapTrifunctorObj F X₁ I₂ I₃).map ψ ≫
          {
            app := fun (X₃ : GradedObject I₃ C₃) (x : I₁ × I₂ × I₃) ↦
              NatTrans.app (NatTrans.app (F.map (φ x.1)) (Y₂ x.2.1)) (X₃ x.2.2),
            naturality := ⋯ })
        X₃ x)
      (NatTrans.app
        ({
            app := fun (X₃ : GradedObject I₃ C₃) (x : I₁ × I₂ × I₃) ↦
              NatTrans.app (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1)) (X₃ x.2.2),
            naturality := ⋯ : NatTrans ((mapTrifunctorObj F X₁ I₂ I₃).obj X₂) ((mapTrifunctorObj F Y₁ I₂ I₃).obj X₂) } ≫
          (mapTrifunctorObj F Y₁ I₂ I₃).map ψ)
        X₃ x)
⊢ (mapTrifunctorObj F X₁ I₂ I₃).map ψ ≫
      {
        app := fun (X₃ : GradedObject I₃ C₃) (x : I₁ × I₂ × I₃) ↦
          NatTrans.app (NatTrans.app (F.map (φ x.1)) (Y₂ x.2.1)) (X₃ x.2.2),
        naturality := ⋯ } =
    {
        app := fun (X₃ : GradedObject I₃ C₃) (x : I₁ × I₂ × I₃) ↦
          NatTrans.app (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1)) (X₃ x.2.2),
        naturality := ⋯ : NatTrans ((mapTrifunctorObj F X₁ I₂ I₃).obj X₂) ((mapTrifunctorObj F Y₁ I₂ I₃).obj X₂) } ≫
      (mapTrifunctorObj F Y₁ I₂ I₃).map ψ

Tactic:
ext X₃ x
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
x : I₁ × I₂ × I₃
w :
  Eq (α := ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).obj (X₃ x.2.2) ⟶ ((F.obj (Y₁ x.1)).obj (Y₂ x.2.1)).obj (X₃ x.2.2))
    (NatTrans.app ((F.obj (X₁ x.1)).map (ψ x.2.1)) (X₃ x.2.2) ≫
      NatTrans.app (NatTrans.app (F.map (φ x.1)) (Y₂ x.2.1)) (X₃ x.2.2))
    (NatTrans.app (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1)) (X₃ x.2.2) ≫
      NatTrans.app ((F.obj (Y₁ x.1)).map (ψ x.2.1)) (X₃ x.2.2))
⊢ Eq.{v_4 + 1}
    (NatTrans.app
      ((mapTrifunctorObj F X₁ I₂ I₃).map ψ ≫
        {
          app := fun (X₃ : GradedObject I₃ C₃) (x : I₁ × I₂ × I₃) ↦
            NatTrans.app (NatTrans.app (F.map (φ x.1)) (Y₂ x.2.1)) (X₃ x.2.2),
          naturality := ⋯ })
      X₃ x)
    (NatTrans.app
      ({
          app := fun (X₃ : GradedObject I₃ C₃) (x : I₁ × I₂ × I₃) ↦
            NatTrans.app (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1)) (X₃ x.2.2),
          naturality := ⋯ : NatTrans ((mapTrifunctorObj F X₁ I₂ I₃).obj X₂) ((mapTrifunctorObj F Y₁ I₂ I₃).obj X₂) } ≫
        (mapTrifunctorObj F Y₁ I₂ I₃).map ψ)
      X₃ x)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
x : I₁ × I₂ × I₃
w :
  Eq (α := ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).obj (X₃ x.2.2) ⟶ ((F.obj (Y₁ x.1)).obj (Y₂ x.2.1)).obj (X₃ x.2.2))
    (NatTrans.app ((F.obj (X₁ x.1)).map (ψ x.2.1) ≫ NatTrans.app (F.map (φ x.1)) (Y₂ x.2.1)) (X₃ x.2.2))
    (NatTrans.app (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1) ≫ (F.obj (Y₁ x.1)).map (ψ x.2.1)) (X₃ x.2.2))
⊢ Eq (α := ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).obj (X₃ x.2.2) ⟶ ((F.obj (Y₁ x.1)).obj (Y₂ x.2.1)).obj (X₃ x.2.2))
    (NatTrans.app ((F.obj (X₁ x.1)).map (ψ x.2.1)) (X₃ x.2.2) ≫
      NatTrans.app (NatTrans.app (F.map (φ x.1)) (Y₂ x.2.1)) (X₃ x.2.2))
    (NatTrans.app (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1)) (X₃ x.2.2) ≫
      NatTrans.app ((F.obj (Y₁ x.1)).map (ψ x.2.1)) (X₃ x.2.2))

Tactic:
simp only [← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
x : I₁ × I₂ × I₃
w :
  Eq (α := NatTrans ((F.obj (X₁ x.1)).obj (X₂ x.2.1)) ((F.obj (Y₁ x.1)).obj (Y₂ x.2.1)))
    ((F.obj (X₁ x.1)).map (ψ x.2.1) ≫ NatTrans.app (F.map (φ x.1)) (Y₂ x.2.1))
    (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1) ≫ (F.obj (Y₁ x.1)).map (ψ x.2.1))
⊢ Eq (α := ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).obj (X₃ x.2.2) ⟶ ((F.obj (Y₁ x.1)).obj (Y₂ x.2.1)).obj (X₃ x.2.2))
    (NatTrans.app ((F.obj (X₁ x.1)).map (ψ x.2.1) ≫ NatTrans.app (F.map (φ x.1)) (Y₂ x.2.1)) (X₃ x.2.2))
    (NatTrans.app (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1) ≫ (F.obj (Y₁ x.1)).map (ψ x.2.1)) (X₃ x.2.2))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
x : I₁ × I₂ × I₃
w w₁ :
  Eq (α := NatTrans ((F.obj (X₁ x.1)).obj (X₂ x.2.1)) ((F.obj (Y₁ x.1)).obj (Y₂ x.2.1)))
    (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1) ≫ (F.obj (Y₁ x.1)).map (ψ x.2.1))
    (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1) ≫ (F.obj (Y₁ x.1)).map (ψ x.2.1))
⊢ Eq (α := NatTrans ((F.obj (X₁ x.1)).obj (X₂ x.2.1)) ((F.obj (Y₁ x.1)).obj (Y₂ x.2.1)))
    ((F.obj (X₁ x.1)).map (ψ x.2.1) ≫ NatTrans.app (F.map (φ x.1)) (Y₂ x.2.1))
    (NatTrans.app (F.map (φ x.1)) (X₂ x.2.1) ≫ (F.obj (Y₁ x.1)).map (ψ x.2.1))

Tactic:
rw [NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ Y₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
w :
  ∀ (X₃ : GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
    Eq.{v_4 + 1}
      (NatTrans.app
        (((mapTrifunctor F I₁ I₂ I₃).obj X₁).map φ ≫
          {
            app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
              NatTrans.app (NatTrans.app (α.app (X₁ x_1.1)) (Y₂ x_1.2.1)) (x x_1.2.2),
            naturality := ⋯ })
        X₃ (i₁, i₂, i₃))
      (NatTrans.app
        ({
            app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
              NatTrans.app (NatTrans.app (α.app (X₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
            naturality := ⋯ :
            NatTrans (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂) (((mapTrifunctor F' I₁ I₂ I₃).obj X₁).obj X₂) } ≫
          ((mapTrifunctor F' I₁ I₂ I₃).obj X₁).map φ)
        X₃ (i₁, i₂, i₃))
⊢ ((mapTrifunctor F I₁ I₂ I₃).obj X₁).map φ ≫
      {
        app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
          NatTrans.app (NatTrans.app (α.app (X₁ x_1.1)) (Y₂ x_1.2.1)) (x x_1.2.2),
        naturality := ⋯ } =
    {
        app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
          NatTrans.app (NatTrans.app (α.app (X₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
        naturality := ⋯ :
        NatTrans (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂) (((mapTrifunctor F' I₁ I₂ I₃).obj X₁).obj X₂) } ≫
      ((mapTrifunctor F' I₁ I₂ I₃).obj X₁).map φ

Tactic:
ext X₃ ⟨i₁, i₂, i₃⟩