-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
theorem imageBasicOpen_image_preimage :
    (coequalizer.π f.toShHom g.toShHom).base ⁻¹' ((coequalizer.π f.toShHom g.toShHom).base ''
      (imageBasicOpen f g U s).1) = (imageBasicOpen f g U s).1

Proof state:
case e.h.e_a.e_a.e_self
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
a✝ : ↑↑X.toPresheafedSpace
⊢ f.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g) = g.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)

Tactic:
exact coequalizer.condition f.toShHom g.toShHom

Result:
no goals

Proof state:
case h.l.l
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsColimit (Cofork.ofπ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)) ?h.l.w)

case h.l.w
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ f.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g) = g.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)

Tactic:
exact coequalizerIsCoequalizer f.toShHom g.toShHom

Result:
no goals

Proof state:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ (Opens.map f.base).obj
      (Y.toRingedSpace.basicOpen
        (let_fun this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s;
        this)) =
    (Opens.map g.base).obj
      (Y.toRingedSpace.basicOpen
        (let_fun this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s;
        this))

Tactic:
rw [preimage_basicOpen f, preimage_basicOpen g]

Result:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (f.c.app
            (op
              (unop
                (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).toPrefunctor.1 (unop (op U))))))))
        (let_fun this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s;
        this)) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (g.c.app
            (op
              (unop
                (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).toPrefunctor.1 (unop (op U))))))))
        (let_fun this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s;
        this))

Proof state:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
this : (Opens.map f.base).obj (imageBasicOpen f g U s) = (Opens.map g.base).obj (imageBasicOpen f g U s)
⊢ ⇑(ConcreteCategory.hom f.base) ⁻¹' (imageBasicOpen f g U s).carrier =
    ⇑(ConcreteCategory.hom g.base) ⁻¹' (imageBasicOpen f g U s).carrier

Tactic:
injection this

Result:
no goals

Proof state:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ unop ((Opens.map (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).op.obj (op U)) ≤
    unop ((Opens.map (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).op.obj (op U))

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

Result:
no goals

Proof state:
case h.l
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsColimit (Cofork.ofπ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base ?h.w)

case h.w
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ f.base ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base =
    g.base ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base

Tactic:
apply isColimitCoforkMapOfIsColimit (SheafedSpace.forget _)

Result:
case h.l.l
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsColimit (Cofork.ofπ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)) ?h.l.w)

case h.l.w
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ f.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g) = g.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)

Proof state:
case h
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsColimit (Cofork.ofπ ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ⋯)

Tactic:
apply isColimitCoforkMapOfIsColimit (forget TopCat)

Result:
case h.l
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsColimit (Cofork.ofπ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base ?h.w)

case h.w
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ f.base ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base =
    g.base ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base

Proof state:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom ((Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s) ≤
    unop ((Opens.map (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).op.obj (op U))

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

Result:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ unop ((Opens.map (Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).op.obj (op U)) ≤
    unop ((Opens.map (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).op.obj (op U))