-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ
⊢ {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) g.base) :
            (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ⁻¹'
          (↑{
                carrier :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                          TopCat.carrier) f.base) :
                      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ''
                    (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
                is_open' := ⋯ : Opens (↑(↑Z : TopCat) : Type u_1) } :
            Set (↑(↑Z : TopCat) : Type u_1)),
      is_open' := ⋯ : Opens (↑(↑Y : TopCat) : Type u_1) } =
    {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) (X := pullback f.base g.base) (pullback.snd f.base g.base)) :
            (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
          (↑{
                carrier :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                          TopCat.carrier) (X := (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat))
                          (pullback.fst f.base g.base)) :
                      (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑X : TopCat) : Type u_1)) ⁻¹'
                    (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
                is_open' := ⋯ : Opens (↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1) } :
            Set (↑(pullback f.base g.base) : Type u_1)),
      is_open' := ⋯ }
have a : {
    carrier :=
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) g.base) :
          (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ⁻¹'
        (↑{
              carrier :=
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        TopCat.carrier) f.base) :
                    (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ''
                  (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
              is_open' := sorry : Opens (↑(↑Z : TopCat) : Type u_1) } :
          Set (↑(↑Z : TopCat) : Type u_1)),
    is_open' := sorry : Opens (↑(↑Y : TopCat) : Type u_1) } ≤
  {
    carrier :=
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X := pullback f.base g.base) (pullback.snd f.base g.base)) :
          (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
        (↑{
              carrier :=
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        TopCat.carrier) (X := (↑(Y.restrict (U := pullback f.base g.base) sorry) : TopCat))
                        (pullback.fst f.base g.base)) :
                    (a : (↑(↑(Y.restrict sorry) : TopCat) : Type u_1)) → (↑(↑X : TopCat) : Type u_1)) ⁻¹'
                  (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
              is_open' := sorry : Opens (↑(↑(Y.restrict (U := pullback f.base g.base) sorry) : TopCat) : Type u_1) } :
          Set (↑(pullback f.base g.base) : Type u_1)),
    is_open' := sorry }
Tactic: apply LE.le.antisymm