-- 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₂
h :
  ∀ (x : (↑(pullback g₁ g₂) : Type u)),
    Membership.mem (γ := Set (↑(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)))
        x ↔
      Membership.mem (γ := Set (↑(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))))
        x
⊢ Eq (α := Set (↑(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)))
    (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:
ext