-- Mathlib/AlgebraicGeometry/Cover/Open.lean
/-- If a global section is nilpotent on each member of a finite open cover, then `f` is
nilpotent. -/
lemma isNilpotent_of_isNilpotent_cover {X : Scheme.{u}} {U : X.Opens} (s : Γ(X, U))
    (𝒰 : X.OpenCover) [Finite 𝒰.J] (h : ∀ i : 𝒰.J, IsNilpotent ((𝒰.map i).app U s)) :
    IsNilpotent s

Proof state:
case h.h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
⊢ ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) (s ^ N) = 0

Tactic:
intro i

Result:
case h.h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
i : 𝒰.J
⊢ (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) (s ^ N) = 0

Proof state:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
⊢ IsNilpotent s

Tactic:
let N : ℕ := Finset.sup Finset.univ fn

Result:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
⊢ IsNilpotent s

Proof state:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
⊢ IsNilpotent s

Tactic:
have hfnleN (i : 𝒰.J) : fn i ≤ N := Finset.le_sup (Finset.mem_univ i)

Result:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
⊢ IsNilpotent s

Proof state:
case h.h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
⊢ ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) (s ^ N) = 0

Tactic:
on_goal 1 => intro i; simp only [map_pow]

Result:
case h.h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
i : 𝒰.J
⊢ (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ N = 0

Proof state:
case h.h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
i : 𝒰.J
⊢ (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) (s ^ N) = 0

Tactic:
simp only [map_pow]

Result:
case h.h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
i : 𝒰.J
⊢ (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ N = 0

Proof state:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h : ∀ (i : 𝒰.J), IsNilpotent ((ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s)
⊢ IsNilpotent s

Tactic:
choose fn hfn using h

Result:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
⊢ IsNilpotent s

Proof state:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
⊢ IsNilpotent s

Tactic:
use N

Result:
case h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
⊢ s ^ N = 0

Proof state:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
⊢ IsNilpotent s

Tactic:
have : Fintype 𝒰.J := Fintype.ofFinite 𝒰.J

Result:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
⊢ IsNilpotent s

Proof state:
case h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
⊢ s ^ N = 0

Tactic:
apply zero_of_zero_cover (𝒰 := 𝒰)

Result:
case h.h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
⊢ ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) (s ^ N) = 0

Proof state:
case h.h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ fn i = 0
this : Fintype 𝒰.J
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.J), fn i ≤ N
i : 𝒰.J
⊢ (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s ^ N = 0

Tactic:
exact pow_eq_zero_of_le (hfnleN i) (hfn i)

Result:
no goals