-- Module: Mathlib.Topology.Category.Stonean.Limits
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)
X_1 : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)
hP' :
  ∀ ⦃Y B : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)⦄ (f : X_1 ⟶ 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_1)
        (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_1) →
            (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
⊢ ∀ ⦃Y B : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)⦄ (f : X_1 ⟶ 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_1)
        (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_1) →
            (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:
_