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
F : J ⥤ PresheafedSpace.{v, u, v} C
j : J
⊢ Eq (α :=
    Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
      (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)))
      (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))))
    ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
        (Quiver.Hom.op
          (map (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.map (𝟙 j)).c ≫
            Iso.inv (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf) ≫
              Iso.hom (pushforwardEq ⋯ (F.obj j).presheaf))) :
      Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))))
    ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
        (𝟙 (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))) :
      Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))))

Tactic:
NatTrans.ext (funext fun U => ?_)

Premises used: CategoryTheory.NatTrans.ext, funext
-- 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
F : J ⥤ PresheafedSpace.{v, u, v} C
j : J
U : Opens (↑(colimit (F ⋙ forget C)) : Type v)
a :
  Eq.{v + 1} (α :=
    (F.obj j).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j)) U)) ⟶
      (F.obj j).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j)) U)))
    (𝟙 ((F.obj j).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j)) U))))
    (NatTrans.app (𝟙 (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)) (op U))
⊢ Eq (α :=
    obj (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))) (op U) ⟶
      obj (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))) (op U))
    (NatTrans.app
      ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
        (Quiver.Hom.op
          (map (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.map (𝟙 j)).c ≫
            Iso.inv (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf) ≫
              Iso.hom (pushforwardEq ⋯ (F.obj j).presheaf))))
      (op U))
    (NatTrans.app
      ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
        (𝟙 (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))))
      (op U))

Tactic:
simp [opEquiv]

Premises used: CategoryTheory.opEquiv
-- 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
F : J ⥤ PresheafedSpace.{v, u, v} C
j : J
U : Opens (↑(colimit (F ⋙ forget C)) : Type v)
⊢ Eq.{v + 1} (α :=
    (F.obj j).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j)) U)) ⟶
      (F.obj j).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j)) U)))
    (𝟙 ((F.obj j).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j)) U))))
    (NatTrans.app (𝟙 (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)) (op U))

Tactic:
rfl
-- 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
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
⊢ Eq (α :=
    Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
      (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)))
      (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))))
    ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf)))
        (Quiver.Hom.op
          (map (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.map (f ≫ g)).c ≫
            Iso.inv (Pushforward.comp ((F ⋙ forget C).map (f ≫ g)) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₁).presheaf) ≫
              Iso.hom (pushforwardEq ⋯ (F.obj j₁).presheaf))) :
      Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))))
    ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf)))
        (Quiver.Hom.op
            (map (pushforward C (colimit.ι (F ⋙ forget C) j₂)) (F.map f).c ≫
              Iso.inv (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j₂) (F.obj j₁).presheaf) ≫
                Iso.hom (pushforwardEq ⋯ (F.obj j₁).presheaf)) ≫
          Quiver.Hom.op
            (map (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.map g).c ≫
              Iso.inv (Pushforward.comp ((F ⋙ forget C).map g) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₂).presheaf) ≫
                Iso.hom (pushforwardEq ⋯ (F.obj j₂).presheaf))) :
      Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))))

Tactic:
NatTrans.ext (funext fun U => ?_)

Premises used: CategoryTheory.NatTrans.ext, funext
-- 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
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens (↑(colimit (F ⋙ forget C)) : Type v))ᵒᵖ
a :
  unop (op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U)))) =
    unop (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U)))
⊢ op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) =
    op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U))

Tactic:
apply unop_injective

Premises used: Opposite.unop_injective
-- 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
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens (↑(colimit (F ⋙ forget C)) : Type v))ᵒᵖ
a :
  unop (op (obj (Opens.map ((F.map g).base ≫ colimit.ι (F ⋙ forget C) j₃)) (unop U))) =
    unop (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U)))
⊢ unop (op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U)))) =
    unop (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U)))

Tactic:
rw [← Opens.map_comp_obj]

Premises used: TopologicalSpace.Opens.map_comp_obj
-- 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
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens (↑(colimit (F ⋙ forget C)) : Type v))ᵒᵖ
a :
  Eq (α := (↑(F.obj j₂) : TopCat) ⟶ colimit (F ⋙ forget C)) ((F.map g).base ≫ colimit.ι (F ⋙ forget C) j₃)
    (colimit.ι (F ⋙ forget C) j₂)
⊢ unop (op (obj (Opens.map ((F.map g).base ≫ colimit.ι (F ⋙ forget C) j₃)) (unop U))) =
    unop (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U)))

Tactic:
congr
-- 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
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens (↑(colimit (F ⋙ forget C)) : Type v))ᵒᵖ
⊢ Eq (α := (↑(F.obj j₂) : TopCat) ⟶ colimit (F ⋙ forget C)) ((F.map g).base ≫ colimit.ι (F ⋙ forget C) j₃)
    (colimit.ι (F ⋙ forget C) j₂)

Tactic:
colimit.w (F ⋙ PresheafedSpace.forget C) g

Premises used: CategoryTheory.Functor.comp, AlgebraicGeometry.PresheafedSpace.forget, CategoryTheory.Limits.colimit.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
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens (↑(colimit (F ⋙ forget C)) : Type v))ᵒᵖ
⊢ Eq (α := (↑(F.obj j₂) : TopCat) ⟶ colimit (F ⋙ forget C)) ((F.map g).base ≫ colimit.ι (F ⋙ forget C) j₃)
    (colimit.ι (F ⋙ forget C) j₂)

Tactic:
exact colimit.w (F ⋙ PresheafedSpace.forget C) g

Premises used: CategoryTheory.Functor.comp, AlgebraicGeometry.PresheafedSpace.forget, CategoryTheory.Limits.colimit.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
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens (↑(colimit (F ⋙ forget C)) : Type v))ᵒᵖ
⊢ op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) =
    op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U))

Tactic:
have :
      op ((Opens.map (F.map g).base).obj
          ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj U.unop)) =
        op ((Opens.map (colimit.ι (F ⋙ PresheafedSpace.forget C) j₂)).obj (unop U)) := by
      apply unop_injective
      rw [← Opens.map_comp_obj]
      congr
      exact colimit.w (F ⋙ PresheafedSpace.forget C) g
-- 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
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens (↑(colimit (F ⋙ forget C)) : Type v))ᵒᵖ
this :
  op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) =
    op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U))
a :
  Eq (α :=
    (F.obj j₃).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) ⟶
      (F.obj j₁).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₁)) (unop U))))
    ((F.map g).c.app (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) ≫
      (F.map f).c.app (op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U)))) ≫
        (F.obj j₁).presheaf.map (eqToHom ⋯))
    ((F.map g).c.app (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) ≫
      (F.map f).c.app (op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U)))) ≫
        (F.obj j₁).presheaf.map (Quiver.Hom.op ((Opens.map (F.map f).base).map (eqToHom ⋯))) ≫
          (F.obj j₁).presheaf.map (eqToHom ⋯))
⊢ (F.map (f ≫ g)).c.app (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) ≫
      𝟙
          ((F.obj j₁).presheaf.obj
            (op ((Opens.map (F.map (f ≫ g)).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))))) ≫
        NatTrans.app (Iso.hom (pushforwardEq ⋯ (F.obj j₁).presheaf)) U =
    ((F.map g).c.app (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) ≫
        𝟙
            ((F.obj j₂).presheaf.obj
              (op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))))) ≫
          NatTrans.app (Iso.hom (pushforwardEq ⋯ (F.obj j₂).presheaf)) U) ≫
      (F.map f).c.app (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U))) ≫
        𝟙
            ((F.obj j₁).presheaf.obj
              (op ((Opens.map (F.map f).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U))))) ≫
          NatTrans.app (Iso.hom (pushforwardEq ⋯ (F.obj j₁).presheaf)) U

Tactic:
simp only [map_comp_c_app, pushforward_obj_obj, pushforward_map_app, comp_base,
      pushforwardEq_hom_app, op_obj, Opens.map_comp_obj, id_comp, assoc, eqToHom_map_comp,
      NatTrans.naturality_assoc, pushforward_obj_map, eqToHom_unop]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_map_comp, TopCat.Presheaf.pushforward_map_app, TopCat.Presheaf.pushforwardEq_hom_app, TopCat.Presheaf.pushforward_obj_obj, TopCat.Presheaf.pushforward_obj_map, AlgebraicGeometry.PresheafedSpace.comp_base, TopologicalSpace.Opens.map_comp_obj, AlgebraicGeometry.PresheafedSpace.map_comp_c_app, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.eqToHom_unop, CategoryTheory.Functor.op_obj, CategoryTheory.Category.id_comp
-- 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
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens (↑(colimit (F ⋙ forget C)) : Type v))ᵒᵖ
this :
  op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) =
    op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₂)) (unop U))
⊢ Eq (α :=
    (F.obj j₃).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) ⟶
      (F.obj j₁).presheaf.obj (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₁)) (unop U))))
    ((F.map g).c.app (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) ≫
      (F.map f).c.app (op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U)))) ≫
        (F.obj j₁).presheaf.map (eqToHom ⋯))
    ((F.map g).c.app (op (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U))) ≫
      (F.map f).c.app (op ((Opens.map (F.map g).base).obj (obj (Opens.map (colimit.ι (F ⋙ forget C) j₃)) (unop U)))) ≫
        (F.obj j₁).presheaf.map (Quiver.Hom.op ((Opens.map (F.map f).base).map (eqToHom ⋯))) ≫
          (F.obj j₁).presheaf.map (eqToHom ⋯))

Tactic:
simp [NatTrans.congr (α := (F.map f).c) this]

Premises used: CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.NatTrans.congr
-- 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
⊢ (↑(colimit F) : TopCat) = Limits.colimit (F ⋙ forget C)

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit, rfl
-- 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
⊢ (colimit F).presheaf =
    limit (Functor.leftOp (pushforwardDiagramToColimit F) : Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit, rfl
-- 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'
w :
  Eq (α := (↑(F.obj j) : TopCat) ⟶ (↑(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') }))
    (Hom.base
      ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
        map (obj (Functor.const J) (colimit F)) f))
h :
  Eq (α :=
    (obj (obj (Functor.const J) (colimit F)) j').presheaf ⟶
      Functor.op
          (Opens.map
            (Hom.base
              ({ base := colimit.ι (F ⋙ forget C) j,
                  c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
                map (obj (Functor.const J) (colimit F)) f))) ⋙
        (F.obj j).presheaf)
    (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))
    (Hom.c
      ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
        map (obj (Functor.const J) (colimit F)) f))
⊢ Eq (α := F.obj j ⟶ obj (obj (Functor.const J) (colimit F)) j')
    (F.map f ≫
      { base := colimit.ι (F ⋙ forget C) j', c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j') })
    ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
      map (obj (Functor.const J) (colimit F)) f)

Tactic:
ext1
-- 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'
w :
  ∀ (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))
⊢ Eq (α := (↑(F.obj j) : TopCat) ⟶ (↑(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') }))
    (Hom.base
      ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
        map (obj (Functor.const J) (colimit F)) f))

Tactic:
ext x