awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
B : CompHausLike P
f g : finiteCoproduct.{w, u} (P := P) X ⟶ B
a : α
x : (↑((X a).toTop (P := P)) : Type (max u w))
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (ι (P := P) X a ≫ f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (ι (P := P) X a ≫ g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
⊢ Eq (α := (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) f :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) g :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))

Tactic:
h
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
B : CompHausLike P
f g : finiteCoproduct.{w, u} (P := P) X ⟶ B
a : α
x : (↑((X a).toTop (P := P)) : Type (max u w))
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (ι (P := P) X a ≫ f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (ι (P := P) X a ≫ g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
⊢ Eq (α := (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) f :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) g :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))

Tactic:
exact h
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
x y : (↑((X a).toTop (P := P)) : Type (max u w))
hxy :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
            (ι (P := P) X a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
            (ι (P := P) X a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
        y :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))
⊢ x = y

Tactic:
eq_of_heq (Sigma.ext_iff.mp hxy).2

Premises used: Sigma.ext_iff, And.right, Iff.mp, eq_of_heq
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
x y : (↑((X a).toTop (P := P)) : Type (max u w))
hxy :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
            (ι (P := P) X a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
            (ι (P := P) X a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
        y :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))
⊢ x = y

Tactic:
exact eq_of_heq (Sigma.ext_iff.mp hxy).2

Premises used: Sigma.ext_iff, And.right, Iff.mp, eq_of_heq
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
R : (↑((finiteCoproduct.{w, u} (P := P) X).toTop (P := P)) : Type (max u w))
⊢ ∃ (a : α) (r : (↑((X a).toTop (P := P)) : Type (max u w))),
    R =
      (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
            (ι (P := P) X a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
        r

Tactic:
⟨R.fst, R.snd, rfl⟩

Premises used: Sigma.fst, Exists.intro, Sigma.snd, rfl
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α_1 : Type w
inst : Finite α_1
X : α_1 → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
inst_2 : HasExplicitFiniteCoproducts.{w, u} P
n : ℕ
α : Type w := ULift.{w, 0} (Fin n)
e : Discrete α ≌ Discrete (Fin n) := Discrete.equivalence Equiv.ulift
⊢ HasColimitsOfShape (Discrete (Fin n)) (CompHausLike P)

Tactic:
hasColimitsOfShape_of_equivalence e

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α_1 : Type w
inst : Finite α_1
X : α_1 → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
inst_2 : HasExplicitFiniteCoproducts.{w, u} P
n : ℕ
α : Type w := ULift.{w, 0} (Fin n)
e : Discrete α ≌ Discrete (Fin n) := Discrete.equivalence Equiv.ulift
⊢ HasColimitsOfShape (Discrete (Fin n)) (CompHausLike P)

Tactic:
exact hasColimitsOfShape_of_equivalence e

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P
⊢ HasFiniteCoproducts.{u, u + 1} (CompHausLike P)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
⊢ IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
          fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
          (ι (P := P) X a)) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))

Tactic:
.sigmaMk (σ := fun a ↦ X a)

Premises used: Topology.IsOpenEmbedding.sigmaMk
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
refine :
  IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)) (Y :=
    (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)))
    (Function.comp (β := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (∐ X))
      (⇑(homeoOfIso (P := P)
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
              (finiteCoproduct.isColimit (P := P) X))) :
        (a : (↑(colimit.cocone (Discrete.functor X)).pt.toTop : Type (max u w))) →
          (↑(finiteCoproduct.cofan X).pt.toTop : Type (max u w)))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := ∐ X) (Sigma.ι X a)) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (∐ X)))
⊢ IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (∐ X))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
          fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := ∐ X) (Sigma.ι X a)) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (∐ X))

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

Premises used: CategoryTheory.Limits.colimit.isColimit, CompHausLike.finiteCoproduct.isColimit, CompHausLike.homeoOfIso, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.of_comp, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
⊢ IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
          fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
          (finiteCoproduct.ι (P := P) X a)) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))

Tactic:
finiteCoproduct.isOpenEmbedding_ι X a

Premises used: CompHausLike.finiteCoproduct.isOpenEmbedding_ι
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
h :
  (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)) =
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X) →
    Eq (α :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a) →
        (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)))
      (Function.comp (β := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (∐ X))
        (⇑(homeoOfIso (P := P)
              (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
                (finiteCoproduct.isColimit (P := P) X))) :
          (a : (↑(colimit.cocone (Discrete.functor X)).pt.toTop : Type (max u w))) →
            (↑(finiteCoproduct.cofan X).pt.toTop : Type (max u w)))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
              fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := ∐ X) (Sigma.ι X a)) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (∐ X)))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
            (finiteCoproduct.ι (P := P) X a)) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
⊢ IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)) (Y :=
    (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)))
    (Function.comp (β := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (∐ X))
      (⇑(homeoOfIso (P := P)
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
              (finiteCoproduct.isColimit (P := P) X))) :
        (a : (↑(colimit.cocone (Discrete.functor X)).pt.toTop : Type (max u w))) →
          (↑(finiteCoproduct.cofan X).pt.toTop : Type (max u w)))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := ∐ X) (Sigma.ι X a)) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (∐ X)))

Tactic:
convert! finiteCoproduct.isOpenEmbedding_ι X a

Premises used: CompHausLike.finiteCoproduct.isOpenEmbedding_ι
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
e_2 :
  (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)) =
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X)
x : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)
⊢ Eq (α :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.cofan.{w, u} (P := P) X).pt)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y :=
            (finiteCoproduct.cofan.{w, u} (P := P) X).pt)
            (CategoryStruct.comp (Y := ∐ X) (Sigma.ι X a)
              (Iso.hom
                (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
                  (finiteCoproduct.isColimit (P := P) X)))) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct.cofan X).pt)
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.cofan.{w, u} (P := P) X).pt)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
            (finiteCoproduct.ι (P := P) X a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))

Tactic:
simp
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P_2 : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P_2
P : TopCat.{u_1} → Prop
inst_3 : HasExplicitFiniteCoproducts P
⊢ PreservesFiniteCoproducts (compHausLikeToTop P)

Tactic:
⟨fun n ↦ ⟨fun {F} ↦ ?_⟩⟩

Premises used: CategoryTheory.Limits.PreservesFiniteCoproducts.mk, CategoryTheory.Limits.PreservesColimitsOfShape.mk
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P_2 : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P_2
P : TopCat.{u_1} → Prop
inst_3 : HasExplicitFiniteCoproducts P
refine : ∀ (n : ℕ) {F : Discrete (Fin n) ⥤ CompHausLike P}, PreservesColimit F (compHausLikeToTop P)
⊢ PreservesFiniteCoproducts (compHausLikeToTop P)

Tactic:
refine ⟨fun n ↦ ⟨fun {F} ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P_2 : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P_2
P : TopCat.{u_1} → Prop
inst_3 : HasExplicitFiniteCoproducts P
n : ℕ
F : Discrete (Fin n) ⥤ CompHausLike P
suffices : PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P)
⊢ PreservesColimit F (compHausLikeToTop P)

Tactic:
suffices PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P) from
    preservesColimit_of_iso_diagram _ Discrete.natIsoFunctor.symm
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P_2 : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P_2
P : TopCat.{u_1} → Prop
inst_3 : HasExplicitFiniteCoproducts P
n : ℕ
F : Discrete (Fin n) ⥤ CompHausLike P
⊢ PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P)

Tactic:
preservesColimit_of_preserves_colimit_cocone (CompHausLike.finiteCoproduct.isColimit _)
    ((isColimitMapCoconeCofanMkEquiv _ _ _).2 (TopCat.sigmaCofanIsColimit _))

Premises used: TopCat.sigmaCofanIsColimit, CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv, CompHausLike.finiteCoproduct.isColimit, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone, Equiv.invFun
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P_2 : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P_2
P : TopCat.{u_1} → Prop
inst_3 : HasExplicitFiniteCoproducts P
n : ℕ
F : Discrete (Fin n) ⥤ CompHausLike P
⊢ PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P)

Tactic:
exact preservesColimit_of_preserves_colimit_cocone (CompHausLike.finiteCoproduct.isColimit _)
    ((isColimitMapCoconeCofanMkEquiv _ _ _).2 (TopCat.sigmaCofanIsColimit _))
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P
P' : TopCat.{u} → Prop
h : ∀ (X : CompHausLike P), P (X.toTop (P := P)) → P' (X.toTop (P := P))
⊢ PreservesFiniteCoproducts (toCompHausLike (P := P) (P' := P') h ⋙ compHausLikeToTop P')

Tactic:
have : PreservesFiniteCoproducts (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesFiniteCoproducts (compHausLikeToTop _))