-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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)
⊢ 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))
      (induced
        (Subtype.val (p := fun (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))))
        (induced Prod.fst X.str ⊓ induced Prod.snd Y.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)
have simp : Eq (α := TopologicalSpace (↑(pullback f g) : Type u))
  (induced
      (Function.comp (β :=
        { 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)) })
        (Prod.fst ∘
          Subtype.val (p := fun (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))))
        (⇑homeo :
          (a : (↑(pullback f g) : Type u)) →
            { 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 }))
      X.str ⊓
    induced
      (Function.comp (β :=
        { 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)) })
        (Prod.snd ∘
          Subtype.val (p := fun (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))))
        (⇑homeo :
          (a : (↑(pullback f g) : Type u)) →
            { 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 }))
      Y.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: simp only [induced_compose, induced_inf]