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 : C
d : (↑(F.obj X) : Type u_1)
⊢ (Grothendieck.ι F X).obj d = (Grothendieck.ι F X).obj ((F.map (𝟙 X)).toFunctor.obj d)

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 : C
d : (↑(F.obj X) : Type u_1)
w :
  Eq (α := G.obj { base := X, fiber := d : Grothendieck F } ⟶ colimit (Grothendieck.ι F X ⋙ G))
    (CategoryStruct.comp (Y := G.obj { base := X, fiber := (F.map (𝟙 X)).toFunctor.obj d })
      (G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) })
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := (Grothendieck.ι F X ⋙ G).obj ((F.map (𝟙 X)).toFunctor.obj d))
      (G.map
        { base := eqToHom ⋯,
          fiber :=
            (eqToHom ⋯ :
              obj (Cat.Hom.toFunctor (F.map (eqToHom ⋯))) ((Grothendieck.ι F X).obj d).fiber ⟶
                ((Grothendieck.ι F X).obj ((F.map (𝟙 X)).toFunctor.obj d)).fiber) })
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
⊢ Eq (α := G.obj { base := X, fiber := d : Grothendieck F } ⟶ colimit (Grothendieck.ι F X ⋙ G))
    (CategoryStruct.comp (Y := G.obj { base := X, fiber := (F.map (𝟙 X)).toFunctor.obj d })
      (G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) })
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := (Grothendieck.ι F X ⋙ G).obj ((F.map (𝟙 X)).toFunctor.obj d)) (eqToHom ⋯)
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))

Tactic:
rw [← eqToHom_map G (by simp), Grothendieck.eqToHom_eq]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.Grothendieck.eqToHom_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)
X : C
d : (↑(F.obj X) : Type u_1)
⊢ Eq (α := G.obj { base := X, fiber := d : Grothendieck F } ⟶ colimit (Grothendieck.ι F X ⋙ G))
    (CategoryStruct.comp (Y := G.obj { base := X, fiber := (F.map (𝟙 X)).toFunctor.obj d })
      (G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) })
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := (Grothendieck.ι F X ⋙ G).obj ((F.map (𝟙 X)).toFunctor.obj d))
      (G.map
        { base := eqToHom ⋯,
          fiber :=
            (eqToHom ⋯ :
              obj (Cat.Hom.toFunctor (F.map (eqToHom ⋯))) ((Grothendieck.ι F X).obj d).fiber ⟶
                ((Grothendieck.ι F X).obj ((F.map (𝟙 X)).toFunctor.obj d)).fiber) })
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))

Tactic:
rfl
-- 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
w :
  ∀ (d : (↑(F.obj X) : Type u_1)),
    Eq (α := (Grothendieck.ι F X ⋙ G).obj d ⟶ colimit (Grothendieck.ι F Z ⋙ G))
      (CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
        (CategoryStruct.comp (Y := colimit ((F.map (f ≫ g)).toFunctor ⋙ Grothendieck.ι F Z ⋙ G))
          (colimMap
            (whiskerRight (Grothendieck.ιNatTrans (f ≫ g)) G ≫
              ((F.map (f ≫ g)).toFunctor.associator (Grothendieck.ι F Z) G).hom))
          (colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map (f ≫ g)).toFunctor)))
      (CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
        (CategoryStruct.comp (Y := colimit (Grothendieck.ι F Y ⋙ G))
          (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G))
            (colimMap
              (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F Y) G).hom))
            (colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f).toFunctor))
          (CategoryStruct.comp (Y := colimit ((F.map g).toFunctor ⋙ Grothendieck.ι F Z ⋙ G))
            (colimMap
              (whiskerRight (Grothendieck.ιNatTrans g) G ≫ ((F.map g).toFunctor.associator (Grothendieck.ι F Z) G).hom))
            (colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map g).toFunctor))))
⊢ Eq (α := colimit (Grothendieck.ι F X ⋙ G) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := colimit ((F.map (f ≫ g)).toFunctor ⋙ Grothendieck.ι F Z ⋙ G))
      (colimMap
        (whiskerRight (Grothendieck.ιNatTrans (f ≫ g)) G ≫
          ((F.map (f ≫ g)).toFunctor.associator (Grothendieck.ι F Z) G).hom))
      (colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map (f ≫ g)).toFunctor))
    (CategoryStruct.comp (Y := colimit (Grothendieck.ι F Y ⋙ G))
      (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G))
        (colimMap
          (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F Y) G).hom))
        (colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f).toFunctor))
      (CategoryStruct.comp (Y := colimit ((F.map g).toFunctor ⋙ Grothendieck.ι F Z ⋙ G))
        (colimMap
          (whiskerRight (Grothendieck.ιNatTrans g) G ≫ ((F.map g).toFunctor.associator (Grothendieck.ι F Z) G).hom))
        (colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map g).toFunctor)))

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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
w :
  Eq (α := G.obj ((Grothendieck.ι F X).obj d) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)))
      (G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)))
      (G.map { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))))
        (G.map
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) })
        (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))))
⊢ Eq (α := (Grothendieck.ι F X ⋙ G).obj d ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
      (CategoryStruct.comp (Y := colimit ((F.map (f ≫ g)).toFunctor ⋙ Grothendieck.ι F Z ⋙ G))
        (colimMap
          (whiskerRight (Grothendieck.ιNatTrans (f ≫ g)) G ≫
            ((F.map (f ≫ g)).toFunctor.associator (Grothendieck.ι F Z) G).hom))
        (colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map (f ≫ g)).toFunctor)))
    (CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
      (CategoryStruct.comp (Y := colimit (Grothendieck.ι F Y ⋙ G))
        (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G))
          (colimMap
            (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F Y) G).hom))
          (colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f).toFunctor))
        (CategoryStruct.comp (Y := colimit ((F.map g).toFunctor ⋙ Grothendieck.ι F Z ⋙ G))
          (colimMap
            (whiskerRight (Grothendieck.ιNatTrans g) G ≫ ((F.map g).toFunctor.associator (Grothendieck.ι F Z) G).hom))
          (colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map g).toFunctor))))

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

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_pre_assoc, CategoryTheory.Grothendieck.ιNatTrans, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Limits.colimit.ι_pre, CategoryTheory.Category.comp_id, CategoryTheory.Functor.whiskerRight_app, 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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
w :
  Eq (α := G.obj ((Grothendieck.ι F X).obj d) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)))
      (G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))))
      (G.map
        (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
          { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }))
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))))
⊢ Eq (α := G.obj ((Grothendieck.ι F X).obj d) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)))
      (G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)))
      (G.map { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))))
        (G.map
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) })
        (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))))

Tactic:
rw [← Category.assoc, ← G.map_comp]

Premises used: CategoryTheory.Category.assoc, 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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
⊢ (F.map (f ≫ g)).toFunctor.obj d = (F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
rw :
  G.map
      (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
        { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
        { base := g,
          fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
    CategoryStruct.comp (Y := (Grothendieck.ι F Z ⋙ G).obj ((F.map (f ≫ g)).toFunctor.obj d)) (eqToHom ⋯)
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d))
| CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))))
    (G.map
      (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
        { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
        { base := g,
          fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }))
    (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))

Tactic:
rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F Z ⋙ G)
      (j := (F.map (f ≫ g)).toFunctor.obj d) (by simp)]

Premises used: CategoryTheory.Grothendieck.ι, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.eqToHom_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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
w :
  Eq (α := G.obj ((Grothendieck.ι F X).obj d) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)))
      (G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
    (G.map
        (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
          { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
      CategoryStruct.comp (Y := (Grothendieck.ι F Z ⋙ G).obj ((F.map (f ≫ g)).toFunctor.obj d)) (eqToHom ⋯)
        (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
⊢ Eq (α := G.obj ((Grothendieck.ι F X).obj d) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)))
      (G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))))
      (G.map
        (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
          { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }))
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))))

Tactic:
conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F Z ⋙ G)
      (j := (F.map (f ≫ g)).toFunctor.obj d) (by simp)]

Premises used: CategoryTheory.Grothendieck.ι, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.eqToHom_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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
⊢ (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    (Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
w :
  Eq (α := G.obj ((Grothendieck.ι F X).obj d) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)))
      (G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := (Grothendieck.ι F Z ⋙ G).obj ((F.map (f ≫ g)).toFunctor.obj d))
      (G.map
        (CategoryStruct.comp (Y := (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
          (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
            { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
            { base := g,
              fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) })
          { base := eqToHom ⋯,
            fiber :=
              (eqToHom ⋯ :
                obj
                    (Cat.Hom.toFunctor (F.map (eqToHom ⋯)) :
                      Functor.{u_2, u_2, u_1, u_1}
                        (↑(F.obj
                              ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).base) :
                          Type u_1)
                        (↑(F.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).base) : Type u_1))
                    ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).fiber ⟶
                  ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).fiber) }))
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
⊢ Eq (α := G.obj ((Grothendieck.ι F X).obj d) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)))
      (G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
    (G.map
        (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
          { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
      CategoryStruct.comp (Y := (Grothendieck.ι F Z ⋙ G).obj ((F.map (f ≫ g)).toFunctor.obj d)) (eqToHom ⋯)
        (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))

Tactic:
rw [← Category.assoc, ← eqToHom_map G (by simp), ← G.map_comp, Grothendieck.eqToHom_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_map, CategoryTheory.Grothendieck.eqToHom_eq, 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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
⊢ Eq.{v₁ + 1} (α :=
    ((Grothendieck.ι F X).obj d).base ⟶ ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).base)
    (Grothendieck.Hom.base
      { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
    (Grothendieck.Hom.base
      (CategoryStruct.comp (Y := (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
        (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
          { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) })
        { base := eqToHom ⋯,
          fiber :=
            (eqToHom ⋯ :
              obj
                  (Cat.Hom.toFunctor (F.map (eqToHom ⋯)) :
                    Functor.{u_2, u_2, u_1, u_1}
                      (↑(F.obj ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).base) :
                        Type u_1)
                      (↑(F.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).base) : Type u_1))
                  ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).fiber ⟶
                ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).fiber) }))

Tactic:
simp only [eqToHom_refl, Category.assoc, Grothendieck.comp_base,
        Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Grothendieck.comp_base, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
enter : (F.map (𝟙 Z)).toFunctor.map (eqToHom ⋯)
| (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:
enter [2, 1]
-- 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 (𝟙 Z)).toFunctor.map (eqToHom ⋯)

Tactic:
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)
enter : eqToHom ⋯
| (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:
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