awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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.{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)
have 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 β)))
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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))
have 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)
Tactic: rw [← colimit.w (Grothendieck.ι F _ ⋙ G) f.fiber]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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)
have 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))
Tactic: simp only [← Category.assoc, Functor.comp_obj, Functor.comp_map, ← G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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))
have e_a : f = NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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 = NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber
have e_a : eqToHom sorry ≫ f.fiber =
  Grothendieck.Hom.fiber
    (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber)
Tactic: apply Grothendieck.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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)
⊢ f = NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber
have e_a₁ : f.base =
  Grothendieck.Hom.base (NatTrans.app (Grothendieck.ιNatTrans f.base) x.fiber ≫ map (Grothendieck.ι F x_1.base) f.fiber)
Tactic: apply Grothendieck.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (hypothesis)
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
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }
have this : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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)
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }
have 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)
Tactic: simp only [Functor.const_obj_obj, IsColimit.fac, NatTrans.comp_app, Functor.comp_obj,
      Grothendieck.forget_obj, natTransIntoForgetCompFiberwiseColimit_app,
      whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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 }
have 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)
Tactic: simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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)
have 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
Tactic: rw [← Category.assoc, ← c.w f, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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)
have 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)
Tactic: rw [← colimit.w _ g, ← Category.assoc, Functor.comp_map, ← G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
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
⊢ 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)
have e_a : f = (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).base ≫ Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g)
Tactic: congr