-- 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_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)))
⊢ IsOpen (closure U)
have 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))
Tactic: rw [← (closure U).preimage_image_eq Subtype.coe_injective,
      ← h.1.isClosedEmbedding_subtypeVal.closure_image_eq U]