awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (↑(pullback f g) : 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 : (↑X : Type u)) → (↑S : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f g) (pullback.fst f g) :
              (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
            x :
          (↑X : Type u)) :
      (↑S : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑S : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f g) (pullback.snd f g) :
              (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
            x :
          (↑Y : Type u)) :
      (↑S : Type u))

Tactic:
CategoryTheory.congr_fun pullback.condition x

Premises used: CategoryTheory.congr_fun, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (↑(pullback f g) : 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 : (↑X : Type u)) → (↑S : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f g) (pullback.fst f g) :
              (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
            x :
          (↑X : Type u)) :
      (↑S : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑S : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f g) (pullback.snd f g) :
              (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
            x :
          (↑Y : Type u)) :
      (↑S : Type u))

Tactic:
exact CategoryTheory.congr_fun pullback.condition x

Premises used: CategoryTheory.congr_fun, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (↑Y : Type u)
x : (↑X : Type u)
eq :
  Eq (α := (↑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))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑S : Type u))
        y :
      (↑S : Type u))
h :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.snd f g) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackIsoProdSubtype f g).inv :
            (a :
                (↑(of
                      { p : (↑X : Type u) × (↑Y : Type u) //
                        (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑S : Type u)) p.1 =
                          (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑S : Type u)) p.2 }) :
                  Type u)) →
              (↑(pullback f g) : Type u))
          (Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : 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 : (↑X : Type u)) → (↑S : Type u))
                  p.1 :
                (↑S : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑S : Type u))
                  p.2 :
                (↑S : Type u)))
            (x, y) eq) :
        (↑(pullback f g) : Type u)) =
    y
⊢ Membership.mem (γ := Set (↑Y : Type u))
    (Set.range (ι := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)))
    y

Tactic:
use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Prod.mk, Subtype.mk, TopCat.pullbackIsoProdSubtype, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (↑Y : Type u)
x : (↑X : Type u)
eq :
  Eq (α := (↑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))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑S : Type u))
        y :
      (↑S : Type u))
h h₁ :
  (↑(Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : 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 : (↑X : Type u)) → (↑S : Type u))
                  p.1 :
                (↑S : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑S : Type u))
                  p.2 :
                (↑S : Type u)))
            (x, y) eq) :
        (↑X : Type u) × (↑Y : Type u)).2 =
    y
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.snd f g) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackIsoProdSubtype f g).inv :
            (a :
                (↑(of
                      { p : (↑X : Type u) × (↑Y : Type u) //
                        (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑S : Type u)) p.1 =
                          (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑S : Type u)) p.2 }) :
                  Type u)) →
              (↑(pullback f g) : Type u))
          (Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : 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 : (↑X : Type u)) → (↑S : Type u))
                  p.1 :
                (↑S : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑S : Type u))
                  p.2 :
                (↑S : Type u)))
            (x, y) eq) :
        (↑(pullback f g) : Type u)) =
    y

Tactic:
rw [pullbackIsoProdSubtype_inv_snd_apply]

Premises used: TopCat.pullbackIsoProdSubtype_inv_snd_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
H₁ :
  IsEmbedding (X := (↑W : Type u)) (Y := (↑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))
H₂ :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(pullback g₁ g₂) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
      (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u))

Tactic:
.of_comp (ContinuousMap.continuous_toFun _)
    (show Continuous (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂)) from
        ContinuousMap.continuous_toFun _)
      ?_

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pullback.snd, ContinuousMap.continuous_toFun, CategoryTheory.Limits.pullback.fst, Topology.IsEmbedding.of_comp, CategoryTheory.Limits.prod.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
H₁ :
  IsEmbedding (X := (↑W : Type u)) (Y := (↑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))
H₂ :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
refine :
  IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(Y ⨯ Z) : Type u))
    (Function.comp (β := (↑(pullback g₁ g₂) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (Y := Y ⨯ Z) (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂))) :
        (a : (↑(pullback g₁ g₂) : 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₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
        (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u)))
⊢ IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(pullback g₁ g₂) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
      (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u))

Tactic:
refine .of_comp (ContinuousMap.continuous_toFun _)
    (show Continuous (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂)) from
        ContinuousMap.continuous_toFun _)
      ?_
-- 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
H₁ :
  IsEmbedding (X := (↑W : Type u)) (Y := (↑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))
H₂ :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
this :
  IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(Y ⨯ Z) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f₁ f₂) (Y := Y ⨯ Z)
          (CategoryStruct.comp (Y := W ⨯ X) (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂)) (prod.map i₁ i₂))) :
      (a : (↑(pullback f₁ f₂) : Type u)) → (↑(Y ⨯ Z) : Type u))
⊢ IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(Y ⨯ Z) : Type u))
    (Function.comp (β := (↑(pullback g₁ g₂) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (Y := Y ⨯ Z) (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂))) :
        (a : (↑(pullback g₁ g₂) : 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₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
        (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u)))

Tactic:
simpa [← coe_comp] using this

Premises used: TopCat.coe_comp
-- 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
H₁ :
  Topology.IsEmbedding (X := (↑W : Type u)) (Y := (↑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))
H₂ :
  Topology.IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
IsEmbedding :
  Topology.IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(Y ⨯ Z) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f₁ f₂) (Y := Y ⨯ Z)
          (CategoryStruct.comp (Y := W ⨯ X) (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂)) (prod.map i₁ i₂))) :
      (a : (↑(pullback f₁ f₂) : Type u)) → (↑(Y ⨯ Z) : Type u))
⊢ Topology.IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(Y ⨯ Z) : Type u))
    (Function.comp (β := (↑(pullback g₁ g₂) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (Y := Y ⨯ Z) (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂))) :
        (a : (↑(pullback g₁ g₂) : 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₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
        (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u)))

Tactic:
suffices
    IsEmbedding (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ Limits.prod.map i₁ i₂) by
    simpa [← coe_comp] using this
-- 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
H₁ :
  IsEmbedding (X := (↑W : Type u)) (Y := (↑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))
H₂ :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(Y ⨯ Z) : Type u))
    (Function.comp (β := (↑(W ⨯ X) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            W ⨯ X) (Y := Y ⨯ Z) (prod.map i₁ i₂)) :
        (a : (↑(W ⨯ X) : 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₁ f₂) (Y := W ⨯ X) (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂))) :
        (a : (↑(pullback f₁ f₂) : Type u)) → (↑(W ⨯ X) : Type u)))

Tactic:
(isEmbedding_prodMap H₁ H₂).comp (isEmbedding_pullback_to_prod _ _)

Premises used: Topology.IsEmbedding.comp, TopCat.isEmbedding_pullback_to_prod, TopCat.isEmbedding_prodMap
-- 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
H₁ :
  IsEmbedding (X := (↑W : Type u)) (Y := (↑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))
H₂ :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(Y ⨯ Z) : Type u))
    (Function.comp (β := (↑(W ⨯ X) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            W ⨯ X) (Y := Y ⨯ Z) (prod.map i₁ i₂)) :
        (a : (↑(W ⨯ X) : 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₁ f₂) (Y := W ⨯ X) (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂))) :
        (a : (↑(pullback f₁ f₂) : Type u)) → (↑(W ⨯ X) : Type u)))

Tactic:
exact (isEmbedding_prodMap H₁ H₂).comp (isEmbedding_pullback_to_prod _ _)

Premises used: Topology.IsEmbedding.comp, TopCat.isEmbedding_pullback_to_prod, TopCat.isEmbedding_prodMap
-- 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
H₁ :
  IsOpenEmbedding (X := (↑W : Type u)) (Y := (↑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))
H₂ :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑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))
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
toIsEmbedding :
  IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(pullback g₁ g₂) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
      (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u))
isOpen_range :
  IsOpen (X := (↑(pullback g₁ g₂) : Type u))
    (Set.range (ι := (↑(pullback f₁ f₂) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
        (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u)))
⊢ IsOpenEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(pullback g₁ g₂) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
      (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u))

Tactic:
constructor
-- 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
H₁ :
  IsOpenEmbedding (X := (↑W : Type u)) (Y := (↑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))
H₂ :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑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))
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsEmbedding (X := (↑(pullback f₁ f₂) : Type u)) (Y := (↑(pullback g₁ g₂) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
      (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u))

Tactic:
apply
      pullback_map_isEmbedding f₁ f₂ g₁ g₂ H₁.isEmbedding H₂.isEmbedding i₃ eq₁ eq₂

Premises used: Topology.IsOpenEmbedding.isEmbedding, TopCat.pullback_map_isEmbedding
-- 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
H₁ :
  IsOpenEmbedding (X := (↑W : Type u)) (Y := (↑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))
H₂ :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑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))
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
isOpen_range :
  IsOpen (X := (↑(pullback g₁ g₂) : Type u))
    (Set.preimage (β := (↑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))
        (Set.range (ι := (↑W : 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))) ∩
      Set.preimage (β := (↑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))
        (Set.range (ι := (↑X : 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))))
⊢ IsOpen (X := (↑(pullback g₁ g₂) : Type u))
    (Set.range (ι := (↑(pullback f₁ f₂) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
        (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u)))

Tactic:
rw [range_pullback_map]

Premises used: TopCat.range_pullback_map