-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
/--
Given `S`-schemes `X Y`, a point `x : X`, and a `S`-morphism `φ : Spec 𝒪_{X, x} ⟶ Y`,
we may spread it out to an `S`-morphism `f : U ⟶ 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.
-/
lemma spread_out_of_isGermInjective' [LocallyOfFiniteType sY] {x : X} [X.IsGermInjectiveAt x]
    (φ : Spec (X.presheaf.stalk x) ⟶ Y)
    (h : φ ≫ sY = X.fromSpecStalk x ≫ sX) :
    ∃ (U : X.Opens) (hxU : x ∈ U) (f : U.toScheme ⟶ Y),
      φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Proof state:
case refine_3
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
this :
  ∃ U,
    ∃ (hxU : x ∈ U),
      ∃ f,
        Spec.map (Scheme.stalkClosedPointTo φ) ≫
              Y.fromSpecStalk ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) =
            U.fromSpecStalkOfMem x hxU ≫ f ∧
          f ≫ sY = U.ι ≫ sX
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
simpa only [Scheme.Spec_stalkClosedPointTo_fromSpecStalk] using this

Result:
no goals

Proof state:
case refine_2.a
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Spec.map
        (Scheme.Hom.stalkMap sY ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) ≫
          Scheme.stalkClosedPointTo φ) ≫
      S.fromSpecStalk
        ((ConcreteCategory.hom sY.base)
          ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))) =
    Spec.map (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x) ≫
      S.fromSpecStalk
        ((ConcreteCategory.hom sY.base) ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))))

Tactic:
simpa only [Spec.map_comp, Category.assoc, Scheme.Spec_map_stalkMap_fromSpecStalk,
  Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc,
  Scheme.Spec_map_stalkSpecializes_fromSpecStalk]

Result:
no goals

Proof state:
case refine_2.a
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Spec.map
      (Scheme.Hom.stalkMap sY ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) ≫
        Scheme.stalkClosedPointTo φ) =
    Spec.map (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x)

Tactic:
rw [← cancel_mono (S.fromSpecStalk _)]

Result:
case refine_2.a
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Spec.map
        (Scheme.Hom.stalkMap sY ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) ≫
          Scheme.stalkClosedPointTo φ) ≫
      S.fromSpecStalk
        ((ConcreteCategory.hom sY.base)
          ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))) =
    Spec.map (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x) ≫
      S.fromSpecStalk
        ((ConcreteCategory.hom sY.base) ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))))

Proof state:
case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ (ConcreteCategory.hom sX.base) x =
    (ConcreteCategory.hom sY.base) ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))

Tactic:
rw [← Scheme.comp_base_apply, h, Scheme.comp_base_apply, Scheme.fromSpecStalk_closedPoint]

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
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
have := spread_out_of_isGermInjective sX sY ?_ (Scheme.stalkClosedPointTo φ) ?_

Result:
case refine_3
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
this :
  ∃ U,
    ∃ (hxU : x ∈ U),
      ∃ f,
        Spec.map (Scheme.stalkClosedPointTo φ) ≫
              Y.fromSpecStalk ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) =
            U.fromSpecStalkOfMem x hxU ≫ f ∧
          f ≫ sY = U.ι ≫ sX
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ (ConcreteCategory.hom sX.base) x =
    (ConcreteCategory.hom sY.base) ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))

case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Scheme.Hom.stalkMap sY ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) ≫
      Scheme.stalkClosedPointTo φ =
    S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x

Proof state:
case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Scheme.Hom.stalkMap sY ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) ≫
      Scheme.stalkClosedPointTo φ =
    S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x

Tactic:
apply Spec.map_injective

Result:
case refine_2.a
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Spec.map
      (Scheme.Hom.stalkMap sY ((ConcreteCategory.hom φ.base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) ≫
        Scheme.stalkClosedPointTo φ) =
    Spec.map (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x)