-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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 (α := (↑(↑(colimit F).toPresheafedSpace : TopCat) : 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))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat)) (Y :=
              (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
              (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F)) :
                (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) ⟶
                  (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat)) :
            C((↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v),
              (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))) :
          (a : (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v)) →
            (↑(↑(forgetToPresheafedSpace.obj (colimit F)) : TopCat) : Type v))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat))
                (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
              (a : (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)) →
                (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
            x :
          (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v)) :
      (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
⊢ False
have eq₁ : Eq (α := (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : 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))
          (Iso.hom
            (Iso.trans (Y := colimit (F ⋙ forget C))
              (preservesColimitIso (forget C) F : Functor.obj (forget C) (colimit F) ≅ colimit (F ⋙ forget C))
              (HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
                  TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk) :
                colimit (F ⋙ forget C) ≅ TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))))) :
        (a : (↑((forget C).obj (colimit F)) : Type v)) →
          (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : 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)) :
    (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : 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))
          (Iso.hom
            (Iso.trans (Y := colimit (F ⋙ forget C))
              (preservesColimitIso (forget C) F : Functor.obj (forget C) (colimit F) ≅ colimit (F ⋙ forget C))
              (HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
                  TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk) :
                colimit (F ⋙ forget C) ≅ TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))))) :
        (a : (↑((forget C).obj (colimit F)) : Type v)) →
          (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (X := (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat)) (Y :=
                (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
                (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F)) :
                  (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) ⟶
                    (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat)) :
              C((↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v),
                (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))) :
            (a : (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v)) →
              (↑(↑(forgetToPresheafedSpace.obj (colimit F)) : TopCat) : Type v))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                  (Y := (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat))
                  (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
                (a : (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)) →
                  (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
              x :
            (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v)) :
        (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v)) :
    (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
Tactic: replace eq := ConcreteCategory.congr_arg (preservesColimitIso (SheafedSpace.forget C) F ≪≫
    HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma.{v, v} _).hom eq
Cleared hypotheses: eq