-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem image_preimage_is_empty (j : Discrete ι) (h : i ≠ j) (U : Opens (F.obj i)) :
    (Opens.map (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) j).base).obj
        ((Opens.map (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv.base).obj
          ((sigma_ι_isOpenEmbedding F i).isOpenMap.functor.obj U)) =
      ⊥

Proof state:
case h.h.h.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  ((preservesColimitIso (forget C) F).hom ≫
        (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
          (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (colimit.ι F i).base) y) =
    ((preservesColimitIso (forget C) F).hom ≫
        (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
          (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (forgetToPresheafedSpace.map (colimit.ι F j)).base) x)
⊢ False

Tactic:
change
  ((SheafedSpace.forget C).map (colimit.ι F i) ≫ _) y =
    ((SheafedSpace.forget C).map (colimit.ι F j) ≫ _) x at eq

Result:
case h.h.h.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((forget C).map (colimit.ι F i) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      y =
    (ConcreteCategory.hom
        ((forget C).map (colimit.ι F j) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      x
⊢ False

Proof state:
case h.h.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
⊢ x ∉
    ↑((Opens.map (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base).obj
        ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U)))

Tactic:
rintro ⟨y, hy, eq⟩

Result:
case h.h.h.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom (colimit.ι F i).base) y =
    (ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
      ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x)
⊢ False