-- 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:
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
⊢ (Opens.map (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base).obj
      ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U)) =
    ⊥

Tactic:
ext x

Result:
case 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))) ↔
    x ∈ ↑⊥

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

Tactic:
cases i

Result:
case h.h.h.intro.intro.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
j : Discrete ι
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
as✝ : ι
h : { as := as✝ } ≠ j
U : Opens ↑↑(F.obj { as := as✝ }).toPresheafedSpace
y : ↑↑(F.obj { as := as✝ }).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((forget C).map (colimit.ι F { as := as✝ }) ≫
          (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.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
          (colimit.ι (F ⋙ forgetToPresheafedSpace) j ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
        x)
⊢ False

Tactic:
rw [ι_preservesColimitIso_inv] 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 :
  ((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

Proof state:
case h.h.h.intro.intro.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
j : Discrete ι
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
as✝ : ι
h : { as := as✝ } ≠ j
U : Opens ↑↑(F.obj { as := as✝ }).toPresheafedSpace
y : ↑↑(F.obj { as := as✝ }).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((forget C).map (colimit.ι F { as := as✝ }) ≫
          (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

Tactic:
cases j

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