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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
w :
  Eq.{u_2 + 1} (α := (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (eqToHom ⋯ : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map (f ≫ g)).toFunctor.obj d)) (eqToHom ⋯)
        (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
          (eqToHom ⋯) (eqToHom ⋯)) :
      (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
⊢ Eq.{u_2 + 1} (α := (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (eqToHom ⋯ : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map (f ≫ g)).toFunctor.obj d)) (eqToHom ⋯)
        (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
          ((F.map (𝟙 Z)).toFunctor.map (eqToHom ⋯)) (eqToHom ⋯)) :
      (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)

Tactic:
conv_rhs => enter [2, 1]; rw [eqToHom_map (F.map (𝟙 Z)).toFunctor]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, CategoryTheory.Cat.Hom.toFunctor
-- 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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
rw : (eqToHom ⋯ : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
| (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map (f ≫ g)).toFunctor.obj d)) (eqToHom ⋯)
      (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
        (eqToHom ⋯) (eqToHom ⋯)) :
    (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)

Tactic:
rw [eqToHom_trans, eqToHom_trans]

Premises used: CategoryTheory.eqToHom_trans
-- 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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
conv_rhs :
  Eq.{u_2 + 1} (α := (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (eqToHom ⋯ : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map (f ≫ g)).toFunctor.obj d)) (eqToHom ⋯)
        (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
          (eqToHom ⋯) (eqToHom ⋯)) :
      (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
w :
  Eq.{u_2 + 1} (α := (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (eqToHom ⋯ : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (eqToHom ⋯ : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
⊢ Eq.{u_2 + 1} (α := (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (eqToHom ⋯ : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
    (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map (f ≫ g)).toFunctor.obj d)) (eqToHom ⋯)
        (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
          (eqToHom ⋯) (eqToHom ⋯)) :
      (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)

Tactic:
conv_rhs => rw [eqToHom_trans, eqToHom_trans]

Premises used: CategoryTheory.eqToHom_trans
-- 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 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
X Y : Grothendieck F ⥤ H
α : X ⟶ Y
c₁ c₂ : C
f : c₁ ⟶ c₂
w :
  ∀ (j : (↑(F.obj c₁) : Type u_1)),
    Eq (α := (Grothendieck.ι F c₁ ⋙ X).obj j ⟶ (fiberwiseColimit Y).obj c₂)
      (colimit.ι (Grothendieck.ι F c₁ ⋙ X) j ≫
        (fiberwiseColimit X).map f ≫ map colim ((Grothendieck.ι F c₂).whiskerLeft α))
      (CategoryStruct.comp (Y := colimit (Grothendieck.ι F c₁ ⋙ X)) (colimit.ι (Grothendieck.ι F c₁ ⋙ X) j)
        (map colim ((Grothendieck.ι F c₁).whiskerLeft α) ≫ (fiberwiseColimit Y).map f))
⊢ Eq (α := (fiberwiseColimit X).obj c₁ ⟶ (fiberwiseColimit Y).obj c₂)
    ((fiberwiseColimit X).map f ≫ map colim ((Grothendieck.ι F c₂).whiskerLeft α))
    (map colim ((Grothendieck.ι F c₁).whiskerLeft α) ≫ (fiberwiseColimit Y).map f)

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_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)
inst_3 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
X Y : Grothendieck F ⥤ H
α : X ⟶ Y
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ ∀ (j : (↑(F.obj c₁) : Type u_1)),
    Eq (α := (Grothendieck.ι F c₁ ⋙ X).obj j ⟶ (fiberwiseColimit Y).obj c₂)
      (colimit.ι (Grothendieck.ι F c₁ ⋙ X) j ≫
        (fiberwiseColimit X).map f ≫ map colim ((Grothendieck.ι F c₂).whiskerLeft α))
      (CategoryStruct.comp (Y := colimit (Grothendieck.ι F c₁ ⋙ X)) (colimit.ι (Grothendieck.ι F c₁ ⋙ X) j)
        (map colim ((Grothendieck.ι F c₁).whiskerLeft α) ≫ (fiberwiseColimit Y).map f))

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_1 : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G_1)
inst_3 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
G : Grothendieck F ⥤ H
w :
  ∀ (x : C),
    NatTrans.app { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ } x =
      NatTrans.app (𝟙 (fiberwiseColimit G)) x
⊢ { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ } = 𝟙 (fiberwiseColimit G)

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_1 : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G_1)
inst_3 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
G : Grothendieck F ⥤ H
x : C
w : colimMap (𝟙 (Grothendieck.ι F x ⋙ G)) = 𝟙 (colimit (Grothendieck.ι F x ⋙ G))
⊢ NatTrans.app { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ } x =
    NatTrans.app (𝟙 (fiberwiseColimit G)) x

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_1 : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G_1)
inst_3 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
G : Grothendieck F ⥤ H
x : C
⊢ colimMap (𝟙 (Grothendieck.ι F x ⋙ G)) = 𝟙 (colimit (Grothendieck.ι F x ⋙ G))

Tactic:
apply Functor.map_id colim

Premises used: CategoryTheory.Limits.colim, CategoryTheory.Functor.map_id
-- 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 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
X Y Z : Grothendieck F ⥤ H
α : X ⟶ Y
β : Y ⟶ Z
w :
  ∀ (x : C),
    Eq.{v₂ + 1} (α := (fiberwiseColimit X).obj x ⟶ (fiberwiseColimit Z).obj x)
      (NatTrans.app { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ } x)
      (NatTrans.app
        (CategoryStruct.comp (Y := fiberwiseColimit Y)
          { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ }
          { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ })
        x)
⊢ Eq (α := fiberwiseColimit X ⟶ fiberwiseColimit Z)
    { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ }
    (CategoryStruct.comp (Y := fiberwiseColimit Y)
      { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ }
      { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ })

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)
inst_3 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
X Y Z : Grothendieck F ⥤ H
α : X ⟶ Y
β : Y ⟶ Z
x : C
w :
  Eq (α := colimit (Grothendieck.ι F x ⋙ X) ⟶ colimit (Grothendieck.ι F x ⋙ Z))
    (colimMap ((Grothendieck.ι F x).whiskerLeft α ≫ (Grothendieck.ι F x).whiskerLeft β))
    (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x ⋙ Y)) (colimMap ((Grothendieck.ι F x).whiskerLeft α))
      (colimMap ((Grothendieck.ι F x).whiskerLeft β)))
⊢ Eq.{v₂ + 1} (α := (fiberwiseColimit X).obj x ⟶ (fiberwiseColimit Z).obj x)
    (NatTrans.app { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ } x)
    (NatTrans.app
      (CategoryStruct.comp (Y := fiberwiseColimit Y)
        { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ }
        { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ })
      x)

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)
inst_3 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
X Y Z : Grothendieck F ⥤ H
α : X ⟶ Y
β : Y ⟶ Z
x : C
⊢ Eq (α := colimit (Grothendieck.ι F x ⋙ X) ⟶ colimit (Grothendieck.ι F x ⋙ Z))
    (colimMap ((Grothendieck.ι F x).whiskerLeft α ≫ (Grothendieck.ι F x).whiskerLeft β))
    (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x ⋙ Y)) (colimMap ((Grothendieck.ι F x).whiskerLeft α))
      (colimMap ((Grothendieck.ι F x).whiskerLeft β)))

Tactic:
apply Functor.map_comp colim

Premises used: CategoryTheory.Limits.colim, CategoryTheory.Functor.map_comp
-- 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)
x x_1 : Grothendieck F
f : x ⟶ x_1
simp :
  Eq (α := G.obj x ⟶ colimit (J := (↑(F.obj x_1.base) : Type u_1)) (Grothendieck.ι F x_1.base ⋙ G))
    (G.map f ≫ colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber)
    (G.map (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber) ≫
      colimit.ι (Grothendieck.ι F x_1.base ⋙ G) ((F.map f.base).toFunctor.obj x.fiber))
⊢ G.map f ≫ colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber =
    colimit.ι (Grothendieck.ι F x.base ⋙ G) x.fiber ≫ (Grothendieck.forget F ⋙ fiberwiseColimit G).map f

Tactic:
simp only [Functor.comp_obj, Grothendieck.forget_obj, fiberwiseColimit_obj, Functor.comp_map,
      Grothendieck.forget_map, fiberwiseColimit_map, ι_colimMap_assoc, 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.Grothendieck.forget_obj, CategoryTheory.Category.comp_id, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Grothendieck.ι_obj, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.comp_map, CategoryTheory.Grothendieck.forget_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)
x x_1 : Grothendieck F
f : x ⟶ x_1
rw :
  Eq (α := G.obj x ⟶ colimit (J := (↑(F.obj x_1.base) : Type u_1)) (Grothendieck.ι F x_1.base ⋙ G))
    (G.map f ≫ colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber)
    (G.map (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber) ≫
      map (Grothendieck.ι F x_1.base ⋙ G) f.fiber ≫ colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber)
⊢ Eq (α := G.obj x ⟶ colimit (J := (↑(F.obj x_1.base) : Type u_1)) (Grothendieck.ι F x_1.base ⋙ G))
    (G.map f ≫ colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber)
    (G.map (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber) ≫
      colimit.ι (Grothendieck.ι F x_1.base ⋙ G) ((F.map f.base).toFunctor.obj x.fiber))

Tactic:
rw [← colimit.w (Grothendieck.ι F _ ⋙ G) f.fiber]

Premises used: CategoryTheory.Grothendieck.ι, CategoryTheory.Functor.comp, CategoryTheory.Grothendieck.Hom.fiber, CategoryTheory.Limits.colimit.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)
x x_1 : Grothendieck F
f : x ⟶ x_1
simp :
  Eq (α := G.obj x ⟶ colimit (J := (↑(F.obj x_1.base) : Type u_1)) (Grothendieck.ι F x_1.base ⋙ G))
    (G.map f ≫ colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber)
    (CategoryStruct.comp (Y := G.obj (obj (Grothendieck.ι F x_1.base) x_1.fiber))
      (G.map (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber))
      (colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber))
⊢ Eq (α := G.obj x ⟶ colimit (J := (↑(F.obj x_1.base) : Type u_1)) (Grothendieck.ι F x_1.base ⋙ G))
    (G.map f ≫ colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber)
    (G.map (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber) ≫
      map (Grothendieck.ι F x_1.base ⋙ G) f.fiber ≫ colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber)

Tactic:
simp only [← Category.assoc, Functor.comp_obj, Functor.comp_map, ← G.map_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, 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)
x x_1 : Grothendieck F
f : x ⟶ x_1
e_a : f = NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber
⊢ Eq (α := G.obj x ⟶ colimit (J := (↑(F.obj x_1.base) : Type u_1)) (Grothendieck.ι F x_1.base ⋙ G))
    (G.map f ≫ colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber)
    (CategoryStruct.comp (Y := G.obj (obj (Grothendieck.ι F x_1.base) x_1.fiber))
      (G.map (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber))
      (colimit.ι (Grothendieck.ι F x_1.base ⋙ G) x_1.fiber))

Tactic:
congr 2
-- 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)
x x_1 : Grothendieck F
f : x ⟶ x_1
e_a :
  eqToHom ⋯ ≫ f.fiber =
    Grothendieck.Hom.fiber
      (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber)
e_a₁ :
  f.base =
    Grothendieck.Hom.base
      (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber)
⊢ f = NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber

Tactic:
apply Grothendieck.ext

Premises used: CategoryTheory.Grothendieck.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)
x x_1 : Grothendieck F
f : x ⟶ x_1
⊢ eqToHom ⋯ ≫ f.fiber =
    Grothendieck.Hom.fiber
      (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber)

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)
x x_1 : Grothendieck F
f : x ⟶ x_1
⊢ f.base =
    Grothendieck.Hom.base
      (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber)

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
x x_1 : C
f : x ⟶ x_1
dsimp :
  Eq (α := colimit (Grothendieck.ι F x ⋙ G) ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x_1 ⋙ G))
        (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F x_1 ⋙ G))
          (colimMap
            (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F x_1) G).hom))
          (colimit.pre (Grothendieck.ι F x_1 ⋙ G) (F.map f).toFunctor))
        (colimit.desc (Grothendieck.ι F x_1 ⋙ G) (Cocone.whisker (Grothendieck.ι F x_1) c)) :
      colimit (Grothendieck.ι F x ⋙ G) ⟶ c.pt)
    (CategoryStruct.comp (Y := c.pt)
        (colimit.desc (Grothendieck.ι F x ⋙ G) (Cocone.whisker (Grothendieck.ι F x) c) :
          colimit (Grothendieck.ι F x ⋙ G) ⟶ (Cocone.whisker (Grothendieck.ι F x) c).pt)
        (𝟙 c.pt) :
      colimit (Grothendieck.ι F x ⋙ G) ⟶ c.pt)
⊢ Eq (α := (fiberwiseColimit G).obj x ⟶ obj.{v₁, v₂, u₁, u₂} (obj (const C) c.pt) x_1)
    ((fiberwiseColimit G).map f ≫ colimit.desc (Grothendieck.ι F x_1 ⋙ G) (Cocone.whisker (Grothendieck.ι F x_1) c) :
      (fiberwiseColimit G).obj x ⟶ obj.{v₁, v₂, u₁, u₂} (obj (const C) c.pt) x_1)
    (CategoryStruct.comp (Y := obj.{v₁, v₂, u₁, u₂} (obj (const C) c.pt) x)
        (colimit.desc (Grothendieck.ι F x ⋙ G) (Cocone.whisker (Grothendieck.ι F x) c) :
          colimit (Grothendieck.ι F x ⋙ G) ⟶ (Cocone.whisker (Grothendieck.ι F x) c).pt)
        (map (obj (const C) c.pt) f) :
      (fiberwiseColimit G).obj x ⟶ obj.{v₁, v₂, u₁, u₂} (obj (const C) c.pt) x_1)

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 : Cocone G
x x_1 : C
f : x ⟶ x_1
w :
  ∀ (j : (↑(F.obj x) : Type u_1)),
    Eq (α := (Grothendieck.ι F x ⋙ G).obj j ⟶ c.pt)
      (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x ⋙ G)) (colimit.ι (Grothendieck.ι F x ⋙ G) j)
          (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x_1 ⋙ G))
            (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F x_1 ⋙ G))
              (colimMap
                (whiskerRight (Grothendieck.ιNatTrans f) G ≫
                  ((F.map f).toFunctor.associator (Grothendieck.ι F x_1) G).hom))
              (colimit.pre (Grothendieck.ι F x_1 ⋙ G) (F.map f).toFunctor))
            (colimit.desc (Grothendieck.ι F x_1 ⋙ G) (Cocone.whisker (Grothendieck.ι F x_1) c))) :
        (Grothendieck.ι F x ⋙ G).obj j ⟶ c.pt)
      (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x ⋙ G)) (colimit.ι (Grothendieck.ι F x ⋙ G) j)
          (CategoryStruct.comp (Y := c.pt)
            (colimit.desc (Grothendieck.ι F x ⋙ G) (Cocone.whisker (Grothendieck.ι F x) c) :
              colimit (Grothendieck.ι F x ⋙ G) ⟶ (Cocone.whisker (Grothendieck.ι F x) c).pt)
            (𝟙 c.pt)) :
        (Grothendieck.ι F x ⋙ G).obj j ⟶ c.pt)
⊢ Eq (α := colimit (Grothendieck.ι F x ⋙ G) ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x_1 ⋙ G))
        (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F x_1 ⋙ G))
          (colimMap
            (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F x_1) G).hom))
          (colimit.pre (Grothendieck.ι F x_1 ⋙ G) (F.map f).toFunctor))
        (colimit.desc (Grothendieck.ι F x_1 ⋙ G) (Cocone.whisker (Grothendieck.ι F x_1) c)) :
      colimit (Grothendieck.ι F x ⋙ G) ⟶ c.pt)
    (CategoryStruct.comp (Y := c.pt)
        (colimit.desc (Grothendieck.ι F x ⋙ G) (Cocone.whisker (Grothendieck.ι F x) c) :
          colimit (Grothendieck.ι F x ⋙ G) ⟶ (Cocone.whisker (Grothendieck.ι F x) c).pt)
        (𝟙 c.pt) :
      colimit (Grothendieck.ι F x ⋙ G) ⟶ c.pt)

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 : Cocone G
x x_1 : C
f : x ⟶ x_1
j : (↑(F.obj x) : Type u_1)
⊢ Eq (α := (Grothendieck.ι F x ⋙ G).obj j ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x ⋙ G)) (colimit.ι (Grothendieck.ι F x ⋙ G) j)
        (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x_1 ⋙ G))
          (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F x_1 ⋙ G))
            (colimMap
              (whiskerRight (Grothendieck.ιNatTrans f) G ≫
                ((F.map f).toFunctor.associator (Grothendieck.ι F x_1) G).hom))
            (colimit.pre (Grothendieck.ι F x_1 ⋙ G) (F.map f).toFunctor))
          (colimit.desc (Grothendieck.ι F x_1 ⋙ G) (Cocone.whisker (Grothendieck.ι F x_1) c))) :
      (Grothendieck.ι F x ⋙ G).obj j ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (Grothendieck.ι F x ⋙ G)) (colimit.ι (Grothendieck.ι F x ⋙ G) j)
        (CategoryStruct.comp (Y := c.pt)
          (colimit.desc (Grothendieck.ι F x ⋙ G) (Cocone.whisker (Grothendieck.ι F x) c) :
            colimit (Grothendieck.ι F x ⋙ G) ⟶ (Cocone.whisker (Grothendieck.ι F x) c).pt)
          (𝟙 c.pt)) :
      (Grothendieck.ι F x ⋙ G).obj j ⟶ c.pt)

Tactic:
simp