-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
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))ᵒᵖ
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' := ⋯ : 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' := ⋯ }
a₁ :
  {
      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' := ⋯ : 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) 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' := ⋯ }
⊢ {
      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' := ⋯ }

Tactic:
apply LE.le.antisymm

Premises used: LE.le.antisymm