awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : Small.{v, w} J
F : J ⥤ SheafedSpace.{u, v, v} C
inst_3 : HasLimits.{v, u} C
X Y : SheafedSpace.{u, v, v} C
f g : X ⟶ Y
⊢ Epi (Y := (↑(coequalizer f g).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π f g)))
have rw : Epi (X := (↑Y.toPresheafedSpace : TopCat)) (Y := (↑(coequalizer f g).toPresheafedSpace : TopCat))
  (CategoryStruct.comp (Y :=
      coequalizer (X := Functor.obj (forget C) X) (CategoryTheory.Functor.map (forget C) f)
        (CategoryTheory.Functor.map (forget C) g))
      (coequalizer.π (CategoryTheory.Functor.map (forget C) f) (CategoryTheory.Functor.map (forget C) g))
      (Iso.hom (PreservesCoequalizer.iso (forget C) f g)) :
    Functor.obj (forget C) Y ⟶ Functor.obj (forget C) (coequalizer f g))
Tactic: rw [← show _ = (coequalizer.π f g).hom.base from
      ι_comp_coequalizerComparison f g (SheafedSpace.forget C),
      ← PreservesCoequalizer.iso_hom]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
x : (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u)
⊢ IsLocalRing.{u} (↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk x) : Type u)
have obtain : ∀ (i : Discrete ι) (y : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)),
  IsLocalRing.{u}
    (↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
              (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
            y)) :
      Type u)
Tactic: obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (hypothesis)
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
i : Discrete ι
y : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)
⊢ IsLocalRing.{u}
    (↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
              (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
            y)) :
      Type u)
have this : IsLocalRing.{u} (↑(((F ⋙ forgetToSheafedSpace).obj i).presheaf.stalk y) : Type u)
Tactic: haveI : IsLocalRing (((F ⋙ forgetToSheafedSpace).obj i).presheaf.stalk y) :=
      (F.obj i).isLocalRing _
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
x x_1 : Discrete ι
j j' : ι
x_2 : { as := j : Discrete ι } ⟶ { as := j' }
f : j = j'
⊢ Eq (α :=
    F.obj { as := j : Discrete ι } ⟶
      Functor.obj (Functor.obj (Functor.const (Discrete ι)) (coproduct F)) { as := j' : Discrete ι })
    (F.map
        { down := { down := f : PLift ({ as := j : Discrete ι }.as = { as := j' : Discrete ι }.as) } :
          ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j' : Discrete ι }.as)) } ≫
      homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j' }) ⋯)
    (homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const (Discrete ι)) (coproduct F))
        { down := { down := f : PLift ({ as := j : Discrete ι }.as = { as := j' : Discrete ι }.as) } :
          ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j' : Discrete ι }.as)) })
have subst : ∀ (x : { as := j : Discrete ι } ⟶ { as := j }),
  Eq (α :=
    F.obj { as := j : Discrete ι } ⟶
      Functor.obj (Functor.obj (Functor.const (Discrete ι)) (coproduct F)) { as := j : Discrete ι })
    (F.map
        { down := { down := sorry : PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as) } :
          ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as)) } ≫
      homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) sorry)
    (homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) sorry ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const (Discrete ι)) (coproduct F))
        { down := { down := sorry : PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as) } :
          ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as)) })
Tactic: subst f
Cleared hypotheses: j', x_2, f
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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 (α := (↑(↑(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))
have 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)))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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)
⊢ 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)
have H : (Opens.map f.base).obj (imageBasicOpen f g U s) = (Opens.map g.base).obj (imageBasicOpen f g U s)
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
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have H : 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]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have 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))
Tactic: apply inf_eq_right.mpr
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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))
have 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))
Tactic: refine (RingedSpace.basicOpen_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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)
⊢ 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))
have 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))
Tactic: rw [coequalizer.condition f.toShHom g.toShHom]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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)
⊢ 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))
have 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))
Tactic: dsimp only [SheafedSpace.forget]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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)
⊢ 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))
have rw : IsOpen (imageBasicOpen f g U s).carrier
Tactic: rw [imageBasicOpen_image_preimage]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : (↑Y.toTopCat : Type v)
⊢ IsLocalHom (R :=
    (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((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))
            x)) :
      Type v))
    (S := (↑(Y.presheaf.stalk x) : Type v)) (F :=
    (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
            ((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))
              x)) :
        Type v) →+*
      (↑(Y.presheaf.stalk x) : Type v))
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))) x))
have map_nonunit : ∀
  (a :
    (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((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))
            x)) :
      Type v)),
  IsUnit (M := (↑(Y.presheaf.stalk x) : Type v))
      ((CommRingCat.Hom.hom
              (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))
                x) :
            (a :
                (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
                      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base :
                          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
                        x)) :
                  Type v)) →
              (↑(Y.presheaf.stalk x) : Type v))
          a :
        (↑(Y.presheaf.stalk x) : Type v)) →
    IsUnit a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : (↑(↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
⊢ IsLocalRing.{v} (↑((Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk x) : Type v)
have obtain : ∀ (y : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)),
  IsLocalRing.{v}
    (↑((Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(Limits.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)) →
                (↑(↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
            y)) :
      Type v)
Tactic: obtain ⟨y, rfl⟩ :=
      (TopCat.epi_iff_surjective (coequalizer.π f.toShHom g.toShHom).hom.base).mp inferInstance x
Cleared hypotheses: x