-- 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 h.e'_5.h.h.intro.fst
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 : ↑↑(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B))).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst (Spec.map φ) (Spec.map ψ) ≫ iX).base)
      ((ConcreteCategory.hom (pullbackSpecIso ↑R ↑A ↑B).inv.base) x) =
    (Prod.map (⇑(ConcreteCategory.hom iX.base)) (⇑(ConcreteCategory.hom iY.base))
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
          ((ConcreteCategory.hom (𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))).base) x))).1

Tactic:
erw [← Scheme.comp_base_apply, pullbackSpecIso_inv_fst_assoc]

Result:
case h.e'_5.h.h.intro.fst
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 : ↑↑(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B))).toPresheafedSpace
⊢ (ConcreteCategory.hom (Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) ≫ iX).base) x =
    (Prod.map (⇑(ConcreteCategory.hom iX.base)) (⇑(ConcreteCategory.hom iY.base))
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
          ((ConcreteCategory.hom (𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))).base) x))).1

Proof state:
case h.e'_5.h.h.intro.fst
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 : ↑↑(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B))).toPresheafedSpace
⊢ (ConcreteCategory.hom (Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) ≫ iX).base) x =
    (Prod.map (⇑(ConcreteCategory.hom iX.base)) (⇑(ConcreteCategory.hom iY.base))
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
          ((ConcreteCategory.hom (𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))).base) x))).1

Tactic:
rfl

Result:
no goals

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)
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
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
H : SurjectiveOnStalks g'
⊢ IsEmbedding (L ∘ ⇑(ConcreteCategory.hom (pullback.map f' g' f g iX iY iS e₁ e₂).base))

Tactic:
obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f' := ⟨_, Spec.map_preimage _⟩

Result:
case 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)
R A B : CommRingCat
g' : Spec B ⟶ Spec R
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
e₂ : g' ≫ iS = iY ≫ g
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
H : SurjectiveOnStalks g'
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
⊢ IsEmbedding (L ∘ ⇑(ConcreteCategory.hom (pullback.map (Spec.map φ) g' f g iX iY iS e₁ e₂).base))