-- 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_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
      X)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
            (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)) f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) Z)
U :
  Set
    (↑(Set.preimage (β :=
          (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
            Z)
          (⇑(ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
                  (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                    Type u_1)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
                i) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                    (↑X.toTop : Type u_1))
                  Y) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
                Z)
          (Set.range (ι :=
            (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
              X)
            (⇑(ConcreteCategory.hom (FC :=
                  fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                      Type u_1),
                    (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                      Type u_1)))
                  (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
                  f) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                      (↑X.toTop : Type u_1))
                    X) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                    (↑X.toTop : Type u_1))
                  Z))) :
      Type u_1)
hU : IsOpen U
h :
  IsClopen (X :=
    (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
      Y)
    (Set.preimage (β :=
      (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
        Z)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
              (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)) i) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
              Y) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) Z)
      (Set.range (ι :=
        (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
          X)
        (⇑(ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
                (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)) f) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
                X) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
              Z)))
rw :
  IsOpen (X :=
    (↑(Set.preimage (β :=
          (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
            Z)
          (⇑(ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
                  (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                    Type u_1)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
                i) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                    (↑X.toTop : Type u_1))
                  Y) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
                Z)
          (Set.range (ι :=
            (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
              X)
            (⇑(ConcreteCategory.hom (FC :=
                  fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                      Type u_1),
                    (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                      Type u_1)))
                  (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
                  f) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                      (↑X.toTop : Type u_1))
                    X) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                    (↑X.toTop : Type u_1))
                  Z))) :
      Type u_1))
    ((fun
          (a :
            { x :
              (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
                Y //
              Membership.mem (γ :=
                Set
                  ((fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                        Type u_1))
                    Y))
                (Set.preimage (β :=
                  (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                        Type u_1))
                    Z)
                  (⇑(ConcreteCategory.hom (FC :=
                        fun
                          (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                        C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                            Type u_1),
                          (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                            Type u_1)))
                        (CC :=
                        fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                          Type u_1))
                        i) :
                    (a :
                        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                            (↑X.toTop : Type u_1))
                          Y) →
                      (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                          (↑X.toTop : Type u_1))
                        Z)
                  (Set.range (ι :=
                    (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                          Type u_1))
                      X)
                    (⇑(ConcreteCategory.hom (FC :=
                          fun
                            (x1 x2 :
                              CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                              Type u_1),
                            (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                              Type u_1)))
                          (CC :=
                          fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                            Type u_1))
                          f) :
                      (a :
                          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                              (↑X.toTop : Type u_1))
                            X) →
                        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                            (↑X.toTop : Type u_1))
                          Z)))
                x }) ↦
        (↑a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
            Y)) ⁻¹'
      closure
        (Subtype.val (p :=
            fun
              (x :
                (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                      Type u_1))
                  Y) ↦
            Membership.mem (γ :=
              Set
                ((fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                      Type u_1))
                  Y))
              (Set.preimage (β :=
                (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                      Type u_1))
                  Z)
                (⇑(ConcreteCategory.hom (FC :=
                      fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                      C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                          Type u_1),
                        (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                          Type u_1)))
                      (CC :=
                      fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                        Type u_1))
                      i) :
                  (a :
                      (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                          (↑X.toTop : Type u_1))
                        Y) →
                    (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                        (↑X.toTop : Type u_1))
                      Z)
                (Set.range (ι :=
                  (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                        Type u_1))
                    X)
                  (⇑(ConcreteCategory.hom (FC :=
                        fun
                          (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                        C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                            Type u_1),
                          (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                            Type u_1)))
                        (CC :=
                        fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
                        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) :
                          Type u_1))
                        f) :
                    (a :
                        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                            (↑X.toTop : Type u_1))
                          X) →
                      (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦
                          (↑X.toTop : Type u_1))
                        Z)))
              x) ''
          U))
⊢ IsOpen (closure U)

Tactic:
rw [← (closure U).preimage_image_eq Subtype.coe_injective,
      ← h.1.isClosedEmbedding_subtypeVal.closure_image_eq U]

Premises used: Subtype.coe_injective, closure, And.left, Topology.IsClosedEmbedding.closure_image_eq, Set.preimage_image_eq, IsClosed.isClosedEmbedding_subtypeVal