-- 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.intro.intro.intro.intro.intro.intro.refine_2
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 ≫ φ'
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX

Tactic:
rw [← IsAffineOpen.Spec_map_appLE_fromSpec sY hU hV iVU, ← Spec.map_comp_assoc, ← h₂,
  ← Scheme.Hom.appLE, ← hW.isoSpec_hom, IsAffineOpen.Spec_map_appLE_fromSpec sX hU hW i,
  ← Iso.eq_inv_comp, IsAffineOpen.isoSpec_inv_ι_assoc]

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, ∃ (hxU : x ∈ U), ∃ f, Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
  (isBasis_affine_open S).exists_subset_of_mem_open (Set.mem_univ (sX.base x)) isOpen_univ

Result:
case 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
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, 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
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
have : sY.appLE U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ =
    sX.app U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU := by
  rw [Scheme.Hom.appLE, Category.assoc, Y.presheaf.germ_res_assoc,
    ← Scheme.stalkMap_germ_assoc, h]
  simp

Result:
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

Proof state:
case 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
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
have hyU : sY.base y ∈ U := e ▸ hxU

Result:
case 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
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX