awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c_1 : Cocone G
hc : IsColimit c_1
s : Cocone (fiberwiseColimit G)
c : C
dsimp :
  CategoryStruct.comp (Y := c_1.pt)
      (colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c_1) :
        colimit (Grothendieck.ι F c ⋙ G) ⟶ (Cocone.whisker (Grothendieck.ι F c) c_1).pt)
      (hc.desc
        { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }) =
    s.ι.app c
⊢ CategoryStruct.comp (Y :=
      obj.{v₁, v₂, u₁, u₂} (obj (const C) (Cocone.pt (F := fiberwiseColimit G) (coconeFiberwiseColimitOfCocone c_1))) c)
      (NatTrans.app (Cocone.ι (coconeFiberwiseColimitOfCocone c_1)) c)
      (hc.desc
        { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }) =
    s.ι.app c

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c_1 : Cocone G
hc : IsColimit c_1
s : Cocone (fiberwiseColimit G)
c : C
w :
  ∀ (j : (↑(F.obj c) : Type u_1)),
    CategoryStruct.comp (Y := colimit (Grothendieck.ι F c ⋙ G)) (colimit.ι (Grothendieck.ι F c ⋙ G) j)
        (CategoryStruct.comp (Y := c_1.pt)
          (colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c_1) :
            colimit (Grothendieck.ι F c ⋙ G) ⟶ (Cocone.whisker (Grothendieck.ι F c) c_1).pt)
          (hc.desc
            { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι })) =
      colimit.ι (Grothendieck.ι F c ⋙ G) j ≫ s.ι.app c
⊢ CategoryStruct.comp (Y := c_1.pt)
      (colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c_1) :
        colimit (Grothendieck.ι F c ⋙ G) ⟶ (Cocone.whisker (Grothendieck.ι F c) c_1).pt)
      (hc.desc
        { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }) =
    s.ι.app c

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c_1 : Cocone G
hc : IsColimit c_1
s : Cocone (fiberwiseColimit G)
c : C
j : (↑(F.obj c) : Type u_1)
⊢ CategoryStruct.comp (Y := colimit (Grothendieck.ι F c ⋙ G)) (colimit.ι (Grothendieck.ι F c ⋙ G) j)
      (CategoryStruct.comp (Y := c_1.pt)
        (colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c_1) :
          colimit (Grothendieck.ι F c ⋙ G) ⟶ (Cocone.whisker (Grothendieck.ι F c) c_1).pt)
        (hc.desc
          { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι })) =
    colimit.ι (Grothendieck.ι F c ⋙ G) j ≫ s.ι.app c

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
hc : IsColimit c
s : Cocone (fiberwiseColimit G)
m : Cocone.pt (F := fiberwiseColimit G) (coconeFiberwiseColimitOfCocone c) ⟶ s.pt
hm : ∀ (j : C), NatTrans.app (Cocone.ι (coconeFiberwiseColimitOfCocone c)) j ≫ m = s.ι.app j
X : Grothendieck F
⊢ Eq (α := (fiberwiseColimit G).obj X.base ⟶ s.pt)
    (NatTrans.app (Cocone.ι (coconeFiberwiseColimitOfCocone c)) X.base ≫ m) (s.ι.app X.base)

Tactic:
have := hm X.base
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
hc : IsColimit c
s : Cocone (fiberwiseColimit G)
m : Cocone.pt (F := fiberwiseColimit G) (coconeFiberwiseColimitOfCocone c) ⟶ s.pt
hm : ∀ (j : C), NatTrans.app (Cocone.ι (coconeFiberwiseColimitOfCocone c)) j ≫ m = s.ι.app j
X : Grothendieck F
this :
  Eq (α := (fiberwiseColimit G).obj X.base ⟶ s.pt)
    (NatTrans.app (Cocone.ι (coconeFiberwiseColimitOfCocone c)) X.base ≫ m) (s.ι.app X.base)
simp :
  c.ι.app X ≫ m =
    CategoryStruct.comp (Y := (fiberwiseColimit G).obj X.base) (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber)
      (s.ι.app X.base)
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }

Tactic:
simp only [Functor.const_obj_obj, IsColimit.fac, NatTrans.comp_app, Functor.comp_obj,
      Grothendieck.forget_obj, natTransIntoForgetCompFiberwiseColimit_app,
      whiskerLeft_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Grothendieck.forget_obj, CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit_app, CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
hc : IsColimit c
s : Cocone (fiberwiseColimit G)
m : Cocone.pt (F := fiberwiseColimit G) (coconeFiberwiseColimitOfCocone c) ⟶ s.pt
hm : ∀ (j : C), NatTrans.app (Cocone.ι (coconeFiberwiseColimitOfCocone c)) j ≫ m = s.ι.app j
X : Grothendieck F
this :
  Eq (α := (fiberwiseColimit G).obj X.base ⟶ s.pt)
    (colimit.desc (Grothendieck.ι F X.base ⋙ G) (Cocone.whisker (Grothendieck.ι F X.base) c) ≫ m) (s.ι.app X.base)
⊢ c.ι.app X ≫ m =
    CategoryStruct.comp (Y := (fiberwiseColimit G).obj X.base) (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber)
      (s.ι.app X.base)

Tactic:
simp [← this]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
simp :
  G.map { base := f, fiber := g : X.Hom Y } ≫
      CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) =
    CategoryStruct.comp (Y := colimit (J := (↑(F.obj X.base) : Type u_1)) (Grothendieck.ι F X.base ⋙ G))
      (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber) (c.ι.app X.base)
⊢ G.map { base := f, fiber := g : X.Hom Y } ≫
      CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) =
    CategoryStruct.comp (Y := colimit (J := (↑(F.obj X.base) : Type u_1)) (Grothendieck.ι F X.base ⋙ G))
        (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber) (c.ι.app X.base) ≫
      map (obj (const (Grothendieck F)) c.pt) { base := f, fiber := g }

Tactic:
simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
rw :
  CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
      (G.map { base := f, fiber := g : X.Hom Y } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) =
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ (fiberwiseColimit G).map f) ≫ c.ι.app Y.base
⊢ G.map { base := f, fiber := g : X.Hom Y } ≫
      CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) =
    CategoryStruct.comp (Y := colimit (J := (↑(F.obj X.base) : Type u_1)) (Grothendieck.ι F X.base ⋙ G))
      (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber) (c.ι.app X.base)

Tactic:
rw [← Category.assoc, ← c.w f, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
simp :
  Eq (α := G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (G.map { base := f, fiber := g : X.Hom Y } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (G.map (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber) ≫
          colimit.ι (Grothendieck.ι F Y.base ⋙ G) ((F.map f).toFunctor.obj X.fiber))
        (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)
⊢ CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
      (G.map { base := f, fiber := g : X.Hom Y } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) =
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ (fiberwiseColimit G).map f) ≫ c.ι.app Y.base

Tactic:
simp only [fiberwiseColimit_obj, fiberwiseColimit_map, ι_colimMap_assoc,
            Functor.comp_obj, Grothendieck.ι_obj, NatTrans.comp_app, whiskerRight_app,
            Functor.associator_hom_app, Category.comp_id, colimit.ι_pre]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.fiberwiseColimit_map, CategoryTheory.Limits.fiberwiseColimit_obj, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Limits.colimit.ι_pre, CategoryTheory.Category.comp_id, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Grothendieck.ι_obj, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
rw :
  Eq (α := G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (G.map { base := f, fiber := g : X.Hom Y } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (CategoryStruct.comp (Y := obj (Grothendieck.ι F Y.base ⋙ G) Y.fiber)
          (G.map (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber ≫ map (Grothendieck.ι F Y.base) g))
          (colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber))
        (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)
⊢ Eq (α := G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (G.map { base := f, fiber := g : X.Hom Y } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (G.map (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber) ≫
          colimit.ι (Grothendieck.ι F Y.base ⋙ G) ((F.map f).toFunctor.obj X.fiber))
        (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)

Tactic:
rw [← colimit.w _ g, ← Category.assoc, Functor.comp_map, ← G.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.colimit.w, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
e_a :
  f = (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).base ≫ Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g)
e_a₁ :
  HEq g (β :=
    obj
        (Cat.Hom.toFunctor
          (F.map
            ((NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).base ≫
              Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g))))
        { base := X.base, fiber := X.fiber : Grothendieck F }.fiber ⟶
      (obj (Grothendieck.ι F Y.base) Y.fiber).fiber)
    (eqToHom ⋯ ≫
      map (Cat.Hom.toFunctor (F.map (Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g))))
          (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).fiber ≫
        Grothendieck.Hom.fiber (map (Grothendieck.ι F Y.base) g))
⊢ Eq (α := G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (G.map { base := f, fiber := g : X.Hom Y } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (CategoryStruct.comp (Y := obj (Grothendieck.ι F Y.base ⋙ G) Y.fiber)
          (G.map (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber ≫ map (Grothendieck.ι F Y.base) g))
          (colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber))
        (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ f = (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).base ≫ Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ HEq g (β :=
    obj
        (Cat.Hom.toFunctor
          (F.map
            ((NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).base ≫
              Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g))))
        { base := X.base, fiber := X.fiber : Grothendieck F }.fiber ⟶
      (obj (Grothendieck.ι F Y.base) Y.fiber).fiber)
    (eqToHom ⋯ ≫
      map (Cat.Hom.toFunctor (F.map (Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g))))
          (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).fiber ≫
        Grothendieck.Hom.fiber (map (Grothendieck.ι F Y.base) g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
hm : ∀ (j : Grothendieck F), (coconeOfCoconeFiberwiseColimit c).ι.app j ≫ m = s.ι.app j
X : C
simp : c.ι.app X ≫ m = colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s)
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc
        { pt := s.pt,
          ι :=
            { app := fun (X : C) ↦ colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s),
              naturality := ⋯ } }

Tactic:
simp only [fiberwiseColimit_obj, Functor.const_obj_obj, IsColimit.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.fiberwiseColimit_obj, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
hm : ∀ (j : Grothendieck F), (coconeOfCoconeFiberwiseColimit c).ι.app j ≫ m = s.ι.app j
X : C
⊢ ∀ (j : Grothendieck F),
    CategoryStruct.comp (Y := colimit (J := (↑(F.obj j.base) : Type u_1)) (Grothendieck.ι F j.base ⋙ G))
        (colimit.ι (Grothendieck.ι F j.base ⋙ G) j.fiber) (c.ι.app j.base ≫ m) =
      s.ι.app j

Tactic:
simp only [coconeOfCoconeFiberwiseColimit_pt, Functor.const_obj_obj,
      coconeOfCoconeFiberwiseColimit_ι_app, Category.assoc] at hm

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_pt, CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_ι_app, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
X : C
hm :
  ∀ (j : Grothendieck F),
    CategoryStruct.comp (Y := colimit (J := (↑(F.obj j.base) : Type u_1)) (Grothendieck.ι F j.base ⋙ G))
        (colimit.ι (Grothendieck.ι F j.base ⋙ G) j.fiber) (c.ι.app j.base ≫ m) =
      s.ι.app j
w :
  ∀ (d : (↑(F.obj X) : Type u_1)),
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ c.ι.app X ≫ m =
      CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
        (colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s))
⊢ c.ι.app X ≫ m = colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s)

Tactic:
ext d
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
X : C
hm :
  ∀ (j : Grothendieck F),
    CategoryStruct.comp (Y := colimit (J := (↑(F.obj j.base) : Type u_1)) (Grothendieck.ι F j.base ⋙ G))
        (colimit.ι (Grothendieck.ι F j.base ⋙ G) j.fiber) (c.ι.app j.base ≫ m) =
      s.ι.app j
d : (↑(F.obj X) : Type u_1)
⊢ colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ c.ι.app X ≫ m =
    CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
      (colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s))

Tactic:
simp [hm ⟨X, d⟩]

Premises used: CategoryTheory.Grothendieck.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst_3 : HasColimit (fiberwiseColimit G)
X : C
d : (↑(F.obj X) : Type u_1)
⊢ Eq (α := (Grothendieck.ι F X ⋙ G).obj d ⟶ colimit G)
    (colimit.ι (Grothendieck.ι F X ⋙ G) d ≫
        CategoryStruct.comp (Y := colimit (fiberwiseColimit G)) (colimit.ι (fiberwiseColimit G) X)
          (Iso.hom (colimitFiberwiseColimitIso G)) :
      (Grothendieck.ι F X ⋙ G).obj d ⟶ colimit G)
    (colimit.ι G { base := X, fiber := d } : G.obj { base := X, fiber := d : Grothendieck F } ⟶ colimit G)

Tactic:
simp [colimitFiberwiseColimitIso]

Premises used: CategoryTheory.Limits.colimitFiberwiseColimitIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst_3 : HasColimit (fiberwiseColimit G)
X : Grothendieck F
rw :
  Eq (α := G.obj X ⟶ colimit G) (colimit.ι G X : G.obj X ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (fiberwiseColimit G))
        (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base)
        (Iso.hom (colimitFiberwiseColimitIso G)) :
      G.obj X ⟶ colimit G)
⊢ Eq (α := G.obj X ⟶ colimit (fiberwiseColimit G)) (colimit.ι G X ≫ Iso.inv (colimitFiberwiseColimitIso G))
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base)

Tactic:
rw [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst_3 : HasColimit (fiberwiseColimit G)
X : Grothendieck F
⊢ Eq (α := G.obj X ⟶ colimit G) (colimit.ι G X : G.obj X ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (fiberwiseColimit G))
        (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base)
        (Iso.hom (colimitFiberwiseColimitIso G)) :
      G.obj X ⟶ colimit G)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
X Y : Grothendieck F ⥤ H
x : X ⟶ Y
w :
  ∀ (j : C),
    Eq (α := (obj (fiberwiseColim F H) X).obj j ⟶ obj colim Y)
      (CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
        (map (fiberwiseColim F H ⋙ colim) x ≫
          Iso.hom
            ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
              Y)))
      (CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
        (Iso.hom
            ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
              X) ≫
          map colim x))
⊢ Eq (α := obj (fiberwiseColim F H ⋙ colim) X ⟶ obj colim Y)
    (map (fiberwiseColim F H ⋙ colim) x ≫
      Iso.hom
        ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G)) Y))
    (Iso.hom
        ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G)) X) ≫
      map colim x)

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext