awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
⊢ HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) LocallyRingedSpace

Tactic:
⟨fun F => ⟨⟨⟨_, coproductCofanIsColimit F⟩⟩⟩⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, AlgebraicGeometry.LocallyRingedSpace.coproductCofanIsColimit, AlgebraicGeometry.LocallyRingedSpace.coproductCofan
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
⊢ PreservesColimitsOfShape.{v, v, u, u, u + 1, u + 1} (Discrete ι) forgetToSheafedSpace

Tactic:
⟨fun {G} =>
    preservesColimit_of_preserves_colimit_cocone (coproductCofanIsColimit G)
      ((colimit.isColimit (C := SheafedSpace.{u+1, u, u} CommRingCat.{u}) _).ofIsoColimit
        (Cocone.ext (Iso.refl _) fun _ => Category.comp_id _))⟩

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.refl, CategoryTheory.Category.comp_id, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone, CategoryTheory.Limits.PreservesColimitsOfShape.mk, AlgebraicGeometry.LocallyRingedSpace.coproductCofanIsColimit, CategoryTheory.NatTrans.app, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)
e :
  Eq (α := X.Hom (coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace)
    (f.toHom ≫ InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))
    (g.toHom ≫ InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))
⊢ Eq (α := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑X.toPresheafedSpace : TopCat)) (Y :=
            (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (f.toHom ≫ InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
        x :
      (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑X.toPresheafedSpace : TopCat)) (Y :=
            (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (g.toHom ≫ InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
        x :
      (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))

Tactic:
congr 3
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)
⊢ Eq (α := X.Hom (coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace)
    (f.toHom ≫ InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))
    (g.toHom ≫ InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))

Tactic:
SheafedSpace.forgetToPresheafedSpace.congr_map
      (coequalizer.condition f.toShHom g.toShHom)

Premises used: CategoryTheory.Limits.coequalizer.condition, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, CategoryTheory.Functor.congr_map, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)
⊢ Eq (α := X.Hom (coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace)
    (f.toHom ≫ InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))
    (g.toHom ≫ InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))

Tactic:
exact SheafedSpace.forgetToPresheafedSpace.congr_map
      (coequalizer.condition f.toShHom g.toShHom)

Premises used: CategoryTheory.Limits.coequalizer.condition, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, CategoryTheory.Functor.congr_map, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
⊢ IsColimit (F :=
    parallelPair (X := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
      (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              f.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
      (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              g.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))))
    (Cofork.ofπ (P := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
      (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)))
      ⋯)

Tactic:
exact isColimitCoforkMapOfIsColimit (forget TopCat) _
      (isColimitCoforkMapOfIsColimit (SheafedSpace.forget _)
      _ (coequalizerIsCoequalizer f.toShHom g.toShHom))

Premises used: CategoryTheory.Limits.isColimitCoforkMapOfIsColimit, AlgebraicGeometry.SheafedSpace.forget, CategoryTheory.Limits.coequalizerIsCoequalizer, CategoryTheory.forget, TopCat, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
this : (Opens.map f.base).obj (imageBasicOpen f g U s) = (Opens.map g.base).obj (imageBasicOpen f g U s)
⊢ Eq (α := Set ((fun (X : Type v) ↦ X) (↑(↑X.toPresheafedSpace : TopCat) : Type v)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.base) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))) :
        (a : (fun (X : Type v) ↦ X) (↑(↑X.toPresheafedSpace : TopCat) : Type v)) →
          (fun (X : Type v) ↦ X) (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ⁻¹'
      (imageBasicOpen f g U s).carrier)
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) g.base) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))) :
        (a : (fun (X : Type v) ↦ X) (↑(↑X.toPresheafedSpace : TopCat) : Type v)) →
          (fun (X : Type v) ↦ X) (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ⁻¹'
      (imageBasicOpen f g U s).carrier)

Tactic:
injection this
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
H : (Opens.map f.base).obj (imageBasicOpen f g U s) = (Opens.map g.base).obj (imageBasicOpen f g U s)
⊢ Eq (α := Set ((fun (X : Type v) ↦ X) (↑(↑X.toPresheafedSpace : TopCat) : Type v)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.base) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))) :
        (a : (fun (X : Type v) ↦ X) (↑(↑X.toPresheafedSpace : TopCat) : Type v)) →
          (fun (X : Type v) ↦ X) (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ⁻¹'
      (imageBasicOpen f g U s).carrier)
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) g.base) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))) :
        (a : (fun (X : Type v) ↦ X) (↑(↑X.toPresheafedSpace : TopCat) : Type v)) →
          (fun (X : Type v) ↦ X) (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ⁻¹'
      (imageBasicOpen f g U s).carrier)

Tactic:
suffices
      (TopologicalSpace.Opens.map f.base).obj (imageBasicOpen f g U s) =
        (TopologicalSpace.Opens.map g.base).obj (imageBasicOpen f g U s)
      by injection this
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
erw [SheafedSpace.congr_hom_app (coequalizer.condition f.toShHom g.toShHom),
      CommRingCat.comp_apply, X.toRingedSpace.basicOpen_res]

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_res, CategoryTheory.Limits.coequalizer.condition, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, CommRingCat.comp_apply, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
H :
  X.toRingedSpace.basicOpen (U :=
      unop
        (Functor.obj
          (Functor.op
            (Opens.map
              (PresheafedSpace.Hom.base
                (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
          (op U)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
            CommRingCat.carrier) (Y :=
            Functor.obj
              (Functor.obj
                (TopCat.Presheaf.pushforward CommRingCat
                  (PresheafedSpace.Hom.base
                    (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                X.presheaf)
              (op U))
            (NatTrans.app
              (PresheafedSpace.Hom.c
                (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))
              (op U)) :
          (a : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj
                      X.presheaf).obj
                  (op U)) :
              Type v))
        s) ≤
    unop
      (Functor.obj
        (Functor.op
          (Opens.map
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
        (op U))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply inf_eq_right.mpr

Premises used: Iff.mpr, inf_eq_right
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
⊢ X.toRingedSpace.basicOpen (U :=
      unop
        (Functor.obj
          (Functor.op
            (Opens.map
              (PresheafedSpace.Hom.base
                (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
          (op U)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
            CommRingCat.carrier) (Y :=
            Functor.obj
              (Functor.obj
                (TopCat.Presheaf.pushforward CommRingCat
                  (PresheafedSpace.Hom.base
                    (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                X.presheaf)
              (op U))
            (NatTrans.app
              (PresheafedSpace.Hom.c
                (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))
              (op U)) :
          (a : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj
                      X.presheaf).obj
                  (op U)) :
              Type v))
        s) ≤
    unop
      (Functor.obj
        (Functor.op
          (Opens.map
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
        (op U))

Tactic:
(RingedSpace.basicOpen_le _ _).trans ?_

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_le, LE.le.trans
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
H :
  unop
      (Functor.obj
        (Functor.op
          (Opens.map
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
        (op U)) ≤
    unop
      (Functor.obj
        (Functor.op
          (Opens.map
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
        (op U))
⊢ X.toRingedSpace.basicOpen (U :=
      unop
        (Functor.obj
          (Functor.op
            (Opens.map
              (PresheafedSpace.Hom.base
                (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
          (op U)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
            CommRingCat.carrier) (Y :=
            Functor.obj
              (Functor.obj
                (TopCat.Presheaf.pushforward CommRingCat
                  (PresheafedSpace.Hom.base
                    (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                X.presheaf)
              (op U))
            (NatTrans.app
              (PresheafedSpace.Hom.c
                (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))
              (op U)) :
          (a : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj
                      X.presheaf).obj
                  (op U)) :
              Type v))
        s) ≤
    unop
      (Functor.obj
        (Functor.op
          (Opens.map
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
        (op U))

Tactic:
refine (RingedSpace.basicOpen_le _ _).trans ?_

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_le, LE.le.trans
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
H H₁ :
  unop
      (Functor.obj
        (Functor.op
          (Opens.map
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
        (op U)) ≤
    unop
      (Functor.obj
        (Functor.op
          (Opens.map
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
        (op U))
⊢ unop
      (Functor.obj
        (Functor.op
          (Opens.map
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
        (op U)) ≤
    unop
      (Functor.obj
        (Functor.op
          (Opens.map
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))))
        (op U))

Tactic:
rw [coequalizer.condition f.toShHom g.toShHom]

Premises used: CategoryTheory.Limits.coequalizer.condition, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
dsimp :
  IsOpen (X := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (Set.preimage (β := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
          (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
        (imageBasicOpen f g U s).carrier))
⊢ IsOpen (X := (↑(Functor.obj (SheafedSpace.forget CommRingCat) Y.toSheafedSpace) : Type v))
    (Set.preimage (β :=
      (↑(Functor.obj (SheafedSpace.forget CommRingCat) (coequalizer (Hom.toShHom f) (Hom.toShHom g))) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := Functor.obj (SheafedSpace.forget CommRingCat) Y.toSheafedSpace) (Y :=
            Functor.obj (SheafedSpace.forget CommRingCat) (coequalizer (Hom.toShHom f) (Hom.toShHom g)))
            (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat)
              (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
        (a : (↑((SheafedSpace.forget CommRingCat).obj Y.toSheafedSpace) : Type v)) →
          (↑((SheafedSpace.forget CommRingCat).obj (coequalizer (Hom.toShHom f) (Hom.toShHom g))) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
        (imageBasicOpen f g U s).carrier))

Tactic:
dsimp only [SheafedSpace.forget]

Premises used: AlgebraicGeometry.SheafedSpace.forget
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
rw : IsOpen (imageBasicOpen f g U s).carrier
⊢ IsOpen (X := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (Set.preimage (β := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
          (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
        (imageBasicOpen f g U s).carrier))

Tactic:
rw [imageBasicOpen_image_preimage]

Premises used: AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage