-- 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.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))
⊢ Scheme.Hom.resLE f V U ⋯ ≫ V.ι = Scheme.Hom.resLE g V U ⋯ ≫ V.ι

Tactic:
congr 1

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

Tactic:
have : IsAffine V := hV

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

Tactic:
suffices ∀ (U₀ V₀) (eU : U = U₀) (eV : V = V₀),
    f.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_left) =
      g.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_right) by
  rw [← cancel_mono V.toScheme.isoSpec.hom]
  simp only [Scheme.isoSpec, asIso_hom, Scheme.toSpecΓ_naturality,
    Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
  congr 2
  apply this <;> simp

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
⊢ ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯

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₀ ⋯
⊢ (↑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 ⋯ ⁻¹ᵁ ⊤) ⋯)

Tactic:
congr 2

Result:
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 ⋯ ⁻¹ᵁ ⊤) ⋯