-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Limits (goal)
Goal:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi :
  IsOpenEmbedding (X :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361))
      X)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361),
            (↑(x2.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) :
              Type ?u.9361)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361))
          f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
              (↑X.toTop : Type ?u.9361))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
            (↑X.toTop : Type ?u.9361))
          Z)
⊢ HasExplicitPullbacksOfInclusions.{u} fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)
have hP' : ∀ ⦃X Y B : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)⦄ (f : X ⟶ B) (g : Y ⟶ B),
  IsOpenEmbedding (X :=
      (fun (X : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
          (↑(X.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u))
        X)
      (Y :=
      (fun (X : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
          (↑(X.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u))
        B)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
            C((↑(x1.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u),
              (↑(x2.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
            (↑(X.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u)) f) :
        (a : (fun (X : CompHausLike fun (Y : TopCat) ↦ ExtremallyDisconnected (↑Y : Type u)) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (Y : TopCat) ↦ ExtremallyDisconnected (↑Y : Type u)) ↦ (↑X.toTop : Type u)) B) →
    HasExplicitPullback (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) f g
Tactic: apply CompHausLike.hasPullbacksOfInclusions