awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.RegularEpi (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} D
inst_2 : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst_3 : HasPushouts.{u_3, u_2} D
inst_4 : IsRegularEpiCategory.{u_3, u_2} D
F G : Functor.{u_4, u_3, u_1, u_2} C D
f : F ⟶ G
inst_5 : Epi f
k : C
⊢ IsColimit (F :=
    parallelPair
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).fst
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).snd ⋙
      obj (evaluation C D) k)
    (mapCocone (obj (evaluation C D) k) (Cofork.ofπ f ⋯))
have this : IsRegularEpi (f.app k)
Tactic: have := IsRegularEpiCategory.regularEpiOfEpi (f.app k)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.RegularEpi (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} D
inst_2 : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst_3 : HasPushouts.{u_3, u_2} D
inst_4 : IsRegularEpiCategory.{u_3, u_2} D
F G : Functor.{u_4, u_3, u_1, u_2} C D
f : F ⟶ G
inst_5 : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ IsColimit (F :=
    parallelPair
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).fst
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).snd ⋙
      obj (evaluation C D) k)
    (mapCocone (obj (evaluation C D) k) (Cofork.ofπ f ⋯))
have refine_1 : parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd ≅
  parallelPair
      (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
          pullback.isLimit (f.app k) (f.app k)).fst
      (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
          pullback.isLimit (f.app k) (f.app k)).snd ⋙
    obj (evaluation C D) k
Tactic: refine .equivOfNatIsoOfIso ?_ _ _ ?_ (isColimitCoforkOfEffectiveEpi (f.app k)
        (pullback.cone (f.app k) (f.app k))
        (pullback.isLimit (f.app k) (f.app k)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.RegularEpi (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} D
inst_2 : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst_3 : HasPushouts.{u_3, u_2} D
inst_4 : IsRegularEpiCategory.{u_3, u_2} D
F G : Functor.{u_4, u_3, u_1, u_2} C D
f : F ⟶ G
inst_5 : Epi f
k : C
this : IsRegularEpi (f.app k)
refine_1 :
  parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd ≅
    parallelPair
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).fst
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).snd ⋙
      obj (evaluation C D) k
⊢ IsColimit (F :=
    parallelPair
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).fst
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).snd ⋙
      obj (evaluation C D) k)
    (mapCocone (obj (evaluation C D) k) (Cofork.ofπ f ⋯))
have refine_2 : Iso (C :=
  Cocone
    (parallelPair
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).fst
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).snd ⋙
      obj (evaluation C D) k))
  (obj
    (Cocone.precompose
      (Iso.inv
        (NatIso.ofComponents
          (fun (X : WalkingParallelPair) ↦
            WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
              (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj x ≅
                (parallelPair
                        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                            pullback.isLimit (f.app k) (f.app k)).fst
                        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                            pullback.isLimit (f.app k) (f.app k)).snd ⋙
                      obj (evaluation C D) k).obj
                  x)
              X
              (Iso.refl
                ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
                  WalkingParallelPair.zero))
              (Iso.refl
                ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
                  WalkingParallelPair.one)))
          sorry)))
    (Cofork.ofπ (f.app k) sorry))
  (mapCocone (obj (evaluation C D) k) (Cofork.ofπ f sorry))
Tactic: refine .equivOfNatIsoOfIso ?_ _ _ ?_ (isColimitCoforkOfEffectiveEpi (f.app k)
        (pullback.cone (f.app k) (f.app k))
        (pullback.isLimit (f.app k) (f.app k)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
⊢ (bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫
      { app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := ⋯ :
        NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj Y₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj Y₂) } =
    { app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := ⋯ :
        NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj X₂) } ≫
      (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ
have w : ∀ (X₃ : C₃),
  ((bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫
          { app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := sorry :
            NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj Y₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj Y₂) }).app
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := sorry :
          NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj X₂) } ≫
        (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ)
      X₃
Tactic: ext X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
X₃ : C₃
⊢ ((bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫
          { app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := ⋯ :
            NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj Y₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj Y₂) }).app
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := ⋯ :
          NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj X₂) } ≫
        (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ)
      X₃
have w : (G.map ((F₁₂.obj X₁).map ψ)).app X₃ ≫ (G.map ((F₁₂.map φ).app Y₂)).app X₃ =
  (G.map ((F₁₂.map φ).app X₂)).app X₃ ≫ (G.map ((F₁₂.obj Y₁).map ψ)).app X₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ ((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫
      { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj Y₂)) X₃, naturality := ⋯ :
        NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj Y₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj Y₂) } =
    { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
        NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) } ≫
      ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f
have w : ∀ (X₃ : C₃),
  (((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫
          { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj Y₂)) X₃, naturality := sorry :
            NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj Y₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj Y₂) }).app
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := sorry :
          NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) } ≫
        ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f)
      X₃
Tactic: ext X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫
          { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj Y₂)) X₃, naturality := ⋯ :
            NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj Y₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj Y₂) }).app
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
          NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) } ≫
        ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f)
      X₃
have w : (G.map ((F₁₂.obj X₁).map f)).app X₃ ≫ NatTrans.app (φ.app ((F₁₂.obj X₁).obj Y₂)) X₃ =
  NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃ ≫ (G'.map ((F₁₂.obj X₁).map f)).app X₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ (bifunctorComp₁₂ F₁₂ G).map f ≫
      {
        app := fun (X₂ : C₂) ↦
          { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj Y₁).obj X₂)) X₃, naturality := ⋯ },
        naturality := ⋯ } =
    {
        app := fun (X₂ : C₂) ↦
          { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
            NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) },
        naturality := ⋯ : NatTrans ((bifunctorComp₁₂ F₁₂ G).obj X₁) ((bifunctorComp₁₂ F₁₂ G').obj X₁) } ≫
      (bifunctorComp₁₂ F₁₂ G').map f
have w : ∀ (X₂ : C₂) (X₃ : C₃),
  NatTrans.app
      (NatTrans.app
        ((bifunctorComp₁₂ F₁₂ G).map f ≫
          {
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj Y₁).obj X₂)) X₃, naturality := sorry },
            naturality := sorry })
        X₂)
      X₃ =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := sorry :
                NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) },
            naturality := sorry : NatTrans ((bifunctorComp₁₂ F₁₂ G).obj X₁) ((bifunctorComp₁₂ F₁₂ G').obj X₁) } ≫
          (bifunctorComp₁₂ F₁₂ G').map f)
        X₂)
      X₃
Tactic: ext X₂ X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ NatTrans.app
      (NatTrans.app
        ((bifunctorComp₁₂ F₁₂ G).map f ≫
          {
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj Y₁).obj X₂)) X₃, naturality := ⋯ },
            naturality := ⋯ })
        X₂)
      X₃ =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
                NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) },
            naturality := ⋯ : NatTrans ((bifunctorComp₁₂ F₁₂ G).obj X₁) ((bifunctorComp₁₂ F₁₂ G').obj X₁) } ≫
          (bifunctorComp₁₂ F₁₂ G').map f)
        X₂)
      X₃
have w : (G.map ((F₁₂.map f).app X₂)).app X₃ ≫ NatTrans.app (φ.app ((F₁₂.obj Y₁).obj X₂)) X₃ =
  NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃ ≫ (G'.map ((F₁₂.map f).app X₂)).app X₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).map f ≫
      { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ :
        NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj Y₂)
          (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj Y₂) } =
    { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
        NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
          (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) } ≫
      ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).map f
have w : ∀ (X₃ : C₃),
  (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).map f ≫
          { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := sorry :
            NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj Y₂)
              (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj Y₂) }).app
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := sorry :
          NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
            (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) } ≫
        ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).map f)
      X₃
Tactic: ext X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).map f ≫
          { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ :
            NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj Y₂)
              (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj Y₂) }).app
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
          NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
            (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) } ≫
        ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).map f)
      X₃
have w : (G.map ((F₁₂.obj X₁).map f)).app X₃ ≫ (G.map ((φ.app X₁).app Y₂)).app X₃ =
  (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.obj X₁).map f)).app X₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ (Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).map f ≫
      { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ },
        naturality := ⋯ } =
    {
        app := fun (X₂ : C₂) ↦
          { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
            NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
              (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) },
        naturality := ⋯ :
        NatTrans ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁)
          ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁) } ≫
      (Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).map f
have w : ∀ (X₂ : C₂) (X₃ : C₃),
  NatTrans.app
      (NatTrans.app
        ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).map f ≫
          { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := sorry },
            naturality := sorry })
        X₂)
      X₃ =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := sorry :
                NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
                  (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) },
            naturality := sorry :
            NatTrans ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁)
              ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁) } ≫
          (Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).map f)
        X₂)
      X₃
Tactic: ext X₂ X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ NatTrans.app
      (NatTrans.app
        ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).map f ≫
          { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ },
            naturality := ⋯ })
        X₂)
      X₃ =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
                NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
                  (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) },
            naturality := ⋯ :
            NatTrans ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁)
              ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁) } ≫
          (Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).map f)
        X₂)
      X₃
have w : (G.map ((F₁₂.map f).app X₂)).app X₃ ≫ (G.map ((φ.app Y₁).app X₂)).app X₃ =
  (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.map f).app X₂)).app X₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
f : G ⟶ G'
⊢ Eq (α := Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G ⟶ Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G')
    (Functor.map (bifunctorComp₁₂FunctorObj F₁₂) f ≫
      {
        app := fun (X₁ : C₁) ↦
          { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
            naturality := ⋯ },
        naturality := ⋯ })
    ({
        app := fun (X₁ : C₁) ↦
          { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
            naturality := ⋯ },
        naturality := ⋯ } ≫
      Functor.map (bifunctorComp₁₂FunctorObj F₁₂') f)
have w : ∀ (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
  Eq (α :=
    (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂).obj X₃ ⟶
      (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G').obj X₁).obj X₂).obj X₃)
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          (Functor.map (bifunctorComp₁₂FunctorObj F₁₂) f ≫
            {
              app := fun (X₁ : C₁) ↦
                {
                  app := fun (X₂ : C₂) ↦
                    { app := fun (X₃ : C₃) ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := sorry },
                  naturality := sorry },
              naturality := sorry })
          X₁)
        X₂)
      X₃)
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          ({
              app := fun (X₁ : C₁) ↦
                { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := sorry },
                  naturality := sorry },
              naturality := sorry } ≫
            Functor.map (bifunctorComp₁₂FunctorObj F₁₂') f)
          X₁)
        X₂)
      X₃)
Tactic: ext X₁ X₂ X₃