-- 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:
case 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
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
have hxV' : g.base x ∈ V := e ▸ hxV

Result:
case 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 ∈ U ∧ U.ι ≫ f = U.ι ≫ g

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
⊢ Scheme.Hom.appLE f V U ⋯ = Scheme.Hom.appLE g V U ⋯

Tactic:
have := ConcreteCategory.mono_of_injective _ HU

Result:
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)
⊢ Scheme.Hom.appLE f V U ⋯ = Scheme.Hom.appLE 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)
⊢ Scheme.Hom.appLE f V U ⋯ ≫ X.presheaf.germ U x hxU = Scheme.Hom.appLE g V U ⋯ ≫ X.presheaf.germ U x hxU

Tactic:
simp only [Scheme.Hom.appLE, Category.assoc, X.presheaf.germ_res', ← Scheme.stalkMap_germ, H]

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

Proof state:
case e_a.e_f
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.appLE f (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE f V U ⋯ ⁻¹ᵁ ⊤) ⋯ =
    Scheme.Hom.appLE g (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE g V U ⋯ ⁻¹ᵁ ⊤) ⋯

Tactic:
apply this <;> simp

Result:
no goals

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
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
obtain ⟨_, ⟨V : Y.Opens, hV, rfl⟩, hxV, -⟩ :=
  (isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ (f.base x)) isOpen_univ

Result:
case 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
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g