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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
⊢ 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)))))
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 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 [← Category.assoc, ← 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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
| 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)))
have 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 sorry)
    (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d))
Tactic: rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F Z ⋙ G)
      (j := (F.map (f ≫ g)).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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
⊢ 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))))
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)))
  (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 sorry)
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
Tactic: conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F Z ⋙ G)
      (j := (F.map (f ≫ g)).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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
⊢ 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)))
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 := (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 sorry,
          fiber :=
            (eqToHom sorry :
              obj
                  (Cat.Hom.toFunctor (F.map (eqToHom sorry)) :
                    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)))
Tactic: rw [← Category.assoc, ← eqToHom_map G (by simp), ← G.map_comp, 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
d : (↑(F.obj X) : Type u_1)
⊢ Eq (α := (Grothendieck.ι F X).obj d ⟶ (Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d))
    { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
    (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) })
have w : 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 sorry,
        fiber :=
          (eqToHom sorry :
            obj
                (Cat.Hom.toFunctor (F.map (eqToHom sorry)) :
                  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: fapply 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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
| (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)
have enter : (F.map (𝟙 Z)).toFunctor.map (eqToHom sorry)
Tactic: enter [2, 1]
-- 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)
| (F.map (𝟙 Z)).toFunctor.map (eqToHom ⋯)
have rw : eqToHom sorry
Tactic: rw [eqToHom_map (F.map (𝟙 Z)).toFunctor]
-- 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)
| (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)
have enter : eqToHom sorry
Tactic: enter [2, 1]; rw [eqToHom_map (F.map (𝟙 Z)).toFunctor]
-- 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.{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)
have w : Eq.{u_2 + 1} (α := (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
  (eqToHom sorry : (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 sorry)
      (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
        (eqToHom sorry) (eqToHom sorry)) :
    (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]
-- 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)
| (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)
have rw : (eqToHom sorry : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
Tactic: rw [eqToHom_trans, eqToHom_trans]
-- 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.{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)
have conv_rhs : Eq.{u_2 + 1} (α := (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
  (eqToHom sorry : (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 sorry)
      (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
        (eqToHom sorry) (eqToHom sorry)) :
    (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
Tactic: conv_rhs => rw [eqToHom_trans, eqToHom_trans]
-- 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)
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)
⊢ 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)
have w : Eq.{u_2 + 1} (α := (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
  (eqToHom sorry : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
  (eqToHom sorry : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
Tactic: conv_rhs => rw [eqToHom_trans, eqToHom_trans]
-- 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 : Grothendieck F ⥤ H
α : X ⟶ Y
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ 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)
have 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))
Tactic: apply colimit.hom_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_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
⊢ { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ } = 𝟙 (fiberwiseColimit G)
have w : ∀ (x : C),
  NatTrans.app { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := sorry } x =
    NatTrans.app (𝟙 (fiberwiseColimit G)) x
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_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
⊢ NatTrans.app { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ } x =
    NatTrans.app (𝟙 (fiberwiseColimit G)) x
have w : colimMap (𝟙 (Grothendieck.ι F x ⋙ G)) = 𝟙 (colimit (Grothendieck.ι F x ⋙ G))
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)
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
⊢ 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 := ⋯ })
have 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 := sorry } x)
    (NatTrans.app
      (CategoryStruct.comp (Y := fiberwiseColimit Y)
        { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft α), naturality := sorry }
        { app := fun (c : C) ↦ map colim ((Grothendieck.ι F c).whiskerLeft β), naturality := sorry })
      x)
Tactic: ext