-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
x : (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)
y : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
hy : y ∈ (↑U : Set (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v))
eq :
  Eq (α := (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            Functor.obj (forget C) (colimit F))
            (CategoryStruct.comp (Y := colimit (F ⋙ forget C))
              (Iso.hom (preservesColimitIso (forget C) F) : Functor.obj (forget C) (colimit F) ⟶ colimit (F ⋙ forget C))
              (Iso.hom (HasColimit.isoOfNatIso Discrete.natIsoFunctor) ≫
                  (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom :
                colimit (F ⋙ forget C) ⟶ TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))) :
          (a : (↑((forget C).obj (colimit F)) : Type v)) → (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(colimit F).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι F i))) :
              (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) →
                (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
            y :
          (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v)) :
      (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            Functor.obj (forget C) (colimit F))
            (CategoryStruct.comp (Y := colimit (F ⋙ forget C))
              (Iso.hom (preservesColimitIso (forget C) F) : Functor.obj (forget C) (colimit F) ⟶ colimit (F ⋙ forget C))
              (Iso.hom (HasColimit.isoOfNatIso Discrete.natIsoFunctor) ≫
                  (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom :
                colimit (F ⋙ forget C) ⟶ TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))) :
          (a : (↑((forget C).obj (colimit F)) : Type v)) → (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
                (PresheafedSpace.Hom.base
                  (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
                    (colimit.ι (F ⋙ forgetToPresheafedSpace) j :
                      (F ⋙ forgetToPresheafedSpace).obj j ⟶ colimit (F ⋙ forgetToPresheafedSpace))
                    (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
                      colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))) :
              (a : (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)) →
                (↑(↑(forgetToPresheafedSpace.obj (colimit F)) : TopCat) : Type v))
            x :
          (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v)) :
      (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
⊢ Eq (α := (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            Functor.obj (forget C) (colimit F))
            (CategoryStruct.comp (Y := colimit (F ⋙ forget C))
              (Iso.hom (preservesColimitIso (forget C) F) : Functor.obj (forget C) (colimit F) ⟶ colimit (F ⋙ forget C))
              (Iso.hom (HasColimit.isoOfNatIso Discrete.natIsoFunctor) ≫
                  (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom :
                colimit (F ⋙ forget C) ⟶ TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))) :
          (a : (↑((forget C).obj (colimit F)) : Type v)) → (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(colimit F).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι F i))) :
              (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) →
                (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
            y :
          (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v)) :
      (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            Functor.obj (forget C) (colimit F))
            (CategoryStruct.comp (Y := colimit (F ⋙ forget C))
              (Iso.hom (preservesColimitIso (forget C) F) : Functor.obj (forget C) (colimit F) ⟶ colimit (F ⋙ forget C))
              (Iso.hom (HasColimit.isoOfNatIso Discrete.natIsoFunctor) ≫
                  (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom :
                colimit (F ⋙ forget C) ⟶ TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))) :
          (a : (↑((forget C).obj (colimit F)) : Type v)) → (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
        (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                  (X := (↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat)) (Y :=
                  (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
                  (PresheafedSpace.Hom.base (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F j))) :
                C((↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v),
                  (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))) :
              (a : (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)) →
                (↑(↑(forgetToPresheafedSpace.obj (colimit F)) : TopCat) : Type v))
            x :
          (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v)) :
      (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))

Tactic:
rw [ι_preservesColimitIso_inv] at eq

Premises used: CategoryTheory.ι_preservesColimitIso_inv