-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
this_1 : IsIso (X := pullback f g) (pullback.snd f g)
this :
  Eq (α := (↑(pullback f g).toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat))
    (CategoryStruct.comp (Y :=
      pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))
      (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g))
      (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)))
    (PresheafedSpace.Hom.base (Hom.toHom (pullback.fst f g)))
rw :
  Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι :=
      (↑(pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
            ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) :
        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 ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
              ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))
            (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
              ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))) :
        (a :
            (↑(pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
                  ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) :
              Type u_1)) →
          (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.preimage (β := (↑(↑Z.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
      (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))))
rw₁ :
  Function.Surjective (α := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) (β :=
    (↑(pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
          ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) :
      Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
          TopCat.carrier) (Y :=
          pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
            ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))
          (CategoryStruct.comp (Y := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (Hom.toHom (inv (pullback.snd f g))))
            (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g)))) :
      (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) →
        (↑(pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
              ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) :
          Type u_1))
⊢ Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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)
            (CategoryStruct.comp (Y := pullback f g) (inv (pullback.snd f g)) (pullback.fst f g)).base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.preimage (β := (↑(↑Z.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
      (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))))

Tactic:
rw [LocallyRingedSpace.comp_base, ← this, ← Category.assoc, TopCat.coe_comp, Set.range_comp,
      Set.range_eq_univ.mpr, Set.image_univ]

Premises used: Iff.mpr, Set.range_eq_univ, Set.range_comp, CategoryTheory.Category.assoc, Set.image_univ, AlgebraicGeometry.LocallyRingedSpace.comp_base, TopCat.coe_comp