-- 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))ᵒᵖ
x : (↑(↑Y : TopCat) : Type u_1)
w : (↑(↑X : TopCat) : Type u_1)
h₁ : w ∈ (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1))
h₂ :
  Eq (α := (↑(↑Z : TopCat) : Type u_1))
    ((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))
        w :
      (↑(↑Z : TopCat) : Type u_1))
    ((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))
        x :
      (↑(↑Z : TopCat) : Type u_1))
⊢ Membership.mem (α := (↑(pullback f.base g.base) : 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))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (TopCat.pullbackIsoProdSubtype f.base g.base).inv :
            (a :
                (↑(TopCat.of
                      { p : (↑(↑X : TopCat) : Type u_1) × (↑(↑Y : TopCat) : Type u_1) //
                        (ConcreteCategory.hom f.base : (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
                            p.1 =
                          (ConcreteCategory.hom g.base :
                              (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
                            p.2 }) :
                  Type u_1)) →
              (↑(pullback f.base g.base) : Type u_1))
          (Subtype.mk (p := fun (p : (↑(↑X : TopCat) : Type u_1) × (↑(↑Y : TopCat) : Type u_1)) ↦
            Eq (α := (↑(↑Z : TopCat) : Type u_1))
              ((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))
                  p.1 :
                (↑(↑Z : TopCat) : Type u_1))
              ((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))
                  p.2 :
                (↑(↑Z : TopCat) : Type u_1)))
            (w, x) h₂) :
        (↑(pullback f.base g.base) : Type u_1)) ∧
    (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))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) (TopCat.pullbackIsoProdSubtype f.base g.base).inv :
              (a :
                  (↑(TopCat.of
                        { p : (↑(↑X : TopCat) : Type u_1) × (↑(↑Y : TopCat) : Type u_1) //
                          (ConcreteCategory.hom f.base :
                                (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
                              p.1 =
                            (ConcreteCategory.hom g.base :
                                (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
                              p.2 }) :
                    Type u_1)) →
                (↑(pullback f.base g.base) : Type u_1))
            (Subtype.mk (p := fun (p : (↑(↑X : TopCat) : Type u_1) × (↑(↑Y : TopCat) : Type u_1)) ↦
              Eq (α := (↑(↑Z : TopCat) : Type u_1))
                ((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))
                    p.1 :
                  (↑(↑Z : TopCat) : Type u_1))
                ((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))
                    p.2 :
                  (↑(↑Z : TopCat) : Type u_1)))
              (w, x) h₂) :
          (↑(pullback f.base g.base) : Type u_1)) =
      x

Tactic:
simpa [(TopCat.pullbackIsoProdSubtype_inv_fst_apply),
                      (TopCat.pullbackIsoProdSubtype_inv_snd_apply)]

Premises used: TopCat.pullbackIsoProdSubtype_inv_snd_apply, TopCat.pullbackIsoProdSubtype_inv_fst_apply