-- 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 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 (imageBasicOpen f g U s) = (Opens.map g.base).obj (imageBasicOpen f g U s)

Tactic:
delta imageBasicOpen

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))
⊢ (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))

Proof state:
case e.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))
a✝ : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom (f.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) a✝ =
    (ConcreteCategory.hom (g.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) a✝

Tactic:
congr 3

Result:
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)

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 f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).op.obj (op U)) ⊓
      X.toRingedSpace.basicOpen
        ((ConcreteCategory.hom ((Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (g.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).toPrefunctor.1 U))))
        ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s))

Tactic:
apply inf_eq_right.mpr

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 ((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))

Proof state:
case e
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))
⊢ ⇑(ConcreteCategory.hom f.base) ≫ ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) =
    ⇑(ConcreteCategory.hom g.base) ≫ ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base)

Tactic:
ext

Result:
case e.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))
a✝ : ↑↑X.toPresheafedSpace
⊢ (⇑(ConcreteCategory.hom f.base) ≫ ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base)) a✝ =
    (⇑(ConcreteCategory.hom g.base) ≫ ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base)) a✝

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
          (f.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).toPrefunctor.1 U))))
        ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s)) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (g.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).toPrefunctor.1 U))))
        ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s))

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

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 f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).op.obj (op U)) ⊓
      X.toRingedSpace.basicOpen
        ((ConcreteCategory.hom ((Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (g.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).toPrefunctor.1 U))))
        ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s))

Proof state:
case e.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))
a✝ : ↑↑X.toPresheafedSpace
⊢ (⇑(ConcreteCategory.hom f.base) ≫ ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base)) a✝ =
    (⇑(ConcreteCategory.hom g.base) ≫ ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base)) a✝

Tactic:
simp_rw [types_comp_apply, ← TopCat.comp_app, ← PresheafedSpace.comp_base]

Result:
case e.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))
a✝ : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom (f.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) a✝ =
    (ConcreteCategory.hom (g.toHom ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) a✝

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

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))
⊢ (Opens.map f.base).obj (imageBasicOpen f g U s) = (Opens.map g.base).obj (imageBasicOpen f g U s)