awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃
⊢ 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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃
⊢ 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))
have 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))
Tactic: simp only [← NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃
⊢ 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))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃
⊢ 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))
have 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))
Tactic: rw [NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₂
⊢ ((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 φ
have 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 := sorry })
      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 := sorry :
          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₃))
Tactic: ext X₃ ⟨i₁, i₂, i₃⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₂
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₃))
have w : Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ ((F'.obj (X₁ i₁)).obj (Y₂ i₂)).obj (X₃ i₃))
  (((F.obj (X₁ i₁)).map (φ i₂)).app (X₃ i₃) ≫ NatTrans.app (NatTrans.app (α.app (X₁ i₁)) (Y₂ i₂)) (X₃ i₃))
  (NatTrans.app (NatTrans.app (α.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫ ((F'.obj (X₁ i₁)).map (φ i₂)).app (X₃ i₃))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
⊢ (mapTrifunctor F I₁ I₂ I₃).map φ ≫
      {
        app := fun (X₂ : GradedObject I₂ C₂) ↦
          {
            app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
              NatTrans.app (NatTrans.app (α.app (Y₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
            naturality := ⋯ },
        naturality := ⋯ } =
    {
        app := fun (X₂ : GradedObject I₂ C₂) ↦
          {
            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₂) },
        naturality := ⋯ : NatTrans ((mapTrifunctor F I₁ I₂ I₃).obj X₁) ((mapTrifunctor F' I₁ I₂ I₃).obj X₁) } ≫
      (mapTrifunctor F' I₁ I₂ I₃).map φ
have w : ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
  Eq.{v_4 + 1}
    (NatTrans.app
      (NatTrans.app
        ((mapTrifunctor F I₁ I₂ I₃).map φ ≫
          {
            app := fun (X₂ : GradedObject I₂ C₂) ↦
              {
                app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
                  NatTrans.app (NatTrans.app (α.app (Y₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
                naturality := sorry },
            naturality := sorry })
        X₂)
      X₃ (i₁, i₂, i₃))
    (NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : GradedObject I₂ C₂) ↦
              {
                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 := sorry :
                NatTrans (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂) (((mapTrifunctor F' I₁ I₂ I₃).obj X₁).obj X₂) },
            naturality := sorry : NatTrans ((mapTrifunctor F I₁ I₂ I₃).obj X₁) ((mapTrifunctor F' I₁ I₂ I₃).obj X₁) } ≫
          (mapTrifunctor F' I₁ I₂ I₃).map φ)
        X₂)
      X₃ (i₁, i₂, i₃))
Tactic: ext X₂ X₃ ⟨i₁, i₂, i₃⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ Eq.{v_4 + 1}
    (NatTrans.app
      (NatTrans.app
        ((mapTrifunctor F I₁ I₂ I₃).map φ ≫
          {
            app := fun (X₂ : GradedObject I₂ C₂) ↦
              {
                app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
                  NatTrans.app (NatTrans.app (α.app (Y₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
                naturality := ⋯ },
            naturality := ⋯ })
        X₂)
      X₃ (i₁, i₂, i₃))
    (NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : GradedObject I₂ C₂) ↦
              {
                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₂) },
            naturality := ⋯ : NatTrans ((mapTrifunctor F I₁ I₂ I₃).obj X₁) ((mapTrifunctor F' I₁ I₂ I₃).obj X₁) } ≫
          (mapTrifunctor F' I₁ I₂ I₃).map φ)
        X₂)
      X₃ (i₁, i₂, i₃))
have w : Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ ((F'.obj (Y₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))
  (NatTrans.app ((F.map (φ i₁)).app (X₂ i₂)) (X₃ i₃) ≫ NatTrans.app (NatTrans.app (α.app (Y₁ i₁)) (X₂ i₂)) (X₃ i₃))
  (NatTrans.app (NatTrans.app (α.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫ NatTrans.app ((F'.map (φ i₁)).app (X₂ i₂)) (X₃ i₃))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
⊢ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ = 𝟙 (mapTrifunctor F I₁ I₂ I₃)
have w : ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
  (((mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃).app X₁).app X₂).app X₃
      (i₁, i₂, i₃) =
    ((NatTrans.app (𝟙 (mapTrifunctor F I₁ I₂ I₃)) X₁).app X₂).app X₃ (i₁, i₂, i₃)
Tactic: ext X₁ X₂ X₃ ⟨i₁, i₂, i₃⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ (((mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃).app X₁).app X₂).app X₃
      (i₁, i₂, i₃) =
    ((NatTrans.app (𝟙 (mapTrifunctor F I₁ I₂ I₃)) X₁).app X₂).app X₃ (i₁, i₂, i₃)
have w : NatTrans.app (NatTrans.app (e.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
    NatTrans.app (NatTrans.app (e.inv.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) =
  𝟙 (((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
⊢ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ = 𝟙 (mapTrifunctor F' I₁ I₂ I₃)
have w : ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
  (((mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃).app X₁).app X₂).app X₃
      (i₁, i₂, i₃) =
    ((NatTrans.app (𝟙 (mapTrifunctor F' I₁ I₂ I₃)) X₁).app X₂).app X₃ (i₁, i₂, i₃)
Tactic: ext X₁ X₂ X₃ ⟨i₁, i₂, i₃⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ (((mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃).app X₁).app X₂).app X₃
      (i₁, i₂, i₃) =
    ((NatTrans.app (𝟙 (mapTrifunctor F' I₁ I₂ I₃)) X₁).app X₂).app X₃ (i₁, i₂, i₃)
have w : NatTrans.app (NatTrans.app (e.inv.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
    NatTrans.app (NatTrans.app (e.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) =
  𝟙 (((F'.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
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
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst_4 : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst_5 : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (mapTrifunctorMapMap F p f₁ f₂ f₃ j))
    (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫ ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)
have dsimp : Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
  (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j)
    (((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j h)
    (mapMap
      ((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
        (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
      p j))
  (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
    ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
        ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
Tactic: dsimp only [ιMapTrifunctorMapObj, mapTrifunctorMapMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
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
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst_4 : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst_5 : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j)
      (((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j h)
      (mapMap
        ((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
          (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
        p j))
    (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
have rw : Eq.{v_4 + 1} (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
  (((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
          (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
        (i₁, i₂, i₃) ≫
      ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h :
    (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃ (i₁, i₂, i₃) ⟶
      ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).mapObj p j)
  (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h :
    ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
Tactic: rw [ι_mapMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
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
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst_4 : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst_5 : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ Eq.{v_4 + 1} (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    (((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
            (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
          (i₁, i₂, i₃) ≫
        ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h :
      (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃ (i₁, i₂, i₃) ⟶
        ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).mapObj p j)
    (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
          ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
            ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h :
      ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
have dsimp : Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
  ((NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) ≫
    (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
  (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
    ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
        (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
Tactic: dsimp