awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : C
h :
  ∀ (val : F.obj x),
    TypeCat.Fun.toFun (X := F.obj x ⊕ G.obj x)
        (hom (FC := TypeCat.Fun)
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
                (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
              (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
                (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x))))
        (Sum.inl val) =
      (hom (FC := TypeCat.Fun) (𝟙 (F.obj x ⊕ G.obj x))).toFun (Sum.inl val)
⊢ ↾Sum.map
        (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
          (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
        (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
          (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x)) =
    𝟙 (F.obj x ⊕ G.obj x)
have h₁ : ∀ (val : G.obj x),
  TypeCat.Fun.toFun (X := F.obj x ⊕ G.obj x)
      (hom (FC := TypeCat.Fun)
        (↾Sum.map
            (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
              (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
            (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
              (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x))))
      (Sum.inr val) =
    (hom (FC := TypeCat.Fun) (𝟙 (F.obj x ⊕ G.obj x))).toFun (Sum.inr val)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α := F.obj X ⊕ G.obj X ⟶ F.obj Z ⊕ G.obj Z)
    (↾Sum.map
        (⇑(hom (FC := TypeCat.Fun) (F.map (x ≫ x_1))) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Z))
        (⇑(hom (FC := TypeCat.Fun) (G.map (x ≫ x_1))) :
          (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Z)))
    (CategoryStruct.comp (Y := F.obj Y ⊕ G.obj Y)
      (↾Sum.map
          (⇑(hom (FC := TypeCat.Fun) (F.map x)) :
            (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
          (⇑(hom (FC := TypeCat.Fun) (G.map x)) :
            (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Y)))
      (↾Sum.map
          (⇑(hom (FC := TypeCat.Fun) (F.map x_1)) :
            (a : (fun (X : Type w) ↦ X) (F.obj Y)) → (fun (X : Type w) ↦ X) (F.obj Z))
          (⇑(hom (FC := TypeCat.Fun) (G.map x_1)) :
            (a : (fun (X : Type w) ↦ X) (G.obj Y)) → (fun (X : Type w) ↦ X) (G.obj Z))))
have h : ∀ (val : F.obj X),
  Eq (α := F.obj Z ⊕ G.obj Z)
    (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
      (hom (FC := TypeCat.Fun)
        (↾Sum.map
            (⇑(hom (FC := TypeCat.Fun) (F.map (x ≫ x_1))) :
              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Z))
            (⇑(hom (FC := TypeCat.Fun) (G.map (x ≫ x_1))) :
              (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Z))))
      (Sum.inl val))
    (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
      (hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := F.obj Y ⊕ G.obj Y)
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map x)) :
                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
              (⇑(hom (FC := TypeCat.Fun) (G.map x)) :
                (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Y)))
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map x_1)) :
                (a : (fun (X : Type w) ↦ X) (F.obj Y)) → (fun (X : Type w) ↦ X) (F.obj Z))
              (⇑(hom (FC := TypeCat.Fun) (G.map x_1)) :
                (a : (fun (X : Type w) ↦ X) (G.obj Y)) → (fun (X : Type w) ↦ X) (G.obj Z)))))
      (Sum.inl val))
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x x_1 : C
x_2 : x ⟶ x_1
⊢ (coprod F₁ F₂).map x_2 ≫
      ↾Sum.elim
          (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
            (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
          (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
            (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1)) =
    ↾Sum.elim
          (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
            (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
          (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
            (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
      F.map x_2
have h : ∀ (val : F₁.obj x),
  TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((coprod F₁ F₂).map x_2 ≫
          ↾Sum.elim
              (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
              (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
                (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))))
      (Sum.inl val) =
    TypeCat.Fun.toFun (X := (coprod F₁ F₂).obj x)
      (hom (FC := TypeCat.Fun)
        (↾Sum.elim
              (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
              (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
                (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
          F.map x_2))
      (Sum.inl val)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x x_1 : C
x_2 : x ⟶ x_1
h :
  ∀ (val : F₁.obj x),
    TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          ((coprod F₁ F₂).map x_2 ≫
            ↾Sum.elim
                (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
                  (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
                (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
                  (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))))
        (Sum.inl val) =
      TypeCat.Fun.toFun (X := (coprod F₁ F₂).obj x)
        (hom (FC := TypeCat.Fun)
          (↾Sum.elim
                (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
                  (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
                (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
                  (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
            F.map x_2))
        (Sum.inl val)
⊢ (coprod F₁ F₂).map x_2 ≫
      ↾Sum.elim
          (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
            (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
          (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
            (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1)) =
    ↾Sum.elim
          (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
            (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
          (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
            (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
      F.map x_2
have h₁ : ∀ (val : F₂.obj x),
  TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((coprod F₁ F₂).map x_2 ≫
          ↾Sum.elim
              (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
              (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
                (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))))
      (Sum.inr val) =
    TypeCat.Fun.toFun (X := (coprod F₁ F₂).obj x)
      (hom (FC := TypeCat.Fun)
        (↾Sum.elim
              (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
              (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
                (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
          F.map x_2))
      (Sum.inr val)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : Cocone (pair F G)
x_1 : (binaryCoproductCocone F G).pt ⟶ x.pt
h : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone F G).ι.app j ≫ x_1 = x.ι.app j
⊢ x_1 = coprod.desc (BinaryCofan.inl x) (BinaryCofan.inr x)
have w : ∀ (x_2 : C) (x_3 : (binaryCoproductCocone F G).pt.obj x_2),
  (hom (FC := TypeCat.Fun) (x_1.app x_2)).toFun x_3 =
    (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x) (BinaryCofan.inr x)).app x_2)).toFun x_3
Tactic: ext _ x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x_1 : Cocone (pair F G)
x_2 : (binaryCoproductCocone F G).pt ⟶ x_1.pt
h : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone F G).ι.app j ≫ x_2 = x_1.ι.app j
x_3 : C
x : (binaryCoproductCocone F G).pt.obj x_3
⊢ (hom (FC := TypeCat.Fun) (x_2.app x_3)).toFun x =
    (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x_1) (BinaryCofan.inr x_1)).app x_3)).toFun x
have w : ∀ (val : F.obj x_3),
  (hom (FC := TypeCat.Fun) (x_2.app x_3)).toFun (Sum.inl val) =
    (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x_1) (BinaryCofan.inr x_1)).app x_3)).toFun (Sum.inl val)
Tactic: cases x with | _ => simp [← h ⟨WalkingPair.right⟩, ← h ⟨WalkingPair.left⟩]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x_1 : Cocone (pair F G)
x_2 : (binaryCoproductCocone F G).pt ⟶ x_1.pt
h : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone F G).ι.app j ≫ x_2 = x_1.ι.app j
x_3 : C
x : (binaryCoproductCocone F G).pt.obj x_3
w :
  ∀ (val : F.obj x_3),
    (hom (FC := TypeCat.Fun) (x_2.app x_3)).toFun (Sum.inl val) =
      (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x_1) (BinaryCofan.inr x_1)).app x_3)).toFun (Sum.inl val)
⊢ (hom (FC := TypeCat.Fun) (x_2.app x_3)).toFun x =
    (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x_1) (BinaryCofan.inr x_1)).app x_3)).toFun x
have w₁ : ∀ (val : G.obj x_3),
  (hom (FC := TypeCat.Fun) (x_2.app x_3)).toFun (Sum.inr val) =
    (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x_1) (BinaryCofan.inr x_1)).app x_3)).toFun (Sum.inr val)
Tactic: cases x with | _ => simp [← h ⟨WalkingPair.right⟩, ← h ⟨WalkingPair.left⟩]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
⊢ Limits.coprod.inr ≫ (binaryCoproductIso F G).hom = coprod.inr
have simp : Eq (α := G ⟶ coprod F G)
  ((binaryCoproductColimitCocone F G).cocone.ι.app { as := WalkingPair.right } :
    Functor.obj (pair F G) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (binaryCoproductColimitCocone F G).cocone.pt)
        { as := WalkingPair.right : Discrete WalkingPair })
  coprod.inr
Tactic: simp [binaryCoproductIso]
-- 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 : C
⊢ CategoryStruct.comp (Y := colimit ((F.map (𝟙 X)).toFunctor ⋙ Grothendieck.ι F X ⋙ G))
      (colimMap
        (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
          ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom))
      (colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor) =
    𝟙 (colimit (Grothendieck.ι F X ⋙ G))
have w : ∀ (d : (↑(F.obj X) : Type u_1)),
  CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
      (CategoryStruct.comp (Y := colimit ((F.map (𝟙 X)).toFunctor ⋙ Grothendieck.ι F X ⋙ G))
        (colimMap
          (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
            ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom))
        (colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor)) =
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ 𝟙 (colimit (Grothendieck.ι F X ⋙ G))
Tactic: ext d
-- 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 : C
d : (↑(F.obj X) : Type u_1)
⊢ CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
      (CategoryStruct.comp (Y := colimit ((F.map (𝟙 X)).toFunctor ⋙ Grothendieck.ι F X ⋙ G))
        (colimMap
          (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
            ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom))
        (colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor)) =
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ 𝟙 (colimit (Grothendieck.ι F X ⋙ G))
have 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)))
  (colimit.ι (Grothendieck.ι F X ⋙ G) d)
Tactic: simp only [Functor.comp_obj, Grothendieck.ιNatTrans, Grothendieck.ι_obj, ι_colimMap_assoc,
      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 : C
d : (↑(F.obj X) : Type u_1)
| colimit.ι (Grothendieck.ι F X ⋙ G) d
have rw : CategoryStruct.comp (Y := (Grothendieck.ι F X ⋙ G).obj ((F.map (𝟙 X)).toFunctor.obj d)) (eqToHom sorry)
  (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d))
Tactic: rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).toFunctor.obj d) (by 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 : 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)))
    (colimit.ι (Grothendieck.ι F X ⋙ G) d)
have 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)) (eqToHom sorry)
    (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
Tactic: conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).toFunctor.obj d) (by 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 : 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)) (eqToHom ⋯)
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
have 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 sorry,
        fiber :=
          (eqToHom sorry :
            obj (Cat.Hom.toFunctor (F.map (eqToHom sorry))) ((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: rw [← eqToHom_map G (by simp), Grothendieck.eqToHom_eq]
-- 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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ 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)))
have 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))))
Tactic: ext d
-- 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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
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))))
have 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)))))
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]