-- 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.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 ⋯

Tactic:
rw [← cancel_mono (X.presheaf.germ U x hxU)]

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

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

Tactic:
rintro U V rfl rfl

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

Tactic:
rw [← cancel_mono V.toScheme.isoSpec.hom]

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₀ ⋯
⊢ Scheme.Hom.resLE f V U ⋯ ≫ (↑V).isoSpec.hom = Scheme.Hom.resLE g V U ⋯ ≫ (↑V).isoSpec.hom

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
hxV' : (ConcreteCategory.hom g.base) x ∈ V
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
obtain ⟨U, hxU, _, hUV, HU⟩ := X.exists_le_and_germ_injective x (f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V) ⟨hxV, hxV'⟩

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, 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))
⊢ U.ι ≫ f = U.ι ≫ g

Tactic:
rw [← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_left),
  ← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_right)]

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