-- 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:
case intro.intro.intro.intro
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' := ⋯ }
z : ↑↑(pullback f g).toPresheafedSpace
is : 𝒰.J
s : ↑↑(𝒰.obj is).toPresheafedSpace
hsx :
  (ConcreteCategory.hom (𝒰.map is).base) s =
    (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f g).base) z)
hsy :
  (ConcreteCategory.hom (𝒰.map is).base) s =
    (ConcreteCategory.hom g.base) ((ConcreteCategory.hom (pullback.snd f g).base) z)
x : ↑↑((Scheme.Cover.pullbackCover 𝒰 f).obj is).toPresheafedSpace
hx : (ConcreteCategory.hom (pullback.fst f (𝒰.map is)).base) x = (ConcreteCategory.hom (pullback.fst f g).base) z
y : ↑↑((Scheme.Cover.pullbackCover 𝒰 g).obj is).toPresheafedSpace
hy : (ConcreteCategory.hom (pullback.fst g (𝒰.map is)).base) y = (ConcreteCategory.hom (pullback.snd f g).base) z
⊢ ∃ a a_1 b, L z ∈ U ⟨a, (a_1, b)⟩

Tactic:
obtain ⟨ix, x, rfl⟩ := (𝒱 is).exists_eq x

Result:
case intro.intro.intro.intro.intro.intro
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' := ⋯ }
z : ↑↑(pullback f g).toPresheafedSpace
is : 𝒰.J
s : ↑↑(𝒰.obj is).toPresheafedSpace
hsx :
  (ConcreteCategory.hom (𝒰.map is).base) s =
    (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f g).base) z)
hsy :
  (ConcreteCategory.hom (𝒰.map is).base) s =
    (ConcreteCategory.hom g.base) ((ConcreteCategory.hom (pullback.snd f g).base) z)
y : ↑↑((Scheme.Cover.pullbackCover 𝒰 g).obj is).toPresheafedSpace
hy : (ConcreteCategory.hom (pullback.fst g (𝒰.map is)).base) y = (ConcreteCategory.hom (pullback.snd f g).base) z
ix : (𝒱 is).J
x : ↑↑((𝒱 is).obj ix).toPresheafedSpace
hx :
  (ConcreteCategory.hom (pullback.fst f (𝒰.map is)).base) ((ConcreteCategory.hom ((𝒱 is).map ix).base) x) =
    (ConcreteCategory.hom (pullback.fst f g).base) z
⊢ ∃ a a_1 b, L z ∈ U ⟨a, (a_1, b)⟩

Proof state:
case h.e'_5.h
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)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↑↑(pullback (Spec.map φ) (Spec.map ψ)).toPresheafedSpace =
    ↑↑(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A)))
            (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B)))).toPresheafedSpace
⊢ L ∘ ⇑(ConcreteCategory.hom (pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂).base) =
    (Prod.map ⇑(ConcreteCategory.hom iX.base) ⇑(ConcreteCategory.hom iY.base) ∘
        PrimeSpectrum.tensorProductTo ↑R ↑A ↑B) ∘
      ⇑(Scheme.homeoOfIso (pullbackSpecIso ↑R ↑A ↑B))

Tactic:
ext1 x

Result:
case h.e'_5.h.h
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)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↑↑(pullback (Spec.map φ) (Spec.map ψ)).toPresheafedSpace =
    ↑↑(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A)))
            (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B)))).toPresheafedSpace
x : ↑↑(pullback (Spec.map φ) (Spec.map ψ)).toPresheafedSpace
⊢ (L ∘ ⇑(ConcreteCategory.hom (pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂).base)) x =
    ((Prod.map ⇑(ConcreteCategory.hom iX.base) ⇑(ConcreteCategory.hom iY.base) ∘
          PrimeSpectrum.tensorProductTo ↑R ↑A ↑B) ∘
        ⇑(Scheme.homeoOfIso (pullbackSpecIso ↑R ↑A ↑B)))
      x