-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : (↑(pullback f g) : Type u) ≃ₜ
  (↑(of
        { p : (↑X : Type u) × (↑Y : Type u) //
          Eq (α := (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                  (a : (↑X : Type u)) → (↑Z : Type u))
                p.1 :
              (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                  (a : (↑Y : Type u)) → (↑Z : Type u))
                p.2 :
              (↑Z : Type u)) }) :
    Type u) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
refine :
  Eq (α := TopologicalSpace (↑(pullback f g) : Type u))
    (induced (Y :=
      (↑(of
            { p : (↑X : Type u) × (↑Y : Type u) //
              Eq (α := (↑Z : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        f :
                      (a : (↑X : Type u)) → (↑Z : Type u))
                    p.1 :
                  (↑Z : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        g :
                      (a : (↑Y : Type u)) → (↑Z : Type u))
                    p.2 :
                  (↑Z : Type u)) }) :
        Type u))
      (⇑homeo :
        (a : (↑(pullback f g) : Type u)) →
          (↑(of
                { p : (↑X : Type u) × (↑Y : Type u) //
                  (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                    (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) :
            Type u))
      (of
          { p : (↑X : Type u) × (↑Y : Type u) //
            Eq (α := (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑X : Type u)) → (↑Z : Type u))
                  p.1 :
                (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑Z : Type u))
                  p.2 :
                (↑Z : Type u)) }).str)
    (induced
        (⇑(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.str ⊓
      induced
        (⇑(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.str)
⊢ Eq (α := TopologicalSpace (↑(pullback f g) : Type u)) (pullback f g).str
    (induced
        (⇑(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.str ⊓
      induced
        (⇑(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.str)

Tactic:
refine homeo.isInducing.eq_induced.trans ?_

Premises used: Homeomorph.isInducing, Topology.IsInducing.eq_induced, Eq.trans