-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
/--
Given `S`-schemes `X Y` and points `x : X` `y : Y` over `s : S`.
Suppose we have the following diagram of `S`-schemes
```
Spec 𝒪_{X, x} ⟶ X
    |
  Spec(φ)
    ↓
Spec 𝒪_{Y, y} ⟶ Y
```
Then the map `Spec(φ)` spreads out to an `S`-morphism on an open subscheme `U ⊆ X`,
```
Spec 𝒪_{X, x} ⟶ U ⊆ X
    |             |
  Spec(φ)         |
    ↓             ↓
Spec 𝒪_{Y, y} ⟶ Y
```
provided that `Y` is locally of finite type over `S` and
`X` is "germ-injective" at `x` (e.g. when it's integral or locally noetherian).

TODO: The condition on `X` is unnecessary when `Y` is locally of finite presentation.
-/
@[stacks 0BX6]
lemma spread_out_of_isGermInjective [LocallyOfFiniteType sY] {x : X} [X.IsGermInjectiveAt x] {y : Y}
    (e : sX.base x = sY.base y) (φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x)
    (h : sY.stalkMap y ≫ φ =
      S.presheaf.stalkSpecializes (Inseparable.of_eq e).specializes ≫ sX.stalkMap x) :
    ∃ (U : X.Opens) (hxU : x ∈ U) (f : U.toScheme ⟶ Y),
      Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧
      f ≫ sY = U.ι ≫ sX

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
y : ↑↑Y.toPresheafedSpace
e : (ConcreteCategory.hom sX.base) x = (ConcreteCategory.hom sY.base) y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↑↑S.toPresheafedSpace
hU : U ∈ S.affineOpens
hxU : (ConcreteCategory.hom sX.base) x ∈ ↑U
hyU : (ConcreteCategory.hom sY.base) y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
obtain ⟨W, hxW, φ', i, hW, h₁, h₂⟩ :=
  exists_lift_of_germInjective (R := Γ(S, U)) (A := Γ(Y, V)) (U := sX ⁻¹ᵁ U) (x := x) hxU
  (Y.presheaf.germ _ y hyV ≫ φ) (sY.appLE U V iVU) (sX.app U)
  (LocallyOfFiniteType.finiteType_of_affine_subset ⟨_, hU⟩ ⟨_, hV⟩ _) this

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
y : ↑↑Y.toPresheafedSpace
e : (ConcreteCategory.hom sX.base) x = (ConcreteCategory.hom sY.base) y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↑↑S.toPresheafedSpace
hU : U ∈ S.affineOpens
hxU : (ConcreteCategory.hom sX.base) x ∈ ↑U
hyU : (ConcreteCategory.hom sY.base) y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Proof state:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
y : ↑↑Y.toPresheafedSpace
e : (ConcreteCategory.hom sX.base) x = (ConcreteCategory.hom sY.base) y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↑↑S.toPresheafedSpace
hU : U ∈ S.affineOpens
hxU : (ConcreteCategory.hom sX.base) x ∈ ↑U
hyU : (ConcreteCategory.hom sY.base) y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
⊢ Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Tactic:
rw [Scheme.Hom.appLE, Category.assoc, Y.presheaf.germ_res_assoc,
  ← Scheme.stalkMap_germ_assoc, h]

Result:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
y : ↑↑Y.toPresheafedSpace
e : (ConcreteCategory.hom sX.base) x = (ConcreteCategory.hom sY.base) y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↑↑S.toPresheafedSpace
hU : U ∈ S.affineOpens
hxU : (ConcreteCategory.hom sX.base) x ∈ ↑U
hyU : (ConcreteCategory.hom sY.base) y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
⊢ S.presheaf.germ U ((ConcreteCategory.hom sY.base) y) ⋯ ≫ S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x =
    Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
y : ↑↑Y.toPresheafedSpace
e : (ConcreteCategory.hom sX.base) x = (ConcreteCategory.hom sY.base) y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↑↑S.toPresheafedSpace
hU : U ∈ S.affineOpens
hxU : (ConcreteCategory.hom sX.base) x ∈ ↑U
hyU : (ConcreteCategory.hom sY.base) y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ Spec.map φ ≫ Y.fromSpecStalk y = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV

Tactic:
rw [W.fromSpecStalkOfMem_toSpecΓ_assoc x hxW, ← Spec.map_comp_assoc, ← h₁,
  Spec.map_comp, Category.assoc, ← IsAffineOpen.fromSpecStalk,
  IsAffineOpen.fromSpecStalk_eq_fromSpecStalk]

Result:
no goals

Proof state:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
y : ↑↑Y.toPresheafedSpace
e : (ConcreteCategory.hom sX.base) x = (ConcreteCategory.hom sY.base) y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↑↑S.toPresheafedSpace
hU : U ∈ S.affineOpens
hxU : (ConcreteCategory.hom sX.base) x ∈ ↑U
hyU : (ConcreteCategory.hom sY.base) y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
⊢ S.presheaf.germ U ((ConcreteCategory.hom sY.base) y) ⋯ ≫ S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x =
    Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Tactic:
simp

Result:
no goals