-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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 : Discrete ι
this_1 :
  Eq (α := (F ⋙ forget C).obj i ⟶ colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) i)
    (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
      (NatTrans.app (Iso.hom Discrete.natIsoFunctor) i ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i)
      (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor)))
this :
  Eq (α :=
    Functor.obj (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as : Discrete ι } ⟶
      colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
    (colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as })
    (TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) i.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv)
⊢ IsOpenEmbedding (X := (↑(↑(F.obj i).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 := (↑(F.obj i).toPresheafedSpace : TopCat)) (Y := (↑(colimit F).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := colimit (F ⋙ forget C))
                (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
                    (NatTrans.app (Iso.hom Discrete.natIsoFunctor) i ≫
                      colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i)
                    (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor)) :
                  (F ⋙ forget C).obj i ⟶ colimit (F ⋙ forget C))
                (Iso.inv (preservesColimitIso (forget C) F) :
                  colimit (F ⋙ forget C) ⟶ Functor.obj (forget C) (colimit F)) :
              (F ⋙ forget C).obj i ⟶ Functor.obj (forget C) (colimit F)) :
          C((↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v),
            (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))) :
      (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) → (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
have mk : ∀ (as : ι)
  (this :
    Eq (α := (F ⋙ forget C).obj { as := as : Discrete ι } ⟶ colimit (F ⋙ forget C))
      (colimit.ι (F ⋙ forget C) { as := as })
      (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
        (NatTrans.app (Iso.hom Discrete.natIsoFunctor) { as := as : Discrete ι } ≫
          colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as })
        (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor))))
  (this :
    Eq (α :=
      Functor.obj (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk))
          { as := { as := as : Discrete ι }.as : Discrete ι } ⟶
        colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
      (colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as }.as })
      (TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as }.as ≫
        (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv)),
  IsOpenEmbedding (X := (↑(↑(F.obj { as := as : Discrete ι }).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 := (↑(F.obj { as := as : Discrete ι }).toPresheafedSpace : TopCat)) (Y :=
            (↑(colimit F).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := colimit (F ⋙ forget C))
                (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
                    (NatTrans.app (Iso.hom Discrete.natIsoFunctor) { as := as : Discrete ι } ≫
                      colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as })
                    (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor)) :
                  (F ⋙ forget C).obj { as := as : Discrete ι } ⟶ colimit (F ⋙ forget C))
                (Iso.inv (preservesColimitIso (forget C) F) :
                  colimit (F ⋙ forget C) ⟶ Functor.obj (forget C) (colimit F)) :
              (F ⋙ forget C).obj { as := as : Discrete ι } ⟶ Functor.obj (forget C) (colimit F)) :
          C((↑(↑(F.obj { as := as : Discrete ι }).toPresheafedSpace : TopCat) : Type v),
            (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))) :
      (a : (↑(↑(F.obj { as := as }).toPresheafedSpace : TopCat) : Type v)) →
        (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
Tactic: cases i
Cleared hypotheses: i, this_1, this