awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
m : of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ s.pt
h₁ : ofHom { toFun := Sum.inl, continuous_toFun := ⋯ : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inl
h₂ : ofHom { toFun := Sum.inr, continuous_toFun := ⋯ : C((↑Y : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inr
x : (↑X : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
          (a : (↑(of ((↑X : Type u) ⊕ (↑Y : Type u))) : Type u)) → (↑s.pt : Type u))
        (Sum.inl x) :
      (↑s.pt : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (of ((↑X : Type u) ⊕ (↑Y : Type u))) s.pt
            ((fun (s : BinaryCofan X Y) ↦
                (ofHom
                    {
                      toFun :=
                        Sum.elim
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                (CC := carrier) s.inl) :
                            (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                              (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) :
                                Type u))
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                (CC := carrier) s.inr) :
                            (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                              (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                                Type u)),
                      continuous_toFun := ⋯ } :
                  of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
              s) :
          (a : (↑(of ((↑X : Type u) ⊕ (↑Y : Type u))) : Type u)) → (↑s.pt : Type u))
        (Sum.inl x) :
      (↑s.pt : Type u))

Tactic:
ConcreteCategory.congr_hom h₁ x

Premises used: CategoryTheory.ConcreteCategory.congr_hom, Sum.elim
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
m : of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ s.pt
h₁ : ofHom { toFun := Sum.inl, continuous_toFun := ⋯ : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inl
h₂ : ofHom { toFun := Sum.inr, continuous_toFun := ⋯ : C((↑Y : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inr
x : (↑Y : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
          (a : (↑(of ((↑X : Type u) ⊕ (↑Y : Type u))) : Type u)) → (↑s.pt : Type u))
        (Sum.inr x) :
      (↑s.pt : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (of ((↑X : Type u) ⊕ (↑Y : Type u))) s.pt
            ((fun (s : BinaryCofan X Y) ↦
                (ofHom
                    {
                      toFun :=
                        Sum.elim
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                (CC := carrier) s.inl) :
                            (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                              (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) :
                                Type u))
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                (CC := carrier) s.inr) :
                            (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                              (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                                Type u)),
                      continuous_toFun := ⋯ } :
                  of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
              s) :
          (a : (↑(of ((↑X : Type u) ⊕ (↑Y : Type u))) : Type u)) → (↑s.pt : Type u))
        (Sum.inr x) :
      (↑s.pt : Type u))

Tactic:
ConcreteCategory.congr_hom h₂ x

Premises used: CategoryTheory.ConcreteCategory.congr_hom, Sum.elim
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
m : of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ s.pt
h₁ : ofHom { toFun := Sum.inl, continuous_toFun := ⋯ : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inl
h₂ : ofHom { toFun := Sum.inr, continuous_toFun := ⋯ : C((↑Y : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inr
x : (↑X : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
          (a : (↑(of ((↑X : Type u) ⊕ (↑Y : Type u))) : Type u)) → (↑s.pt : Type u))
        (Sum.inl x) :
      (↑s.pt : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (of ((↑X : Type u) ⊕ (↑Y : Type u))) s.pt
            ((fun (s : BinaryCofan X Y) ↦
                (ofHom
                    {
                      toFun :=
                        Sum.elim
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                (CC := carrier) s.inl) :
                            (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                              (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) :
                                Type u))
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                (CC := carrier) s.inr) :
                            (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                              (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                                Type u)),
                      continuous_toFun := ⋯ } :
                  of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
              s) :
          (a : (↑(of ((↑X : Type u) ⊕ (↑Y : Type u))) : Type u)) → (↑s.pt : Type u))
        (Sum.inl x) :
      (↑s.pt : Type u))

Tactic:
exacts [ConcreteCategory.congr_hom h₁ x, ConcreteCategory.congr_hom h₂ x]

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑c.pt : Type u))
      (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))) ∧
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
        (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
            (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))) ∧
      IsCompl (α := Set (↑c.pt : Type u))
        (range (ι := (↑X : Type u))
          (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
            (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
              (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
            (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
                  C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
              (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
        (range (ι := (↑Y : Type u))
          (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
            (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
              (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
            (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                  C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
              (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))

Tactic:
⟨(homeoOfIso <| h.coconePointUniqueUpToIso
        (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inl,
          (homeoOfIso <| h.coconePointUniqueUpToIso
            (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inr, ?_⟩

Premises used: Topology.IsOpenEmbedding.inr, TopCat.homeoOfIso, Homeomorph.symm, And.intro, Topology.IsOpenEmbedding.inl, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp, TopCat.binaryCofanIsColimit, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
mp :
  Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑X : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
    (range (ι := (↑Y : Type u))
        (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
            (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
⊢ IsCompl (α := Set (↑c.pt : Type u))
    (range (ι := (↑X : Type u))
      (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
    (range (ι := (↑Y : Type u))
      (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
              C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))

Tactic:
rw [Set.range_comp, ← eq_compl_iff_isCompl]

Premises used: Set.range_comp, eq_compl_iff_isCompl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
rw :
  (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑Y : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
              C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
| (range (ι := (↑Y : Type u))
      (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
              C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ

Tactic:
rw [Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
mp :
  Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑X : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (range (ι := (↑Y : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
⊢ Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑X : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
    (range (ι := (↑Y : Type u))
        (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
            (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ

Tactic:
conv_rhs => rw [Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous.{u, u} (X :=
    { p : (↑X : Type u) × (↑Y : Type u) //
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
              (a : (↑X : Type u)) → (↑Z : Type u))
            p.1 :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
              (a : (↑Y : Type u)) → (↑Z : Type u))
            p.2 :
          (↑Z : Type u)) })
    (Prod.fst ∘
      Subtype.val (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
        Eq (α := (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                (a : (↑X : Type u)) → (↑Z : Type u))
              p.1 :
            (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                (a : (↑Y : Type u)) → (↑Z : Type u))
              p.2 :
            (↑Z : Type u))))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x :
  (↑(of
        { p : (↑X : Type u) × (↑Y : Type u) //
          Eq (α := (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                  (a : (↑X : Type u)) → (↑Z : Type u))
                p.1 :
              (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                  (a : (↑Y : Type u)) → (↑Z : Type u))
                p.2 :
              (↑Z : Type u)) }) :
    Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (pullbackFst f g) :
        (a :
            (↑(of
                  { p : (↑X : Type u) × (↑Y : Type u) //
                    (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                      (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) :
              Type u)) →
          (↑X : Type u))
      x =
    (↑x : (↑X : Type u) × (↑Y : Type u)).1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous.{u, u} (X :=
    { p : (↑X : Type u) × (↑Y : Type u) //
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
              (a : (↑X : Type u)) → (↑Z : Type u))
            p.1 :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
              (a : (↑Y : Type u)) → (↑Z : Type u))
            p.2 :
          (↑Z : Type u)) })
    (Prod.snd ∘
      Subtype.val (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
        Eq (α := (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                (a : (↑X : Type u)) → (↑Z : Type u))
              p.1 :
            (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                (a : (↑Y : Type u)) → (↑Z : Type u))
              p.2 :
            (↑Z : Type u))))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x :
  (↑(of
        { p : (↑X : Type u) × (↑Y : Type u) //
          Eq (α := (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                  (a : (↑X : Type u)) → (↑Z : Type u))
                p.1 :
              (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                  (a : (↑Y : Type u)) → (↑Z : Type u))
                p.2 :
              (↑Z : Type u)) }) :
    Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (pullbackSnd f g) :
        (a :
            (↑(of
                  { p : (↑X : Type u) × (↑Y : Type u) //
                    (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                      (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) :
              Type u)) →
          (↑Y : Type u))
      x =
    (↑x : (↑X : Type u) × (↑Y : Type u)).2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
x : (↑S.1 : Type u)
⊢ Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) S.fst :
                  (a : (↑S.pt : Type u)) → (↑X : Type u))
                x,
              (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    S.snd :
                  (a : (↑S.pt : Type u)) → (↑Y : Type u))
                x).1 :
          (↑X : Type u)) :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) S.fst :
                  (a : (↑S.pt : Type u)) → (↑X : Type u))
                x,
              (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    S.snd :
                  (a : (↑S.pt : Type u)) → (↑Y : Type u))
                x).2 :
          (↑Y : Type u)) :
      (↑Z : Type u))

Tactic:
simpa using ConcreteCategory.congr_hom S.condition x

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ Continuous (Y :=
    { p : (↑X : Type u) × (↑Y : Type u) //
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
              (a : (↑X : Type u)) → (↑Z : Type u))
            p.1 :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
              (a : (↑Y : Type u)) → (↑Z : Type u))
            p.2 :
          (↑Z : Type u)) })
    fun (x : (↑S.1 : Type u)) ↦
    Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
              (a : (↑X : Type u)) → (↑Z : Type u))
            p.1 :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
              (a : (↑Y : Type u)) → (↑Z : Type u))
            p.2 :
          (↑Z : Type u)))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) S.fst :
            (a : (↑S.pt : Type u)) → (↑X : Type u))
          x,
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) S.snd :
            (a : (↑S.pt : Type u)) → (↑Y : Type u))
          x)
      ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ S.pt ⟶ (pullbackCone f g).pt

Tactic:
exact ofHom
          { toFun := fun x =>
              ⟨⟨S.fst x, S.snd x⟩, by simpa using ConcreteCategory.congr_hom S.condition x⟩
            continuous_toFun := by fun_prop }

Premises used: ContinuousMap.mk, TopCat.ofHom