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

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))
⊢ IsOpen
    (⇑(ConcreteCategory.hom ((SheafedSpace.forget CommRingCat).map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ''
        (imageBasicOpen f g U s).carrier))

Tactic:
dsimp only [SheafedSpace.forget]

Result:
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))
⊢ IsOpen
    (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ''
        (imageBasicOpen f g U s).carrier))

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))
⊢ IsOpen (imageBasicOpen f g U s).carrier

Tactic:
exact (imageBasicOpen f g U s).2

Result:
no goals

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))
⊢ IsOpen
    (⇑(ConcreteCategory.hom
          (coequalizer.π ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
              ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g)) ≫
            (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g)).hom)) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ''
        (imageBasicOpen f g U s).carrier))

Tactic:
rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]

Result:
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))
⊢ IsOpen
    (⇑(ConcreteCategory.hom ((SheafedSpace.forget CommRingCat).map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ''
        (imageBasicOpen f g U s).carrier))

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))
⊢ IsOpen
    (⇑(TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g))) ∘
        ⇑(ConcreteCategory.hom
            (coequalizer.π ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
              ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g)))) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ''
        (imageBasicOpen f g U s).carrier))

Tactic:
erw [← TopCat.coe_comp]

Result:
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))
⊢ IsOpen
    (⇑(ConcreteCategory.hom
          (coequalizer.π ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
              ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g)) ≫
            (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g)).hom)) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ''
        (imageBasicOpen f g U s).carrier))

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))
⊢ IsOpen
    (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ''
        (imageBasicOpen f g U s).carrier))

Tactic:
rw [imageBasicOpen_image_preimage]

Result:
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))
⊢ IsOpen (imageBasicOpen f g U s).carrier

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))
⊢ IsOpen
    (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' (imageBasicOpen f g U s).carrier)

Tactic:
rw [← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.toShHom
  g.toShHom)).isOpen_preimage, TopCat.coequalizer_isOpen_iff, ← Set.preimage_comp]

Result:
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))
⊢ IsOpen
    (⇑(TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g))) ∘
        ⇑(ConcreteCategory.hom
            (coequalizer.π ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
              ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g)))) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ''
        (imageBasicOpen f g U s).carrier))