-- Mathlib/Topology/Category/CompHausLike/Limits.lean
/-- The inclusion maps into the abstract finite coproduct are open embeddings. -/
lemma Sigma.isOpenEmbedding_ι (a : α) :
    IsOpenEmbedding (Sigma.ι X a)

Proof state:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ IsOpenEmbedding
    (⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘
      ⇑(ConcreteCategory.hom (Sigma.ι X a)))

Tactic:
convert finiteCoproduct.isOpenEmbedding_ι X a

Result:
case h.e'_5.h
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
e_2✝ : ↑(finiteCoproduct.cofan X).pt.toTop = (fun X => ↑X.toTop) (finiteCoproduct X)
⊢ ⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘
      ⇑(ConcreteCategory.hom (Sigma.ι X a)) =
    ⇑(ConcreteCategory.hom (finiteCoproduct.ι X a))

Proof state:
case h.e'_5.h.h
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
e_2✝ : ↑(finiteCoproduct.cofan X).pt.toTop = (fun X => ↑X.toTop) (finiteCoproduct X)
x : (fun X => ↑X.toTop) (X a)
⊢ (ConcreteCategory.hom
        (Sigma.ι X a ≫
          ((compHausLikeToTop P).mapIso
              ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))).hom))
      x =
    (ConcreteCategory.hom (finiteCoproduct.ι X a)) x

Tactic:
simp

Result:
no goals

Proof state:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (Sigma.ι X a))

Tactic:
refine IsOpenEmbedding.of_comp _ (homeoOfIso ((colimit.isColimit _).coconePointUniqueUpToIso
  (finiteCoproduct.isColimit X))).isOpenEmbedding ?_

Result:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ IsOpenEmbedding
    (⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘
      ⇑(ConcreteCategory.hom (Sigma.ι X a)))

Proof state:
case h.e'_5.h.h
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
e_2✝ : ↑(finiteCoproduct.cofan X).pt.toTop = (fun X => ↑X.toTop) (finiteCoproduct X)
x : (fun X => ↑X.toTop) (X a)
⊢ (⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘
        ⇑(ConcreteCategory.hom (Sigma.ι X a)))
      x =
    (ConcreteCategory.hom (finiteCoproduct.ι X a)) x

Tactic:
change (Sigma.ι X a ≫ _) x = _

Result:
case h.e'_5.h.h
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
e_2✝ : ↑(finiteCoproduct.cofan X).pt.toTop = (fun X => ↑X.toTop) (finiteCoproduct X)
x : (fun X => ↑X.toTop) (X a)
⊢ (ConcreteCategory.hom
        (Sigma.ι X a ≫
          ((compHausLikeToTop P).mapIso
              ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))).hom))
      x =
    (ConcreteCategory.hom (finiteCoproduct.ι X a)) x

Proof state:
case h.e'_5.h
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
e_2✝ : ↑(finiteCoproduct.cofan X).pt.toTop = (fun X => ↑X.toTop) (finiteCoproduct X)
⊢ ⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘
      ⇑(ConcreteCategory.hom (Sigma.ι X a)) =
    ⇑(ConcreteCategory.hom (finiteCoproduct.ι X a))

Tactic:
ext x

Result:
case h.e'_5.h.h
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
e_2✝ : ↑(finiteCoproduct.cofan X).pt.toTop = (fun X => ↑X.toTop) (finiteCoproduct X)
x : (fun X => ↑X.toTop) (X a)
⊢ (⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘
        ⇑(ConcreteCategory.hom (Sigma.ι X a)))
      x =
    (ConcreteCategory.hom (finiteCoproduct.ι X a)) x