awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
B X : CompHausLike P
π : X ⟶ B
hπ :
  Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) π) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
W : CompHausLike P
e : X ⟶ W
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
suffices :
  g =
    ofHom P
      ((⋯.liftEquiv :
          (a :
              { g : C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X, (↑W.toTop : Type u)) //
                Function.FactorsThrough
                  (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
                  (⇑(ConcreteCategory.hom π) :
                    (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                      (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) }) →
            C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B, (↑W.toTop : Type u)))
        (Subtype.mk (p :=
          fun (g : C((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X, (↑(W.toTop (P := P)) : Type u))) ↦
          Function.FactorsThrough (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
            (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B) (γ := (↑(W.toTop (P := P)) : Type u))
            (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                  C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
                  (↑(X.toTop (P := P)) : Type u)) π) :
              (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B))
          (TopCat.Hom.hom e.hom) ⋯))
⊢ g = ofHom P (⋯.lift (TopCat.Hom.hom e.hom) ⋯)

Tactic:
suffices g = ofHom _
        ((IsQuotientMap.of_surjective_continuous hπ π.hom.hom.continuous).liftEquiv ⟨e.hom.hom,
      fun a b hab ↦ CategoryTheory.congr_fun
        (h
          (ofHom _ ⟨fun _ ↦ a, continuous_const⟩)
          (ofHom _ ⟨fun _ ↦ b, continuous_const⟩)
          (by ext; exact hab))
        a⟩) by assumption
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
B X : CompHausLike P
π : X ⟶ B
hπ :
  Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) π) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
W : CompHausLike P
e : X ⟶ W
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X
⊢ Eq (α := (↑(W.toTop (P := P)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) g :
          (a : (↑B.toTop : Type u)) → (↑W.toTop : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
                (↑(X.toTop (P := P)) : Type u)) π :
              (a : (↑X.toTop : Type u)) → (↑B.toTop : Type u))
            a :
          (↑(B.toTop (P := P)) : Type u)) :
      (↑(W.toTop (P := P)) : Type u))
    ((TopCat.Hom.hom (π ≫ g).hom : (a : (↑X.toTop : Type u)) → (↑W.toTop : Type u)) a : (↑(W.toTop (P := P)) : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
⊢ ∃ (W : CompHausLike P) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ π = h ≫ f

Tactic:
⟨pullback f π, pullback.fst f π, ⟨⟨effectiveEpiStruct _ ?_⟩⟩, pullback.snd f π,
      (pullback.condition _ _).symm⟩

Premises used: CompHausLike.pullback.condition, CompHausLike.pullback.fst, CompHausLike.pullback, Nonempty.intro, Exists.intro, CompHausLike.pullback.snd, Eq.symm, CompHausLike.effectiveEpiStruct, CategoryTheory.EffectiveEpi.mk
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
refine :
  Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (pullback (P := P) f π)) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) (X := pullback (P := P) f π) (pullback.fst (P := P) f π)) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (pullback f π)) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
⊢ ∃ (W : CompHausLike P) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ π = h ≫ f

Tactic:
refine ⟨pullback f π, pullback.fst f π, ⟨⟨effectiveEpiStruct _ ?_⟩⟩, pullback.snd f π,
      (pullback.condition _ _).symm⟩
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
y : (↑(X.toTop (P := P)) : Type u)
obtain :
  ∀ (z : (↑(Z.toTop (P := P)) : Type u))
    (hz :
      Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
                (↑(X.toTop (P := P)) : Type u)) π :
              (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) →
                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
            z :
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
                (↑(X.toTop (P := P)) : Type u)) f :
              (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
            y :
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)),
    ∃ (a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (pullback (P := P) f π)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) (X := pullback (P := P) f π) (pullback.fst (P := P) f π) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (pullback f π)) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
          a =
        y
⊢ ∃ (a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (pullback (P := P) f π)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (X := pullback (P := P) f π) (pullback.fst (P := P) f π) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (pullback f π)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        a =
      y

Tactic:
obtain ⟨z, hz⟩ := hs π hπ (f y)

Premises used: CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
y : (↑(X.toTop (P := P)) : Type u)
z : (↑(Z.toTop (P := P)) : Type u)
hz :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) π :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        y :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
⊢ ∃ (a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (pullback (P := P) f π)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (X := pullback (P := P) f π) (pullback.fst (P := P) f π) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (pullback f π)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        a =
      y

Tactic:
⟨⟨(y, z), hz.symm⟩, rfl⟩

Premises used: Prod.mk, Subtype.mk, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
y : (↑(X.toTop (P := P)) : Type u)
z : (↑(Z.toTop (P := P)) : Type u)
hz :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) π :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        y :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
⊢ ∃ (a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (pullback (P := P) f π)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (X := pullback (P := P) f π) (pullback.fst (P := P) f π) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (pullback f π)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        a =
      y

Tactic:
exact ⟨⟨(y, z), hz.symm⟩, rfl⟩
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
inst_1 : HasExplicitFiniteCoproducts P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
⊢ Preregular.{u, u + 1} (CompHausLike P)

Tactic:
have : Preregular (CompHausLike P) := preregular hs
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
inst_1 : HasExplicitFiniteCoproducts P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
this : Preregular.{u, u + 1} (CompHausLike P)
⊢ Precoherent.{u, u + 1} (CompHausLike P)

Tactic:
infer_instance
-- 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
e : (a : α) → X a ⟶ B
hf :
  ∀ (i : α),
    Continuous (Y := (↑B.1 : Type (max u w))) fun (a : (↑((X i).toTop (P := P)) : Type (max u w))) ↦
      match (motive := (a : α) × (↑((X a).toTop (P := P)) : Type (max u w)) → (↑B.1 : Type (max u w)))
        Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) i a with
      | ⟨a, 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))) (e a) :
            (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
⊢ Continuous (Y := (↑B.1 : Type (max u w))) fun (x : (a : α) × (↑((X a).toTop (P := P)) : Type (max u w))) ↦
    match (motive := (a : α) × (↑((X a).toTop (P := P)) : Type (max u w)) → (↑B.1 : Type (max u w))) x with
    | ⟨a, 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))) (e a) :
          (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

Tactic:
apply continuous_sigma

Premises used: continuous_sigma
-- 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
e : (a : α) → X a ⟶ B
a : α
⊢ Continuous (Y := (↑B.1 : Type (max u w))) fun (a_1 : (↑((X a).toTop (P := P)) : Type (max u w))) ↦
    match (motive := (a : α) × (↑((X a).toTop (P := P)) : Type (max u w)) → (↑B.1 : Type (max u w)))
      Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a a_1 with
    | ⟨a, 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))) (e a) :
          (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

Tactic:
(e a).hom.hom.continuous

Premises used: ContinuousMap.continuous, TopCat.Hom.hom, CategoryTheory.InducedCategory.Hom.hom
-- 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
e : (a : α) → X a ⟶ B
a : α
⊢ Continuous (Y := (↑B.1 : Type (max u w))) fun (a_1 : (↑((X a).toTop (P := P)) : Type (max u w))) ↦
    match (motive := (a : α) × (↑((X a).toTop (P := P)) : Type (max u w)) → (↑B.1 : Type (max u w)))
      Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a a_1 with
    | ⟨a, 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))) (e a) :
          (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

Tactic:
exact (e a).hom.hom.continuous

Premises used: ContinuousMap.continuous, TopCat.Hom.hom, CategoryTheory.InducedCategory.Hom.hom
-- 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
e : (a : α) → X a ⟶ B
a : α
⊢ CategoryStruct.comp (Y := finiteCoproduct.{w, u} (P := P) X) (ι (P := P) X a) (desc (P := P) X e) = e a

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- 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
h : ∀ (a : α), ι (P := P) X a ≫ f = ι (P := P) X a ≫ g
h₁ :
  ∀ (a : α) (x : (↑((X a).toTop (P := P)) : Type (max u w))),
    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)))
⊢ f = g

Tactic:
ext ⟨a, x⟩
-- 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
h : ∀ (a : α), ι (P := P) X a ≫ f = ι (P := P) X a ≫ g
a : α
x : (↑((X a).toTop (P := P)) : Type (max u w))
⊢ ι (P := P) X a ≫ f = ι (P := P) X a ≫ g

Tactic:
specialize h a
-- 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 : ι (P := P) X a ≫ f = ι (P := P) X a ≫ g
⊢ 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)

Tactic:
apply_fun (fun q ↦ q x) at h