-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
refine_1 :
  ∀ (x : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)),
    IsLocalHom (R :=
      (↑((pullbackConeOfLeft f g).pt.presheaf.stalk
            (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) (X := (↑s.pt.toPresheafedSpace : TopCat)) (Y :=
                    (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) :
                      (↑s.pt.toPresheafedSpace : TopCat) ⟶ (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat)) :
                  C((↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1),
                    (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))) :
                (a : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)) →
                  (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1))
      (S := (↑(s.pt.presheaf.stalk x) : Type u_1)) (F :=
      (↑((pullbackConeOfLeft f g).pt.presheaf.stalk
              (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      TopCat.carrier) (X := (↑s.pt.toPresheafedSpace : TopCat)) (Y :=
                      (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat))
                      (PresheafedSpace.Hom.base
                          (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                            (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) :
                        (↑s.pt.toPresheafedSpace : TopCat) ⟶
                          (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat)) :
                    C((↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1),
                      (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))) :
                  (a : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)) →
                    (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))
                x)) :
          Type u_1) →+*
        (↑(s.pt.presheaf.stalk x) : Type u_1))
      (CommRingCat.Hom.hom
        (PresheafedSpace.Hom.stalkMap
          (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
            (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
          x))
refine_2 :
  ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
    m ≫ (pullbackConeOfLeft f g).fst = s.fst →
      m ≫ (pullbackConeOfLeft f g).snd = s.snd →
        m =
          {
            toHom :=
              PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
            prop := ⋯ }
⊢ { l : s.pt ⟶ (pullbackConeOfLeft f g).pt //
    l ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
      l ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
          m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = l }

Tactic:
refine ⟨LocallyRingedSpace.Hom.mk (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift
        f.1 g.1 (PullbackCone.mk _ _ (congr_arg LocallyRingedSpace.Hom.toHom s.condition))) ?_,
      LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst f.1 g.1 _),
      LocallyRingedSpace.Hom.ext'
          (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 _), ?_⟩