-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
/-- A section over a compact open of a scheme is nilpotent if and only if its associated
basic open is empty. -/
lemma Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact {X : Scheme.{u}}
    {U : X.Opens} (hU : IsCompact (U : Set X)) (f : Γ(X, U)) :
    IsNilpotent f ↔ X.basicOpen f = ⊥

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
this : Subsingleton ↑Γ(X, ⊥)
⊢ ((1 |_ ⊥) ⋯ |_ X.basicOpen f) e = 0

Tactic:
rw [Subsingleton.eq_zero (1 |_ ⊥)]

Result:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
this : Subsingleton ↑Γ(X, ⊥)
⊢ (0 |_ X.basicOpen f) e = 0

Proof state:
case intro
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
n : ℕ
hn : f ^ n * 1 = 0
⊢ IsNilpotent f

Tactic:
rw [mul_one] at hn

Result:
case intro
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent f

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
⊢ (1 |_ X.basicOpen f) ⋯ = 0

Tactic:
have e : X.basicOpen f ≤ ⊥ := by rw [hf]

Result:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ (1 |_ X.basicOpen f) ⋯ = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ ((1 |_ ⊥) ⋯ |_ X.basicOpen f) e = 0

Tactic:
have : Subsingleton Γ(X, ⊥) :=
  CommRingCat.subsingleton_of_isTerminal X.sheaf.isTerminalOfEmpty

Result:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
this : Subsingleton ↑Γ(X, ⊥)
⊢ ((1 |_ ⊥) ⋯ |_ X.basicOpen f) e = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
⊢ IsNilpotent f

Tactic:
have h : (1 : Γ(X, U)) |_ (X.basicOpen f) = 0 := by
  have e : X.basicOpen f ≤ ⊥ := by rw [hf]
  rw [← TopCat.Presheaf.restrict_restrict e bot_le]
  have : Subsingleton Γ(X, ⊥) :=
    CommRingCat.subsingleton_of_isTerminal X.sheaf.isTerminalOfEmpty
  rw [Subsingleton.eq_zero (1 |_ ⊥)]
  show X.presheaf.map _ 0 = 0
  rw [map_zero]

Result:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
⊢ IsNilpotent f

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
this : Subsingleton ↑Γ(X, ⊥)
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE e).op)) 0 = 0

Tactic:
rw [map_zero]

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
this : Subsingleton ↑Γ(X, ⊥)
⊢ (0 |_ X.basicOpen f) e = 0

Tactic:
show X.presheaf.map _ 0 = 0

Result:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
this : Subsingleton ↑Γ(X, ⊥)
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE e).op)) 0 = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
⊢ X.basicOpen f ≤ ⊥

Tactic:
rw [hf]

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
⊢ IsNilpotent f ↔ X.basicOpen f = ⊥

Tactic:
refine ⟨X.basicOpen_eq_bot_of_isNilpotent U f, fun hf ↦ ?_⟩

Result:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
⊢ IsNilpotent f

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ (1 |_ X.basicOpen f) ⋯ = 0

Tactic:
rw [← TopCat.Presheaf.restrict_restrict e bot_le]

Result:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ ((1 |_ ⊥) ⋯ |_ X.basicOpen f) e = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
⊢ IsNilpotent f

Tactic:
obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU 1 f h

Result:
case intro
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
n : ℕ
hn : f ^ n * 1 = 0
⊢ IsNilpotent f

Proof state:
case intro
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent f

Tactic:
use n

Result:
no goals