awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : (↑(pullback f g) : Type u)
⊢ Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g)
            (CategoryStruct.comp (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) (prod.fst ≫ f)) :
          (a : (↑(pullback f g) : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g)
            (CategoryStruct.comp (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) (prod.snd ≫ g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
a :
  (↑((fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
              (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
                  ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) ⋯ :
                { p : X × Y // f p.1 = g p.2 }))
            ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
                (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯ :
                  { x : X // x ∈ f ⁻¹' Set.range g }))
              x)) :
        X × Y).1 =
    (↑x : X × Y).1
a₁ :
  (↑((fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
              (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
                  ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) ⋯ :
                { p : X × Y // f p.1 = g p.2 }))
            ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
                (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯ :
                  { x : X // x ∈ f ⁻¹' Set.range g }))
              x)) :
        X × Y).2 =
    (↑x : X × Y).2
⊢ (fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
        (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
            ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) ⋯ :
          { p : X × Y // f p.1 = g p.2 }))
      ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
          (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯ : { x : X // x ∈ f ⁻¹' Set.range g }))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
⊢ (↑((fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
              (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
                  ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) ⋯ :
                { p : X × Y // f p.1 = g p.2 }))
            ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
                (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯ :
                  { x : X // x ∈ f ⁻¹' Set.range g }))
              x)) :
        X × Y).1 =
    (↑x : X × Y).1

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
a : Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) ⋯ = (↑x : X × Y).2
⊢ (↑((fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
              (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
                  ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) ⋯ :
                { p : X × Y // f p.1 = g p.2 }))
            ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
                (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯ :
                  { x : X // x ∈ f ⁻¹' Set.range g }))
              x)) :
        X × Y).2 =
    (↑x : X × Y).2

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
a : g (Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) ⋯) = g (↑x : X × Y).2
⊢ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) ⋯ = (↑x : X × Y).2

Tactic:
apply hg.injective

Premises used: Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
⊢ f (↑x : X × Y).1 = g (↑x : X × Y).2

Tactic:
x.prop

Premises used: Subtype.prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
h : g (Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) ⋯) = f (↑x : X × Y).1
⊢ g (Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) ⋯) = g (↑x : X × Y).2

Tactic:
convert! x.prop

Premises used: Subtype.prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
⊢ g (Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) ⋯) = f (↑x : X × Y).1

Tactic:
Exists.choose_spec (p := fun y ↦ g y = f (↑x : X × Y).1) _

Premises used: Exists.choose_spec
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
⊢ g (Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) ⋯) = f (↑x : X × Y).1

Tactic:
exact Exists.choose_spec (p := fun y ↦ g y = f (↑x : X × Y).1) _

Premises used: Exists.choose_spec
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
h :
  Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
    ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
    Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2) ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)
      ⋯

Tactic:
apply Continuous.subtype_mk

Premises used: Continuous.subtype_mk
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
    ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)

Tactic:
continuous_subtype_val.prodMk <| hg.isInducing.continuous_iff.mpr ?_

Premises used: Iff.mpr, continuous_subtype_val, Topology.IsInducing.continuous_iff, Topology.IsEmbedding.isInducing, Continuous.prodMk
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
h :
  Continuous[instTopologicalSpaceSubtype, inst_3]
    (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
    ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)

Tactic:
refine continuous_subtype_val.prodMk <| hg.isInducing.continuous_iff.mpr ?_

Premises used: Iff.mpr, continuous_subtype_val, Topology.IsInducing.continuous_iff, Topology.IsEmbedding.isInducing, Continuous.prodMk
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
⊢ Continuous[instTopologicalSpaceSubtype, inst_3] (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g))

Tactic:
hf.comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
h :
  Eq (α := { x : X // x ∈ f ⁻¹' Set.range g } → Z)
    (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)
    (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g))
⊢ Continuous[instTopologicalSpaceSubtype, inst_3]
    (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)

Tactic:
convert! hf.comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
h :
  ∀ (x : { x : X // x ∈ f ⁻¹' Set.range g }),
    (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) x =
      (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g)) x
⊢ Eq (α := { x : X // x ∈ f ⁻¹' Set.range g } → Z)
    (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)
    (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g))

Tactic:
ext x
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { x : X // x ∈ f ⁻¹' Set.range g }
⊢ (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) x =
    (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g)) x

Tactic:
Exists.choose_spec x.2

Premises used: Exists.choose_spec, Subtype.property
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { x : X // x ∈ f ⁻¹' Set.range g }
⊢ (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) x =
    (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g)) x

Tactic:
exact Exists.choose_spec x.2

Premises used: Exists.choose_spec, Subtype.property
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := TopologicalSpace (↑(pullback f g) : Type u)) (pullback f g).str
    (induced (Y := (↑(X ⨯ Y) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
        (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u))
      (X ⨯ Y).str)

Tactic:
simp [prod_topology, pullback_topology, induced_compose, ← coe_comp]

Premises used: TopCat.pullback_topology, TopCat.prod_topology, induced_compose, TopCat.coe_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ IsEmbedding (X := (↑(pullback f g) : Type u)) (Y := (↑(X ⨯ Y) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
      (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u))

Tactic:
⟨isInducing_pullback_to_prod f g, (TopCat.mono_iff_injective _).mp inferInstance⟩

Premises used: TopCat.isInducing_pullback_to_prod, inferInstance, Iff.mp, TopCat.mono_iff_injective, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
y : (↑(pullback f₁ f₂) : Type u)
h :
  (∃ (y_1 : (↑W : Type u)),
      Eq (α := (↑Y : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₁ :
              (a : (↑W : Type u)) → (↑Y : Type u))
            y_1 :
          (↑Y : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ i₁) :
              (a : (↑(pullback f₁ f₂) : Type u)) → (↑Y : Type u))
            y :
          (↑Y : Type u))) ∧
    ∃ (y_1 : (↑X : Type u)),
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₂ :
              (a : (↑X : Type u)) → (↑Z : Type u))
            y_1 :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f₁ f₂) (pullback.snd f₁ f₂ ≫ i₂) :
              (a : (↑(pullback f₁ f₂) : Type u)) → (↑Z : Type u))
            y :
          (↑Z : Type u))
⊢ (∃ (y_1 : (↑W : Type u)),
      Eq (α := (↑Y : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₁ :
              (a : (↑W : Type u)) → (↑Y : Type u))
            y_1 :
          (↑Y : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f₁ f₂)
                (CategoryStruct.comp (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
                  (pullback.fst g₁ g₂)) :
              (a : (↑(pullback f₁ f₂) : Type u)) → (↑Y : Type u))
            y :
          (↑Y : Type u))) ∧
    ∃ (y_1 : (↑X : Type u)),
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₂ :
              (a : (↑X : Type u)) → (↑Z : Type u))
            y_1 :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f₁ f₂)
                (CategoryStruct.comp (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
                  (pullback.snd g₁ g₂)) :
              (a : (↑(pullback f₁ f₂) : Type u)) → (↑Z : Type u))
            y :
          (↑Z : Type u))

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
y : (↑(pullback f₁ f₂) : Type u)
⊢ (∃ (y_1 : (↑W : Type u)),
      Eq (α := (↑Y : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₁ :
              (a : (↑W : Type u)) → (↑Y : Type u))
            y_1 :
          (↑Y : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ i₁) :
              (a : (↑(pullback f₁ f₂) : Type u)) → (↑Y : Type u))
            y :
          (↑Y : Type u))) ∧
    ∃ (y_1 : (↑X : Type u)),
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₂ :
              (a : (↑X : Type u)) → (↑Z : Type u))
            y_1 :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f₁ f₂) (pullback.snd f₁ f₂ ≫ i₂) :
              (a : (↑(pullback f₁ f₂) : Type u)) → (↑Z : Type u))
            y :
          (↑Z : Type u))

Tactic:
⟨exists_apply_eq_apply _ _, exists_apply_eq_apply _ _⟩

Premises used: And.intro, exists_apply_eq_apply
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
y : (↑(pullback f₁ f₂) : Type u)
⊢ (∃ (y_1 : (↑W : Type u)),
      Eq (α := (↑Y : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₁ :
              (a : (↑W : Type u)) → (↑Y : Type u))
            y_1 :
          (↑Y : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ i₁) :
              (a : (↑(pullback f₁ f₂) : Type u)) → (↑Y : Type u))
            y :
          (↑Y : Type u))) ∧
    ∃ (y_1 : (↑X : Type u)),
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₂ :
              (a : (↑X : Type u)) → (↑Z : Type u))
            y_1 :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f₁ f₂) (pullback.snd f₁ f₂ ≫ i₂) :
              (a : (↑(pullback f₁ f₂) : Type u)) → (↑Z : Type u))
            y :
          (↑Z : Type u))

Tactic:
exact ⟨exists_apply_eq_apply _ _, exists_apply_eq_apply _ _⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x : (↑(pullback g₁ g₂) : Type u)
x₁ : (↑W : Type u)
hx₁ :
  Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₁ :
          (a : (↑W : Type u)) → (↑Y : Type u))
        x₁ :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (pullback.fst g₁ g₂) :
          (a : (↑(pullback g₁ g₂) : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
x₂ : (↑X : Type u)
hx₂ :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₂ :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x₂ :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (pullback.snd g₁ g₂) :
          (a : (↑(pullback g₁ g₂) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
a :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₃ :
          (a : (↑S : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₁ :
              (a : (↑W : Type u)) → (↑S : Type u))
            x₁ :
          (↑S : Type u)) :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₃ :
          (a : (↑S : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₂ :
              (a : (↑X : Type u)) → (↑S : Type u))
            x₂ :
          (↑S : Type u)) :
      (↑T : Type u))
⊢ Eq (α := (↑S : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₁ :
          (a : (↑W : Type u)) → (↑S : Type u))
        x₁ :
      (↑S : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₂ :
          (a : (↑X : Type u)) → (↑S : Type u))
        x₂ :
      (↑S : Type u))

Tactic:
apply (TopCat.mono_iff_injective _).mp H₃

Premises used: Iff.mp, TopCat.mono_iff_injective