-- Mathlib/AlgebraicGeometry/Properties.lean
theorem map_injective_of_isIntegral [IsIntegral X] {U V : X.Opens} (i : U ⟶ V)
    [H : Nonempty U] : Function.Injective (X.presheaf.map i.op)

Proof state:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.map i.op))

Tactic:
rw [injective_iff_map_eq_zero]

Result:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ ∀ (a : ↑Γ(X, V)), (ConcreteCategory.hom (X.presheaf.map i.op)) a = 0 → a = 0

Proof state:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ ∀ (a : ↑Γ(X, V)), (ConcreteCategory.hom (X.presheaf.map i.op)) a = 0 → a = 0

Tactic:
intro x hx

Result:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
hx : (ConcreteCategory.hom (X.presheaf.map i.op)) x = 0
⊢ x = 0

Proof state:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
⊢ U ⊓ X.basicOpen x = ⊥ → X.basicOpen x = ⊥

Tactic:
contrapose!

Result:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
⊢ X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥

Proof state:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
⊢ X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥

Tactic:
simp_rw [Ne, ← Opens.not_nonempty_iff_eq_bot, Classical.not_not]

Result:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
⊢ (↑(X.basicOpen x)).Nonempty → (↑(U ⊓ X.basicOpen x)).Nonempty

Proof state:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
hx : U ⊓ X.basicOpen x = ⊥
⊢ X.basicOpen x = ⊥

Tactic:
revert hx

Result:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
⊢ U ⊓ X.basicOpen x = ⊥ → X.basicOpen x = ⊥

Proof state:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
⊢ (↑(X.basicOpen x)).Nonempty → (↑(U ⊓ X.basicOpen x)).Nonempty

Tactic:
apply nonempty_preirreducible_inter U.isOpen (RingedSpace.basicOpen _ _).isOpen

Result:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
⊢ (↑U).Nonempty

Proof state:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
hx : X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i.op)) x) = ⊥
⊢ X.basicOpen x = ⊥

Tactic:
rw [Scheme.basicOpen_res] at hx

Result:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
hx : U ⊓ X.basicOpen x = ⊥
⊢ X.basicOpen x = ⊥

Proof state:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
hx : (ConcreteCategory.hom (X.presheaf.map i.op)) x = 0
⊢ x = 0

Tactic:
rw [← basicOpen_eq_bot_iff] at hx ⊢

Result:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
hx : X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i.op)) x) = ⊥
⊢ X.basicOpen x = ⊥

Proof state:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↑↑(↑U).toPresheafedSpace
x : ↑Γ(X, V)
⊢ (↑U).Nonempty

Tactic:
simpa using H

Result:
no goals