awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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))
⊢ 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))
have 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)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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 := (↑(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)))
have 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))))
Tactic: rw [range_pullback_map]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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 := (↑(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))))
have 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))))
Tactic: apply IsOpen.inter
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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 (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))))
have 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))))
Tactic: apply IsOpen.inter
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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 := (↑(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))))
have 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))
Tactic: apply Continuous.isOpen_preimage
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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 (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))))
have 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)))
Tactic: apply Continuous.isOpen_preimage
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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 := (↑(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))))
have 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))
Tactic: apply Continuous.isOpen_preimage
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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 (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))))
have 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)))
Tactic: apply Continuous.isOpen_preimage
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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
⊢ 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))
have 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) sorry sorry)) :
      (a : (↑(pullback f g) : Type u)) → (↑(pullback (𝟙 S) g) : 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))
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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))
⊢ 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))
have 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) sorry sorry)) :
      (a : (↑(pullback f g) : Type u)) → (↑(pullback f (𝟙 S)) : 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))
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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 := (↑(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))
have 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)))
Tactic: convert! H₂.comp (snd_isEmbedding_of_left H₁ g)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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)
⊢ 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)))
have 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))
Tactic: rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr]