-- Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean
/-- If `Y ⟶ S` is surjective on stalks, then for every `X ⟶ S`, `X ×ₛ Y` is a subset of
`X × Y` (cartesian product as topological spaces) with the induced topology. -/
lemma isEmbedding_pullback {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) [SurjectiveOnStalks g] :
    IsEmbedding (fun x ↦ ((pullback.fst f g).base x, (pullback.snd f g).base x))

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↑↑(pullback f g).toPresheafedSpace → ↑↑X.toPresheafedSpace × ↑↑Y.toPresheafedSpace :=
  fun x => ((ConcreteCategory.hom (pullback.fst f g).base) x, (ConcreteCategory.hom (pullback.snd f g).base) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY →
        IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(ConcreteCategory.hom (pullback.map f' g' f g iX iY iS e₁ e₂).base))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) → ((Scheme.Cover.pullbackCover 𝒰 f).obj i).OpenCover :=
  fun i => ((Scheme.Cover.pullbackCover 𝒰 f).obj i).affineOpenCover.openCover
𝒲 : (i : (Scheme.Cover.pullbackCover 𝒰 g).J) → ((Scheme.Cover.pullbackCover 𝒰 g).obj i).OpenCover :=
  fun i => ((Scheme.Cover.pullbackCover 𝒰 g).obj i).affineOpenCover.openCover
U : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) × (𝒱 i).J × (𝒲 i).J →
  TopologicalSpace.Opens (↑↑X.toPresheafedSpace × ↑↑Y.toPresheafedSpace) :=
  fun ijk =>
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).map ijk.snd.1 ≫ (Scheme.Cover.pullbackCover 𝒰 f).map ijk.fst) ∧
            P.2 ∈ Scheme.Hom.opensRange ((𝒲 ijk.fst).map ijk.snd.2 ≫ (Scheme.Cover.pullbackCover 𝒰 g).map ijk.fst)},
      is_open' := ⋯ }
this : Set.range L ⊆ ↑(iSup U)
𝓤 : Scheme.Cover (@IsOpenImmersion) (pullback f g) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f g) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i) (pullback.snd f (𝒰.map i)) (pullback.snd g (𝒰.map i))
⊢ IsEmbedding fun x =>
    ((ConcreteCategory.hom (pullback.fst f g).base) x, (ConcreteCategory.hom (pullback.snd f g).base) x)

Tactic:
refine isEmbedding_of_iSup_eq_top_of_preimage_subset_range _ ?_ U this _ (fun i ↦ (𝓤.map i).base)
  (fun i ↦ (𝓤.map i).continuous) ?_ ?_

Result:
case refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↑↑(pullback f g).toPresheafedSpace → ↑↑X.toPresheafedSpace × ↑↑Y.toPresheafedSpace :=
  fun x => ((ConcreteCategory.hom (pullback.fst f g).base) x, (ConcreteCategory.hom (pullback.snd f g).base) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY →
        IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(ConcreteCategory.hom (pullback.map f' g' f g iX iY iS e₁ e₂).base))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) → ((Scheme.Cover.pullbackCover 𝒰 f).obj i).OpenCover :=
  fun i => ((Scheme.Cover.pullbackCover 𝒰 f).obj i).affineOpenCover.openCover
𝒲 : (i : (Scheme.Cover.pullbackCover 𝒰 g).J) → ((Scheme.Cover.pullbackCover 𝒰 g).obj i).OpenCover :=
  fun i => ((Scheme.Cover.pullbackCover 𝒰 g).obj i).affineOpenCover.openCover
U : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) × (𝒱 i).J × (𝒲 i).J →
  TopologicalSpace.Opens (↑↑X.toPresheafedSpace × ↑↑Y.toPresheafedSpace) :=
  fun ijk =>
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).map ijk.snd.1 ≫ (Scheme.Cover.pullbackCover 𝒰 f).map ijk.fst) ∧
            P.2 ∈ Scheme.Hom.opensRange ((𝒲 ijk.fst).map ijk.snd.2 ≫ (Scheme.Cover.pullbackCover 𝒰 g).map ijk.fst)},
      is_open' := ⋯ }
this : Set.range L ⊆ ↑(iSup U)
𝓤 : Scheme.Cover (@IsOpenImmersion) (pullback f g) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f g) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i) (pullback.snd f (𝒰.map i)) (pullback.snd g (𝒰.map i))
⊢ Continuous fun x =>
    ((ConcreteCategory.hom (pullback.fst f g).base) x, (ConcreteCategory.hom (pullback.snd f g).base) x)

case refine_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↑↑(pullback f g).toPresheafedSpace → ↑↑X.toPresheafedSpace × ↑↑Y.toPresheafedSpace :=
  fun x => ((ConcreteCategory.hom (pullback.fst f g).base) x, (ConcreteCategory.hom (pullback.snd f g).base) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY →
        IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(ConcreteCategory.hom (pullback.map f' g' f g iX iY iS e₁ e₂).base))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) → ((Scheme.Cover.pullbackCover 𝒰 f).obj i).OpenCover :=
  fun i => ((Scheme.Cover.pullbackCover 𝒰 f).obj i).affineOpenCover.openCover
𝒲 : (i : (Scheme.Cover.pullbackCover 𝒰 g).J) → ((Scheme.Cover.pullbackCover 𝒰 g).obj i).OpenCover :=
  fun i => ((Scheme.Cover.pullbackCover 𝒰 g).obj i).affineOpenCover.openCover
U : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) × (𝒱 i).J × (𝒲 i).J →
  TopologicalSpace.Opens (↑↑X.toPresheafedSpace × ↑↑Y.toPresheafedSpace) :=
  fun ijk =>
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).map ijk.snd.1 ≫ (Scheme.Cover.pullbackCover 𝒰 f).map ijk.fst) ∧
            P.2 ∈ Scheme.Hom.opensRange ((𝒲 ijk.fst).map ijk.snd.2 ≫ (Scheme.Cover.pullbackCover 𝒰 g).map ijk.fst)},
      is_open' := ⋯ }
this : Set.range L ⊆ ↑(iSup U)
𝓤 : Scheme.Cover (@IsOpenImmersion) (pullback f g) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f g) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i) (pullback.snd f (𝒰.map i)) (pullback.snd g (𝒰.map i))
⊢ ∀ (i : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) × (𝒱 i).J × (𝒲 i).J),
    (fun x => ((ConcreteCategory.hom (pullback.fst f g).base) x, (ConcreteCategory.hom (pullback.snd f g).base) x)) ⁻¹'
        ↑(U i) ⊆
      Set.range ((fun i => ⇑(ConcreteCategory.hom (𝓤.map i).base)) i)

case refine_3
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↑↑(pullback f g).toPresheafedSpace → ↑↑X.toPresheafedSpace × ↑↑Y.toPresheafedSpace :=
  fun x => ((ConcreteCategory.hom (pullback.fst f g).base) x, (ConcreteCategory.hom (pullback.snd f g).base) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY →
        IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(ConcreteCategory.hom (pullback.map f' g' f g iX iY iS e₁ e₂).base))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) → ((Scheme.Cover.pullbackCover 𝒰 f).obj i).OpenCover :=
  fun i => ((Scheme.Cover.pullbackCover 𝒰 f).obj i).affineOpenCover.openCover
𝒲 : (i : (Scheme.Cover.pullbackCover 𝒰 g).J) → ((Scheme.Cover.pullbackCover 𝒰 g).obj i).OpenCover :=
  fun i => ((Scheme.Cover.pullbackCover 𝒰 g).obj i).affineOpenCover.openCover
U : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) × (𝒱 i).J × (𝒲 i).J →
  TopologicalSpace.Opens (↑↑X.toPresheafedSpace × ↑↑Y.toPresheafedSpace) :=
  fun ijk =>
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).map ijk.snd.1 ≫ (Scheme.Cover.pullbackCover 𝒰 f).map ijk.fst) ∧
            P.2 ∈ Scheme.Hom.opensRange ((𝒲 ijk.fst).map ijk.snd.2 ≫ (Scheme.Cover.pullbackCover 𝒰 g).map ijk.fst)},
      is_open' := ⋯ }
this : Set.range L ⊆ ↑(iSup U)
𝓤 : Scheme.Cover (@IsOpenImmersion) (pullback f g) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f g) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i) (pullback.snd f (𝒰.map i)) (pullback.snd g (𝒰.map i))
⊢ ∀ (i : (i : (Scheme.Cover.pullbackCover 𝒰 f).J) × (𝒱 i).J × (𝒲 i).J),
    IsEmbedding
      ((fun x => ((ConcreteCategory.hom (pullback.fst f g).base) x, (ConcreteCategory.hom (pullback.snd f g).base) x)) ∘
        (fun i => ⇑(ConcreteCategory.hom (𝓤.map i).base)) i)