-- 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.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
        (Discrete.natIsoFunctor.hom.app { as := as✝¹ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝¹))
      y =
    (ConcreteCategory.hom
        (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝))
      x
⊢ False

Tactic:
exact h (congr_arg Discrete.mk (congr_arg Sigma.fst eq))

Result:
no goals

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 ≪≫
          HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom
      ((ConcreteCategory.hom (colimit.ι F i).base) y) =
    (preservesColimitIso (forget C) F ≪≫
          HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom
      ((ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x))
⊢ False

Tactic:
simp_rw [CategoryTheory.Iso.trans_hom, ← TopCat.comp_app, ← PresheafedSpace.comp_base] 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
          (colimit.ι (F ⋙ forgetToPresheafedSpace) j ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
        x)
⊢ False

Proof state:
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 ∈ ↑⊥

Tactic:
apply iff_false_intro

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

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 (colimit.ι F i).base) y =
    (ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
      ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x)
⊢ False

Tactic:
replace eq := ConcreteCategory.congr_arg (preservesColimitIso (SheafedSpace.forget C) F ≪≫
  HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma.{v, v} _).hom 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 ≪≫
          HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom
      ((ConcreteCategory.hom (colimit.ι F i).base) y) =
    (preservesColimitIso (forget C) F ≪≫
          HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom
      ((ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x))
⊢ False

Proof state:
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

Tactic:
rw [ι_preservesColimitIso_hom_assoc, ι_preservesColimitIso_hom_assoc,
  HasColimit.isoOfNatIso_ι_hom_assoc, HasColimit.isoOfNatIso_ι_hom_assoc,
  TopCat.sigmaIsoSigma_hom_ι, TopCat.sigmaIsoSigma_hom_ι] at eq

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
        (Discrete.natIsoFunctor.hom.app { as := as✝¹ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝¹))
      y =
    (ConcreteCategory.hom
        (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝))
      x
⊢ False