-- Mathlib/AlgebraicGeometry/FunctionField.lean
theorem germ_injective_of_isIntegral [IsIntegral X] {U : X.Opens} (x : X) (hx : x ∈ U) :
    Function.Injective (X.presheaf.germ U x hx)

Proof state:
case intro.intro.intro.intro.refl
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
W : Opens ↑↑X.toPresheafedSpace
hW : x ∈ W
iU : W ⟶ U
e : (ConcreteCategory.hom (X.presheaf.map iU.op)) y = (ConcreteCategory.hom (X.presheaf.map iU.op)) 0
⊢ y = 0

Tactic:
haveI : Nonempty W := ⟨⟨_, hW⟩⟩

Result:
case intro.intro.intro.intro.refl
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
W : Opens ↑↑X.toPresheafedSpace
hW : x ∈ W
iU : W ⟶ U
e : (ConcreteCategory.hom (X.presheaf.map iU.op)) y = (ConcreteCategory.hom (X.presheaf.map iU.op)) 0
this : Nonempty ↑↑(↑W).toPresheafedSpace
⊢ y = 0

Proof state:
case intro.intro.intro.intro.refl
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
W : Opens ↑↑X.toPresheafedSpace
hW : x ∈ W
iU : W ⟶ U
e : (ConcreteCategory.hom (X.presheaf.map iU.op)) y = (ConcreteCategory.hom (X.presheaf.map iU.op)) 0
this : Nonempty ↑↑(↑W).toPresheafedSpace
⊢ y = 0

Tactic:
exact map_injective_of_isIntegral X iU e

Result:
no goals

Proof state:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ ∀ (a : ↑(X.presheaf.obj (op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) a = 0 → a = 0

Tactic:
intro y hy

Result:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = 0
⊢ y = 0

Proof state:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
⊢ y = 0

Tactic:
obtain ⟨W, hW, iU, iV, e⟩ := X.presheaf.germ_eq _ hx hx _ _ hy

Result:
case intro.intro.intro.intro
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
W : Opens ↑↑X.toPresheafedSpace
hW : x ∈ W
iU iV : W ⟶ U
e : (ConcreteCategory.hom (X.presheaf.map iU.op)) y = (ConcreteCategory.hom (X.presheaf.map iV.op)) 0
⊢ y = 0

Proof state:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = 0
⊢ y = 0

Tactic:
rw [← (X.presheaf.germ U x hx).hom.map_zero] at hy

Result:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
⊢ y = 0

Proof state:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))

Tactic:
rw [injective_iff_map_eq_zero]

Result:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ ∀ (a : ↑(X.presheaf.obj (op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) a = 0 → a = 0

Proof state:
case intro.intro.intro.intro
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
W : Opens ↑↑X.toPresheafedSpace
hW : x ∈ W
iU iV : W ⟶ U
e : (ConcreteCategory.hom (X.presheaf.map iU.op)) y = (ConcreteCategory.hom (X.presheaf.map iV.op)) 0
⊢ y = 0

Tactic:
cases Subsingleton.elim iU iV

Result:
case intro.intro.intro.intro.refl
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
W : Opens ↑↑X.toPresheafedSpace
hW : x ∈ W
iU : W ⟶ U
e : (ConcreteCategory.hom (X.presheaf.map iU.op)) y = (ConcreteCategory.hom (X.presheaf.map iU.op)) 0
⊢ y = 0