-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
/--
Let `x : X` and `f g : X ⟶ Y` be two morphisms such that `f x = g x`.
If `f` and `g` agree on the stalk of `x`, then they agree on an open neighborhood of `x`,
provided `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 type.
-/
@[stacks 0BX6]
lemma spread_out_unique_of_isGermInjective {x : X} [X.IsGermInjectiveAt x]
    (f g : X ⟶ Y) (e : f.base x = g.base x)
    (H : f.stalkMap x =
      Y.presheaf.stalkSpecializes (Inseparable.of_eq e.symm).specializes ≫ g.stalkMap x) :
    ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Proof state:
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : (ConcreteCategory.hom f.base) x ∈ ↑V
hxV' : (ConcreteCategory.hom g.base) x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Scheme.Hom.resLE f V U ⋯ ≫ (↑V).isoSpec.hom = Scheme.Hom.resLE g V U ⋯ ≫ (↑V).isoSpec.hom

Tactic:
simp only [Scheme.isoSpec, asIso_hom, Scheme.toSpecΓ_naturality,
  Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]

Result:
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : (ConcreteCategory.hom f.base) x ∈ ↑V
hxV' : (ConcreteCategory.hom g.base) x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ (↑U).toSpecΓ ≫ Spec.map (Scheme.Hom.appLE f (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE f V U ⋯ ⁻¹ᵁ ⊤) ⋯) =
    (↑U).toSpecΓ ≫ Spec.map (Scheme.Hom.appLE g (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE g V U ⋯ ⁻¹ᵁ ⊤) ⋯)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.e_a
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : (ConcreteCategory.hom f.base) x ∈ ↑V
hxV' : (ConcreteCategory.hom g.base) x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this : Mono (X.presheaf.germ U x hxU)
⊢ Y.presheaf.germ V ((ConcreteCategory.hom f.base) x) ⋯ ≫ Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x =
    Y.presheaf.germ V ((ConcreteCategory.hom g.base) x) ⋯ ≫ Scheme.Hom.stalkMap g x

Tactic:
simp only [TopCat.Presheaf.germ_stalkSpecializes_assoc, Scheme.stalkMap_germ]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : (ConcreteCategory.hom f.base) x ∈ ↑V
hxV' : (ConcreteCategory.hom g.base) x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
refine ⟨U, hxU, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom g.base) x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : (ConcreteCategory.hom f.base) x ∈ ↑V
hxV' : (ConcreteCategory.hom g.base) x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ U.ι ≫ f = U.ι ≫ g