awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
F : J ⥤ PresheafedSpace.{v, u, v} C
j j' : J
f : j ⟶ j'
x : (↑(↑(F.obj j) : TopCat) : Type v)
⊢ Eq (α := (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat))
            (Hom.base
              (F.map f ≫
                { base := colimit.ι (F ⋙ forget C) j',
                  c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j') })) :
          (a : (↑(↑(F.obj j) : TopCat) : Type v)) →
            (↑(↑(((Functor.const J).obj (colimit F)).obj j') : TopCat) : Type v))
        x :
      (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(F.obj j) : TopCat)) (Y := (↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat))
            (Hom.base
              ({ base := colimit.ι (F ⋙ forget C) j,
                  c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
                map (obj (Functor.const J) (colimit F)) f)) :
          (a : (↑(↑(F.obj j) : TopCat) : Type v)) →
            (↑(↑(((Functor.const J).obj (colimit F)).obj j') : TopCat) : Type v))
        x :
      (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v))

Tactic:
colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.w_apply, AlgebraicGeometry.PresheafedSpace.forget
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
F : J ⥤ PresheafedSpace.{v, u, v} C
j j' : J
f : j ⟶ j'
x : (↑(↑(F.obj j) : TopCat) : Type v)
⊢ Eq (α := (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat))
            (Hom.base
              (F.map f ≫
                { base := colimit.ι (F ⋙ forget C) j',
                  c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j') })) :
          (a : (↑(↑(F.obj j) : TopCat) : Type v)) →
            (↑(↑(((Functor.const J).obj (colimit F)).obj j') : TopCat) : Type v))
        x :
      (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(F.obj j) : TopCat)) (Y := (↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat))
            (Hom.base
              ({ base := colimit.ι (F ⋙ forget C) j,
                  c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
                map (obj (Functor.const J) (colimit F)) f)) :
          (a : (↑(↑(F.obj j) : TopCat) : Type v)) →
            (↑(↑(((Functor.const J).obj (colimit F)).obj j') : TopCat) : Type v))
        x :
      (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v))

Tactic:
exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.w_apply, AlgebraicGeometry.PresheafedSpace.forget
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
F : J ⥤ PresheafedSpace.{v, u, v} C
j j' : J
f : j ⟶ j'
carrier : Set (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v)
is_open' : IsOpen carrier
⊢ Eq (α :=
    (obj (obj (Functor.const J) (colimit F)) j').presheaf.obj
        (op
          { carrier := carrier, is_open' := is_open' :
            Opens (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v) }) ⟶
      obj
        (Functor.op
            (Opens.map
              (Hom.base
                ({ base := colimit.ι (F ⋙ forget C) j,
                    c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) :
                    (F.obj j).Hom (obj (obj (Functor.const J) (colimit F)) j) } ≫
                  map (obj (Functor.const J) (colimit F)) f))) ⋙
          (F.obj j).presheaf)
        (op
          { carrier := carrier, is_open' := is_open' :
            Opens (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v) }))
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj
          (pushforward C
            (Hom.base
              (F.map f ≫
                { base := colimit.ι (F ⋙ forget C) j',
                  c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j') :
                  (F.obj j').Hom (obj (obj (Functor.const J) (colimit F)) j') })))
          (F.obj j).presheaf)
        (Hom.c
          (F.map f ≫
            { base := colimit.ι (F ⋙ forget C) j',
              c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j') }))
        (whiskerRight (eqToHom ⋯) (F.obj j).presheaf))
      (op { carrier := carrier, is_open' := is_open' }))
    (NatTrans.app
      (Hom.c
        ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
          map (obj (Functor.const J) (colimit F)) f))
      (op { carrier := carrier, is_open' := is_open' }))

Tactic:
simp [← congr_arg NatTrans.app (limit.w (pushforwardDiagramToColimit F).leftOp f.op)]

Premises used: Quiver.Hom.op, congr_arg, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit, CategoryTheory.Functor.leftOp, CategoryTheory.NatTrans.app, CategoryTheory.Limits.limit.w
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
U : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
j : Jᵒᵖ
refine_1 :
  op (obj (Opens.map (Hom.base (s.ι.app (unop j)))) (unop U)) =
    op
      (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v)) (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
        (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))
⊢ Eq (α := (Opens (↑(↑(F.obj (unop j)) : TopCat) : Type v))ᵒᵖ)
    (obj (Functor.op (Opens.map (Hom.base (s.ι.app (unop j))))) U)
    (obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
      (Functor.op (Opens.map (colimit.ι (F ⋙ forget C) (unop j))))
      (obj (Functor.op (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)))) U))

Tactic:
dsimp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
U : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
j : Jᵒᵖ
⊢ op (obj (Opens.map (Hom.base (s.ι.app (unop j)))) (unop U)) =
    op
      (obj
        (Opens.map
          (CategoryStruct.comp (Y := Limits.colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) (unop j))
            (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))))
        (unop U))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
U : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
refine_2 :
  Eq (α :=
    s.pt.presheaf.obj U ⟶
      (F.obj (unop j')).presheaf.obj
        (op
          (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v)) (Opens.map (colimit.ι (F ⋙ forget C) (unop j')))
            (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))))
    (𝟙 (s.pt.presheaf.obj U) ≫
      CategoryStruct.comp (Y :=
        (F.obj (unop j')).presheaf.obj (op (obj (Opens.map (Hom.base (s.ι.app (unop j')))) (unop U))))
        (NatTrans.app (Hom.c (s.ι.app (unop j'))) U) ((F.obj (unop j')).presheaf.map (eqToHom ⋯)))
    (CategoryStruct.comp (Y :=
        (F.obj (unop j)).presheaf.obj (op (obj (Opens.map (Hom.base (s.ι.app (unop j)))) (unop U))))
        (NatTrans.app (Hom.c (s.ι.app (unop j))) U) ((F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map f.unop).c.app
          (op
            (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))
              (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
              (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))
                    (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
                    (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))))) ≫
          NatTrans.app (Iso.hom (pushforwardEq ⋯ (F.obj (unop j')).presheaf))
            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))))
⊢ map (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj U)) f ≫
      CategoryStruct.comp (Y := (obj (pushforward C (Hom.base (s.ι.app (unop j')))) (F.obj (unop j')).presheaf).obj U)
        (NatTrans.app (Hom.c (s.ι.app (unop j'))) U) ((F.obj (unop j')).presheaf.map (eqToHom ⋯)) =
    CategoryStruct.comp (Y := (obj (pushforward C (Hom.base (s.ι.app (unop j)))) (F.obj (unop j)).presheaf).obj U)
        (NatTrans.app (Hom.c (s.ι.app (unop j))) U) ((F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (Functor.comp (D := CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
            (Functor.leftOp (pushforwardDiagramToColimit F) :
              Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
            (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (obj (Functor.op (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)))) U) :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)).map
        f

Tactic:
dsimp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
U : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
⊢ Eq (α := Opens (↑((F ⋙ forget C).obj (unop j)) : Type v))
    (obj
      (Opens.map
        (CategoryStruct.comp (Y := Limits.colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) (unop j))
          (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))))
      (unop U))
    (obj (Opens.map (NatTrans.app (Cocone.ι (mapCocone (forget C) s)) (unop j))) (unop U))

Tactic:
have w :=
      Functor.congr_obj
        (congr_arg Opens.map (colimit.ι_desc ((PresheafedSpace.forget C).mapCocone s) (unop j)))
        (unop U)
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
U : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
w :
  Eq (α := Opens (↑((F ⋙ forget C).obj (unop j)) : Type v))
    (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v)) (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
      (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))
    (obj (Opens.map (NatTrans.app (Cocone.ι (mapCocone (forget C) s)) (unop j))) (unop U))
⊢ Eq (α := (Opens (↑((F ⋙ forget C).obj (unop j)) : Type v))ᵒᵖ)
    (op
      (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v)) (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
        (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))))
    (op (obj (Opens.map (NatTrans.app (Cocone.ι (mapCocone (forget C) s)) (unop j))) (unop U)))

Tactic:
replace w := congr_arg op w
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
U : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
w :
  Eq (α := (Opens (↑((F ⋙ forget C).obj (unop j)) : Type v))ᵒᵖ)
    (op
      (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v)) (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
        (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))))
    (op (obj (Opens.map (NatTrans.app (Cocone.ι (mapCocone (forget C) s)) (unop j))) (unop U)))
⊢ (F.map f.unop).c.app
      (op
        (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v)) (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
          (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))) =
    (F.obj (unop j)).presheaf.map (eqToHom w) ≫
      (F.map f.unop).c.app (op (obj (Opens.map (NatTrans.app (Cocone.ι (mapCocone (forget C) s)) (unop j))) (unop U))) ≫
        (obj (pushforward C (F.map f.unop).base) (F.obj (unop j')).presheaf).map (eqToHom ⋯)

Tactic:
have w' := NatTrans.congr (F.map f.unop).c w
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
U : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
w :
  Eq (α := (Opens (↑((F ⋙ forget C).obj (unop j)) : Type v))ᵒᵖ)
    (op
      (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v)) (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
        (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))))
    (op (obj (Opens.map (NatTrans.app (Cocone.ι (mapCocone (forget C) s)) (unop j))) (unop U)))
w' :
  (F.map f.unop).c.app
      (op
        (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v)) (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
          (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))) =
    (F.obj (unop j)).presheaf.map (eqToHom w) ≫
      (F.map f.unop).c.app (op (obj (Opens.map (NatTrans.app (Cocone.ι (mapCocone (forget C) s)) (unop j))) (unop U))) ≫
        (obj (pushforward C (F.map f.unop).base) (F.obj (unop j')).presheaf).map (eqToHom ⋯)
⊢ Eq (α :=
    s.pt.presheaf.obj U ⟶
      (F.obj (unop j')).presheaf.obj
        (op
          (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v)) (Opens.map (colimit.ι (F ⋙ forget C) (unop j')))
            (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))))
    (𝟙 (s.pt.presheaf.obj U) ≫
      ((F.map f.unop ≫ s.ι.app (unop j)).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯)) ≫
        (F.obj (unop j')).presheaf.map (eqToHom ⋯))
    (CategoryStruct.comp (Y :=
        (F.obj (unop j)).presheaf.obj (op (obj (Opens.map (Hom.base (s.ι.app (unop j)))) (unop U))))
        (NatTrans.app (Hom.c (s.ι.app (unop j))) U) ((F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      ((F.obj (unop j)).presheaf.map (eqToHom w) ≫
          (F.map f.unop).c.app
              (op (obj (Opens.map (NatTrans.app (Cocone.ι (mapCocone (forget C) s)) (unop j))) (unop U))) ≫
            (obj (pushforward C (F.map f.unop).base) (F.obj (unop j')).presheaf).map (eqToHom ⋯)) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  (obj (C := Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))
                    (Opens.map (colimit.ι (F ⋙ forget C) (unop j)))
                    (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))))) ≫
          NatTrans.app (Iso.hom (pushforwardEq ⋯ (F.obj (unop j')).presheaf))
            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
U V : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
i : U ⟶ V
j : Jᵒᵖ
⊢ Eq (α :=
    Quiver.Hom (V := Opens (↑((F ⋙ forget C).obj (unop j)) : Type v))
      (obj
        (Opens.map
          (CategoryStruct.comp (Y := Limits.colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) (unop j))
            (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))))
        (unop V))
      (obj
        (Opens.map
          (CategoryStruct.comp (Y := Limits.colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) (unop j))
            (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))))
        (unop U)))
    (map
      (Opens.map
        (CategoryStruct.comp (Y := Limits.colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) (unop j))
          (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))))
      i.unop)
    (eqToHom ⋯ ≫ map (Opens.map (NatTrans.app (Cocone.ι (mapCocone (forget C) s)) (unop j))) i.unop ≫ eqToHom ⋯)

Tactic:
have w := Functor.congr_hom (congr_arg Opens.map
    (colimit.ι_desc ((PresheafedSpace.forget C).mapCocone s) (unop j))) i.unop
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
j : J
w :
  ∀ (U : (↑(↑(F.obj j) : TopCat) : Type v)),
    Eq (α := (↑(↑s.pt : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              ((colimitCocone F).ι.app j ≫ desc F s).base :
            (a : (↑(↑(F.obj j) : TopCat) : Type v)) → (↑(↑s.pt : TopCat) : Type v))
          U :
        (↑(↑s.pt : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (s.ι.app j).base :
            (a : (↑(↑(F.obj j) : TopCat) : Type v)) → (↑(↑s.pt : TopCat) : Type v))
          U :
        (↑(↑s.pt : TopCat) : Type v))
h :
  ∀ (U : Opens (↑(↑s.pt : TopCat) : Type v)),
    Eq (α := s.pt.presheaf.obj (op U) ⟶ ((Opens.map (s.ι.app j).base).op ⋙ (F.obj j).presheaf).obj (op U))
      (NatTrans.app (((colimitCocone F).ι.app j ≫ desc F s).c ≫ whiskerRight (eqToHom ⋯) (F.obj j).presheaf) (op U))
      ((s.ι.app j).c.app (op U))
⊢ (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j

Tactic:
ext U
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
j : J
U : (↑(↑(F.obj j) : TopCat) : Type v)
⊢ Eq (α := (↑(↑s.pt : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            ((colimitCocone F).ι.app j ≫ desc F s).base :
          (a : (↑(↑(F.obj j) : TopCat) : Type v)) → (↑(↑s.pt : TopCat) : Type v))
        U :
      (↑(↑s.pt : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (s.ι.app j).base :
          (a : (↑(↑(F.obj j) : TopCat) : Type v)) → (↑(↑s.pt : TopCat) : Type v))
        U :
      (↑(↑s.pt : TopCat) : Type v))

Tactic:
simp [desc]

Premises used: AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
j : J
U : Opens (↑(↑s.pt : TopCat) : Type v)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := s.pt.presheaf.obj (op U) ⟶ ((Opens.map (s.ι.app j).base).op ⋙ (F.obj j).presheaf).obj (op U))
    (NatTrans.app (((colimitCocone F).ι.app j ≫ desc F s).c ≫ whiskerRight (eqToHom ⋯) (F.obj j).presheaf) (op U))
    ((s.ι.app j).c.app (op U))

Tactic:
simp only [op_obj, desc, descCApp, Presheaf.comp_app, comp_c_app, colimitCocone_ι_app_c, assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.PresheafedSpace.comp_c_app, TopCat.Presheaf.comp_app, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc, CategoryTheory.Functor.op_obj, AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_c, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
apply :
  ∀ (j : J),
    colimit.ι (F ⋙ forget C) j ≫ m.base =
      CategoryStruct.comp (Y := Limits.colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) j)
        (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))
⊢ m.base = colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)

Tactic:
apply colimit.hom_ext fun j => ?_

Premises used: CategoryTheory.Limits.colimit.hom_ext