awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
dsimp : bi ⟶ bi
⊢ base.{u₁, v₁, u_2, u_1} (F := G ⋙ F)
      (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f }) (T := pre F G)
        (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
          { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })) ⟶
    base.{u₁, v₁, u_2, u_1} (F := G ⋙ F)
      (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F }) (T := pre F G)
        { left := { as := PUnit.unit : Discrete PUnit.{1} },
          right := { base := bi, fiber := fi : Grothendieck (G ⋙ F) },
          hom :=
            { base := gbi, fiber := gfi :
              (obj (fromPUnit { base := d, fiber := f : Grothendieck F }) { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                ((pre F G).obj { base := bi, fiber := fi : Grothendieck (G ⋙ F) }) } :
          Comma (fromPUnit { base := d, fiber := f : Grothendieck F }) (pre F G) })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bi ⟶ bi

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((G ⋙ F).map (_root_.id (𝟙 bi))).toFunctor.obj
      (fiber
        (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F }) (T := pre F G)
          (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f : Grothendieck (G ⋙ F) })
            { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) :
              { base := d, fiber := f : Grothendieck F }.Hom
                ((pre F G).obj { base := bi, fiber := (F.map gbi).toFunctor.obj f : Grothendieck (G ⋙ F) }) }))) =
    (F.map gbi).toFunctor.obj f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ Eq (α :=
    { base := d, fiber := f : Grothendieck F }.base ⟶
      ((pre F G).obj
          (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F }) (T := pre F G)
            { left := { as := PUnit.unit : Discrete PUnit.{1} },
              right := { base := bi, fiber := fi : Grothendieck (G ⋙ F) },
              hom :=
                { base := gbi, fiber := gfi :
                  (obj (fromPUnit { base := d, fiber := f : Grothendieck F })
                        { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                    ((pre F G).obj { base := bi, fiber := fi : Grothendieck (G ⋙ F) }) } :
              Comma (fromPUnit { base := d, fiber := f : Grothendieck F }) (pre F G) })).base)
    (Hom.base
      (CategoryStruct.comp (Y :=
        (pre F G).obj
          (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f }) (T := pre F G)
            (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
              { base := gbi,
                fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })))
        (StructuredArrow.hom
          (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
            { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) }))
        ((pre F G).map { base := _root_.id (𝟙 bi), fiber := eqToHom ⋯ ≫ gfi })))
    (Hom.base
      (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bi, fiber := fi }, hom := { base := gbi, fiber := gfi } }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
out :
  Zigzag (J := StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G))
    (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
      { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })
    { left := { as := PUnit.unit }, right := { base := bj, fiber := fj }, hom := { base := gbj, fiber := gfj } }
⊢ Zigzag (J := StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G))
    { left := { as := PUnit.unit }, right := { base := bi, fiber := fi }, hom := { base := gbi, fiber := gfi } }
    { left := { as := PUnit.unit }, right := { base := bj, fiber := fj }, hom := { base := gbj, fiber := gfj } }

Tactic:
apply Zigzag.trans (j₂ := StructuredArrow.mk (Y := ⟨bi, ((F.map gbi).toFunctor.obj f)⟩)
      (Grothendieck.Hom.mk gbi (𝟙 _)))
    (.of_zag (.inr ⟨StructuredArrow.homMk (Grothendieck.Hom.mk (by dsimp; exact 𝟙 _)
      (eqToHom (by simp) ≫ gfi)) (by apply Grothendieck.ext <;> simp)⟩))

Premises used: CategoryTheory.StructuredArrow.homMk, Nonempty.intro, CategoryTheory.Zigzag.of_zag, CategoryTheory.Zigzag.trans, Or.inr
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
dsimp : bj ⟶ bj
⊢ base.{u₁, v₁, u_2, u_1} (F := G ⋙ F)
      (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f }) (T := pre F G)
        (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
          { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })) ⟶
    base.{u₁, v₁, u_2, u_1} (F := G ⋙ F)
      (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F }) (T := pre F G)
        { left := { as := PUnit.unit : Discrete PUnit.{1} },
          right := { base := bj, fiber := fj : Grothendieck (G ⋙ F) },
          hom :=
            { base := gbj, fiber := gfj :
              (obj (fromPUnit { base := d, fiber := f : Grothendieck F }) { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                ((pre F G).obj { base := bj, fiber := fj : Grothendieck (G ⋙ F) }) } :
          Comma (fromPUnit { base := d, fiber := f : Grothendieck F }) (pre F G) })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bj ⟶ bj

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((G ⋙ F).map (_root_.id (𝟙 bj))).toFunctor.obj
      (fiber
        (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F }) (T := pre F G)
          (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f : Grothendieck (G ⋙ F) })
            { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) :
              { base := d, fiber := f : Grothendieck F }.Hom
                ((pre F G).obj { base := bj, fiber := (F.map gbj).toFunctor.obj f : Grothendieck (G ⋙ F) }) }))) =
    (F.map gbj).toFunctor.obj f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ Eq (α :=
    { base := d, fiber := f : Grothendieck F }.base ⟶
      ((pre F G).obj
          (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F }) (T := pre F G)
            { left := { as := PUnit.unit : Discrete PUnit.{1} },
              right := { base := bj, fiber := fj : Grothendieck (G ⋙ F) },
              hom :=
                { base := gbj, fiber := gfj :
                  (obj (fromPUnit { base := d, fiber := f : Grothendieck F })
                        { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                    ((pre F G).obj { base := bj, fiber := fj : Grothendieck (G ⋙ F) }) } :
              Comma (fromPUnit { base := d, fiber := f : Grothendieck F }) (pre F G) })).base)
    (Hom.base
      (CategoryStruct.comp (Y :=
        (pre F G).obj
          (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f }) (T := pre F G)
            (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
              { base := gbj,
                fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })))
        (StructuredArrow.hom
          (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
            { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) }))
        ((pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj })))
    (Hom.base
      (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj }, hom := { base := gbj, fiber := gfj } }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
out :
  Zigzag (J := StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G))
    (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
      { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })
    (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
      { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })
⊢ Zigzag (J := StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G))
    (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
      { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })
    { left := { as := PUnit.unit }, right := { base := bj, fiber := fj }, hom := { base := gbj, fiber := gfj } }

Tactic:
refine Zigzag.trans (j₂ := StructuredArrow.mk (Y := ⟨bj, ((F.map gbj).toFunctor.obj f)⟩)
      (Grothendieck.Hom.mk gbj (𝟙 _))) ?_
    (.of_zag (.inl ⟨StructuredArrow.homMk (Grothendieck.Hom.mk (by dsimp; exact 𝟙 _)
      (eqToHom (by simp) ≫ gfj)) (by apply Grothendieck.ext <;> simp)⟩))

Premises used: CategoryTheory.StructuredArrow.homMk, Nonempty.intro, CategoryTheory.Zigzag.of_zag, Or.inl, CategoryTheory.Zigzag.trans
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ Zigzag (J := StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G))
    (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
      { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })
    (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
      { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })

Tactic:
zigzag_prefunctor_obj_of_zigzag (Grothendieck.structuredArrowToStructuredArrowPre F G d f)
    (isPreconnected_zigzag (.mk gbi) (.mk gbj))

Premises used: CategoryTheory.isPreconnected_zigzag, CategoryTheory.StructuredArrow.mk, CategoryTheory.Grothendieck.structuredArrowToStructuredArrowPre, CategoryTheory.zigzag_prefunctor_obj_of_zigzag
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ Zigzag (J := StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G))
    (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
      { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })
    (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
      { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })

Tactic:
exact zigzag_prefunctor_obj_of_zigzag (Grothendieck.structuredArrowToStructuredArrowPre F G d f)
    (isPreconnected_zigzag (.mk gbi) (.mk gbj))

Premises used: CategoryTheory.isPreconnected_zigzag, CategoryTheory.Grothendieck.structuredArrowToStructuredArrowPre, CategoryTheory.zigzag_prefunctor_obj_of_zigzag
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₂, max ?u.411012 ?u.411013, u₂, max (?u.411012 + 1) (?u.411013 + 1)} D Cat
G_1 : Functor.{v₁, v₂, u₁, u₂} C_1 D
C : Type u₁
inst_2 : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst_3 : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X Y : C
f : X ⟶ Y
d : (↑(F.obj X) : Type u₂)
⊢ Eq (α := (↑(G.obj Y) : Type u₂)) (obj (Cat.Hom.toFunctor (F.map f ≫ α.app Y)) d)
    (obj (Cat.Hom.toFunctor (α.app X ≫ G.map f)) d)

Tactic:
have := Functor.congr_obj congr($(α.naturality f).toFunctor) d
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₂, max ?u.411012 ?u.411013, u₂, max (?u.411012 + 1) (?u.411013 + 1)} D Cat
G_1 : Functor.{v₁, v₂, u₁, u₂} C_1 D
C : Type u₁
inst_2 : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst_3 : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X Y : C
f : X ⟶ Y
d : (↑(F.obj X) : Type u₂)
this : (α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d) = (G.map f).toFunctor.obj ((α.app X).toFunctor.obj d)
h :
  HEq.{v₂ + 1} (α :=
    (G.map f).toFunctor.obj { base := X, fiber := (α.app X).toFunctor.obj d : Grothendieck G }.fiber ⟶
      { base := Y, fiber := (α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d) }.fiber)
    (eqToHom ⋯ :
      (G.map f).toFunctor.obj ((α.app X).toFunctor.obj d) ⟶ (α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d))
    (β :=
    (G.map f).toFunctor.obj { base := X, fiber := (α.app X).toFunctor.obj d : Grothendieck G }.fiber ⟶
      { base := Y, fiber := (G.map f).toFunctor.obj ((α.app X).toFunctor.obj d) }.fiber)
    (𝟙 ((G.map f).toFunctor.obj ((α.app X).toFunctor.obj d)))
⊢ Eq (α := H.obj { base := X, fiber := (α.app X).toFunctor.obj d : Grothendieck G } ⟶ (fiberwiseColimit H).obj Y)
    (CategoryStruct.comp (Y := H.obj { base := Y, fiber := (α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d) })
      (H.map { base := f, fiber := eqToHom ⋯ })
      (colimit.ι (ι G Y ⋙ H) ((α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d))))
    (CategoryStruct.comp (Y := H.obj { base := Y, fiber := (G.map f).toFunctor.obj ((α.app X).toFunctor.obj d) })
      (H.map { base := f, fiber := 𝟙 ((G.map f).toFunctor.obj ((α.app X).toFunctor.obj d)) })
      (colimit.ι (ι G Y ⋙ H) ((G.map f).toFunctor.obj ((α.app X).toFunctor.obj d))))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₂, max ?u.411012 ?u.411013, u₂, max (?u.411012 + 1) (?u.411013 + 1)} D Cat
G_1 : Functor.{v₁, v₂, u₁, u₂} C_1 D
C : Type u₁
inst_2 : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst_3 : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X Y : C
f : X ⟶ Y
d : (↑(F.obj X) : Type u₂)
this : (α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d) = (G.map f).toFunctor.obj ((α.app X).toFunctor.obj d)
⊢ HEq.{v₂ + 1} (α :=
    (G.map f).toFunctor.obj { base := X, fiber := (α.app X).toFunctor.obj d : Grothendieck G }.fiber ⟶
      { base := Y, fiber := (α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d) }.fiber)
    (eqToHom ⋯ :
      (G.map f).toFunctor.obj ((α.app X).toFunctor.obj d) ⟶ (α.app Y).toFunctor.obj ((F.map f).toFunctor.obj d))
    (β :=
    (G.map f).toFunctor.obj { base := X, fiber := (α.app X).toFunctor.obj d : Grothendieck G }.fiber ⟶
      { base := Y, fiber := (G.map f).toFunctor.obj ((α.app X).toFunctor.obj d) }.fiber)
    (𝟙 ((G.map f).toFunctor.obj ((α.app X).toFunctor.obj d)))

Tactic:
apply eqToHom_heq_id_dom

Premises used: CategoryTheory.eqToHom_heq_id_dom
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
rw : ∀ (G_1 : Grothendieck G ⥤ Type u₁), IsIso (X := colimit (map α ⋙ G_1)) (Y := colimit G_1) (colimit.pre G_1 (map α))
⊢ (map α).Final

Tactic:
rw [final_iff_isIso_colimit_pre]

Premises used: CategoryTheory.Functor.final_iff_isIso_colimit_pre
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  Iso.trans (Y := colimit (fiberwiseColimit (map α ⋙ H))) (Iso.symm (colimitFiberwiseColimitIso (map α ⋙ H)))
    (Iso.trans (Y := colimit (fiberwiseColimit H)) (HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H))
      (colimitFiberwiseColimitIso H))
⊢ IsIso i.hom

Tactic:
Iso.isIso_hom i

Premises used: CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  Iso.trans (Y := colimit (fiberwiseColimit (map α ⋙ H))) (Iso.symm (colimitFiberwiseColimitIso (map α ⋙ H)))
    (Iso.trans (Y := colimit (fiberwiseColimit H)) (HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H))
      (colimitFiberwiseColimitIso H))
h : colimit.pre H (map α) = i.hom
⊢ IsIso (X := colimit (map α ⋙ H)) (Y := colimit H) (colimit.pre H (map α))

Tactic:
convert! Iso.isIso_hom i

Premises used: CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  Iso.trans (Y := colimit (fiberwiseColimit (map α ⋙ H))) (Iso.symm (colimitFiberwiseColimitIso (map α ⋙ H)))
    (Iso.trans (Y := colimit (fiberwiseColimit H)) (HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H))
      (colimitFiberwiseColimitIso H))
h :
  ∀ (j : Grothendieck F),
    CategoryStruct.comp (Y := colimit (map α ⋙ H)) (colimit.ι (map α ⋙ H) j) (colimit.pre H (map α)) =
      colimit.ι (map α ⋙ H) j ≫ i.hom
⊢ colimit.pre H (map α) = i.hom

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext