awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
this : PreservesFiniteCoproducts (toCompHausLike (P := P) (P' := P') h ⋙ compHausLikeToTop P')
⊢ PreservesFiniteCoproducts (toCompHausLike (P := P) (P' := P') h)

Tactic:
preservesFiniteCoproducts_of_reflects_of_preserves (toCompHausLike h) (compHausLikeToTop P')

Premises used: CompHausLike.toCompHausLike, CompHausLike.compHausLikeToTop, CategoryTheory.Limits.preservesFiniteCoproducts_of_reflects_of_preserves
-- 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))
this : PreservesFiniteCoproducts (toCompHausLike (P := P) (P' := P') h ⋙ compHausLikeToTop P')
⊢ PreservesFiniteCoproducts (toCompHausLike (P := P) (P' := P') h)

Tactic:
exact preservesFiniteCoproducts_of_reflects_of_preserves (toCompHausLike h) (compHausLikeToTop P')

Premises used: CompHausLike.toCompHausLike, CompHausLike.compHausLikeToTop, CategoryTheory.Limits.preservesFiniteCoproducts_of_reflects_of_preserves
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
z : (↑(Z.toTop (P := P)) : Type u)
⊢ Eq (α := (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 ≫ f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
        z :
      (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)) (b ≫ g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)

Tactic:
apply_fun (fun q ↦ q z) at w
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ Continuous (Y := (↑((pullback (P := P) f g).toTop (P := P)) : Type u)) fun (z : (↑(Z.toTop (P := P)) : Type u)) ↦
    Subtype.mk (p := fun (x : (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)) ↦
      Membership.mem (γ := Set ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)))
        {xy : (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u) |
          Eq (α := (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)) f :
                  (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                    (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
                xy.1 :
              (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)) g :
                  (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                    (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
                xy.2 :
              (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)}
        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)) a :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
          z,
        (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)) b :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
          z)
      ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ CategoryStruct.comp (Y := pullback (P := P) f g) (lift (P := P) f g a b w) (fst (P := P) f g) = a

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ CategoryStruct.comp (Y := pullback (P := P) f g) (lift (P := P) f g a b w) (snd (P := P) f g) = b

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a b : Z ⟶ pullback (P := P) f g
hfst : a ≫ fst (P := P) f g = b ≫ fst (P := P) f g
hsnd : a ≫ snd (P := P) f g = b ≫ snd (P := P) f g
h :
  ∀ (z : (↑(Z.toTop (P := P)) : Type u)),
    Eq (α := (↑((pullback (P := P) f g).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)) a :
            (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
          z :
        (↑((pullback (P := P) f g).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)) b :
            (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
          z :
        (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
⊢ a = b

Tactic:
ext z
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a b : Z ⟶ pullback (P := P) f g
hfst : a ≫ fst (P := P) f g = b ≫ fst (P := P) f g
hsnd : a ≫ snd (P := P) f g = b ≫ snd (P := P) f g
z : (↑(Z.toTop (P := P)) : Type u)
⊢ Eq (α := (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)) (a ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (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)) (b ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)

Tactic:
apply_fun (fun q ↦ q z) at hfst hsnd
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a b : Z ⟶ pullback (P := P) f g
hfst : a ≫ fst (P := P) f g = b ≫ fst (P := P) f g
hsnd : a ≫ snd (P := P) f g = b ≫ snd (P := P) f g
z : (↑(Z.toTop (P := P)) : Type u)
hfst₁ :
  Eq (α := (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)) (a ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (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)) (b ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
⊢ 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 ≫ snd (P := P) f g) :
          (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)) (b ≫ snd (P := P) f g) :
          (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)

Tactic:
apply_fun (fun q ↦ q z) at hfst hsnd
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a b : Z ⟶ pullback (P := P) f g
z : (↑(Z.toTop (P := P)) : Type u)
hfst :
  Eq (α := (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)) (a ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (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)) (b ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
hsnd :
  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 ≫ snd (P := P) f g) :
          (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)) (b ≫ snd (P := P) f g) :
          (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)
⊢ Eq.{u + 1} (α := (↑(X.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)) a :
              (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
            z) :
        (↑X.toTop : Type u) × (↑Y.toTop : Type u)).1
    (↑((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)) b :
              (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
            z) :
        (↑X.toTop : Type u) × (↑Y.toTop : Type u)).1

Tactic:
hfst
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a b : Z ⟶ pullback (P := P) f g
z : (↑(Z.toTop (P := P)) : Type u)
hfst :
  Eq (α := (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)) (a ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (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)) (b ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
hsnd :
  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 ≫ snd (P := P) f g) :
          (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)) (b ≫ snd (P := P) f g) :
          (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)
⊢ Eq.{u + 1} (α := (↑(X.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)) a :
              (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
            z) :
        (↑X.toTop : Type u) × (↑Y.toTop : Type u)).1
    (↑((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)) b :
              (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
            z) :
        (↑X.toTop : Type u) × (↑Y.toTop : Type u)).1

Tactic:
exact hfst
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a b : Z ⟶ pullback (P := P) f g
z : (↑(Z.toTop (P := P)) : Type u)
hfst :
  Eq (α := (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)) (a ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (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)) (b ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
hsnd :
  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 ≫ snd (P := P) f g) :
          (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)) (b ≫ snd (P := P) f g) :
          (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)
⊢ Eq.{u + 1} (α := (↑(Y.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)) a :
              (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
            z) :
        (↑X.toTop : Type u) × (↑Y.toTop : Type u)).2
    (↑((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)) b :
              (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
            z) :
        (↑X.toTop : Type u) × (↑Y.toTop : Type u)).2

Tactic:
hsnd
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a b : Z ⟶ pullback (P := P) f g
z : (↑(Z.toTop (P := P)) : Type u)
hfst :
  Eq (α := (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)) (a ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (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)) (b ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
hsnd :
  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 ≫ snd (P := P) f g) :
          (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)) (b ≫ snd (P := P) f g) :
          (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)
⊢ Eq.{u + 1} (α := (↑(Y.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)) a :
              (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
            z) :
        (↑X.toTop : Type u) × (↑Y.toTop : Type u)).2
    (↑((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)) b :
              (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
            z) :
        (↑X.toTop : Type u) × (↑Y.toTop : Type u)).2

Tactic:
exact hsnd
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
⊢ cospan f.hom g.hom ≅ cospan f.hom g.hom

Tactic:
rfl
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
⊢ PreservesLimit (cospan f g) (compHausLikeToTop P)

Tactic:
preservesLimit_of_createsLimit_and_hasLimit _ _

Premises used: CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
P' : TopCat.{u} → Prop
h : ∀ (X : CompHausLike P), P (X.toTop (P := P)) → P' (X.toTop (P := P))
⊢ PreservesLimit (cospan f g) (toCompHausLike (P := P) (P' := P') h ⋙ compHausLikeToTop P')

Tactic:
have : PreservesLimit (cospan f g) (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesLimit _ (compHausLikeToTop _))