awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))))
isOpen_range₁ :
  IsOpen (X := (↑(pullback g₁ g₂) : 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.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))))

Tactic:
apply IsOpen.inter

Premises used: IsOpen.inter
-- 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 :
  Continuous (X := (↑(pullback g₁ g₂) : Type u)) (Y := (↑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))
isOpen_range₁ :
  IsOpen (X := (↑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)))
⊢ 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))))

Tactic:
apply Continuous.isOpen_preimage

Premises used: Continuous.isOpen_preimage
-- 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 :
  Continuous (X := (↑(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 g₁ g₂) (pullback.snd g₁ g₂)) :
      (a : (↑(pullback g₁ g₂) : Type u)) → (↑Z : Type u))
isOpen_range₁ :
  IsOpen (X := (↑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.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))))

Tactic:
apply Continuous.isOpen_preimage

Premises used: Continuous.isOpen_preimage
-- 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₂
⊢ Continuous (X := (↑(pullback g₁ g₂) : Type u)) (Y := (↑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))

Tactic:
apply ContinuousMap.continuous_toFun

Premises used: 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₁ :
  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 (X := (↑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)))

Tactic:
H₁.isOpen_range

Premises used: Topology.IsOpenEmbedding.isOpen_range
-- 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 (X := (↑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)))

Tactic:
exact H₁.isOpen_range

Premises used: Topology.IsOpenEmbedding.isOpen_range
-- 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₂
⊢ Continuous (X := (↑(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 g₁ g₂) (pullback.snd g₁ g₂)) :
      (a : (↑(pullback g₁ g₂) : Type u)) → (↑Z : Type u))

Tactic:
apply ContinuousMap.continuous_toFun

Premises used: 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₁ :
  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 (X := (↑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)))

Tactic:
H₂.isOpen_range

Premises used: Topology.IsOpenEmbedding.isOpen_range
-- 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 (X := (↑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)))

Tactic:
exact H₂.isOpen_range

Premises used: Topology.IsOpenEmbedding.isOpen_range
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
H :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
g : Y ⟶ S
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
H :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
g : Y ⟶ S
h :
  Eq (α := (↑(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) (X :=
          pullback f g) (pullback.snd f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
    (Function.comp (β := (↑(pullback (𝟙 S) g) : Type u))
      (⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) : (a : (↑(pullback (𝟙 S) g) : Type u)) → (↑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 := pullback (𝟙 S) g) (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯)) :
        (a : (↑(pullback f g) : Type u)) → (↑(pullback (𝟙 S) g) : Type u)))
⊢ IsEmbedding (X := (↑(pullback f g) : Type u)) (Y := (↑Y : 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))

Tactic:
convert!
    (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isEmbedding.comp
      (pullback_map_isEmbedding (i₂ := 𝟙 Y) f g (𝟙 S) g H (homeoOfIso (Iso.refl _)).isEmbedding
        (𝟙 _) rfl (by simp))

Premises used: Homeomorph.isEmbedding, CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.id, CategoryTheory.Iso.refl, Topology.IsEmbedding.comp, TopCat.homeoOfIso, TopCat.pullback_map_isEmbedding, rfl, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
H :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
g : Y ⟶ S
⊢ Eq (α := (↑(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) (X :=
          pullback f g) (pullback.snd f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
    (Function.comp (β := (↑(pullback (𝟙 S) g) : Type u))
      (⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) : (a : (↑(pullback (𝟙 S) g) : Type u)) → (↑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 := pullback (𝟙 S) g) (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯)) :
        (a : (↑(pullback f g) : Type u)) → (↑(pullback (𝟙 S) g) : Type u)))

Tactic:
simp [homeoOfIso, ← coe_comp]

Premises used: TopCat.homeoOfIso, TopCat.coe_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
h :
  Eq (α := (↑(pullback f g) : Type u) → (↑X : 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))
    (Function.comp (β := (↑(pullback f (𝟙 S)) : Type u))
      (⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) : (a : (↑(pullback f (𝟙 S)) : Type u)) → (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (Y := pullback f (𝟙 S)) (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯)) :
        (a : (↑(pullback f g) : Type u)) → (↑(pullback f (𝟙 S)) : Type u)))
⊢ IsEmbedding (X := (↑(pullback f g) : Type u)) (Y := (↑X : 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))

Tactic:
convert!
    (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isEmbedding.comp
      (pullback_map_isEmbedding (i₁ := 𝟙 X) f g f (𝟙 _) (homeoOfIso (Iso.refl _)).isEmbedding H
        (𝟙 _) rfl (by simp))

Premises used: Homeomorph.isEmbedding, CategoryTheory.CategoryStruct.id, CategoryTheory.Iso.refl, Topology.IsEmbedding.comp, TopCat.homeoOfIso, CategoryTheory.Limits.pullback.fst, TopCat.pullback_map_isEmbedding, rfl, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
⊢ Eq (α := (↑(pullback f g) : Type u) → (↑X : 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))
    (Function.comp (β := (↑(pullback f (𝟙 S)) : Type u))
      (⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) : (a : (↑(pullback f (𝟙 S)) : Type u)) → (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (Y := pullback f (𝟙 S)) (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯)) :
        (a : (↑(pullback f g) : Type u)) → (↑(pullback f (𝟙 S)) : Type u)))

Tactic:
simp [homeoOfIso, ← coe_comp]

Premises used: TopCat.homeoOfIso, TopCat.coe_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
H₂ :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
⊢ IsEmbedding (X := (↑(pullback f g) : Type u)) (Y := (↑S : Type u))
    (Function.comp (β := (↑Y : 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)))

Tactic:
H₂.comp (snd_isEmbedding_of_left H₁ g)

Premises used: Topology.IsEmbedding.comp, TopCat.snd_isEmbedding_of_left
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
H₂ :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
h :
  (↑((cospan f g).obj WalkingCospan.one) : Type u) = (↑S : Type u) →
    Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)) :
        (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
      (Function.comp (β := (↑Y : 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)))
⊢ IsEmbedding (X := (↑(limit (cospan f g)) : Type u)) (Y := (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))

Tactic:
convert! H₂.comp (snd_isEmbedding_of_left H₁ g)

Premises used: Topology.IsEmbedding.comp, TopCat.snd_isEmbedding_of_left
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑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))
H₂ :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
e_2 : (↑((cospan f g).obj WalkingCospan.one) : Type u) = (↑S : Type u)
h :
  Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : 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 ≫ g)) :
      (a : (↑(pullback f g) : Type u)) → (↑S : Type u))
⊢ Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (Function.comp (β := (↑Y : 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)))

Tactic:
rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr]

Premises used: CategoryTheory.Limits.WalkingCospan.Hom.inr, TopCat.coe_comp, CategoryTheory.Limits.limit.w