-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem sigma_ι_isOpenEmbedding : IsOpenEmbedding (colimit.ι F i).base

Proof state:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  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
    ⇑(ConcreteCategory.hom
        ((((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
                TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as) ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Tactic:
rw [TopCat.isOpenEmbedding_iff_comp_isIso, TopCat.isOpenEmbedding_iff_comp_isIso,
  TopCat.isOpenEmbedding_iff_comp_isIso, TopCat.isOpenEmbedding_iff_isIso_comp]

Result:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  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 ⇑(ConcreteCategory.hom (TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this :
  colimit.ι (F ⋙ forget C) i ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom =
    Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) i ≫ (preservesColimitIso (forget C) F).inv))

Tactic:
rw [← Iso.eq_comp_inv] at this

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this :
  colimit.ι (F ⋙ forget C) i =
    (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) i ≫ (preservesColimitIso (forget C) F).inv))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this✝ :
  colimit.ι (F ⋙ forget C) i =
    (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  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
    ⇑(ConcreteCategory.hom
        (((Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Tactic:
cases i

Result:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  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
    ⇑(ConcreteCategory.hom
        (((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
              colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this✝ :
  colimit.ι (F ⋙ forget C) i =
    (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as } ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) i.as
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (((Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Tactic:
rw [← Iso.eq_comp_inv] at this

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this✝ :
  colimit.ι (F ⋙ forget C) i =
    (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  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
    ⇑(ConcreteCategory.hom
        (((Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))