awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
H : ∃ (i : ι), s i ∉ x.asIdeal
i : ι := H.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)
this :
  Set.range (ι := PrimeSpectrum (Localization.Away (s i)))
      (PrimeSpectrum.comap (algebraMap (↑R : Type u_2) (Localization.Away (s i)))) =
    (↑(PrimeSpectrum.basicOpen (s i)) : Set (PrimeSpectrum (↑R : Type u_2)))
⊢ Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec
          (CommRingCat.of
            (Localization.Away
              (s
                (have this := H;
                this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)))))))
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R : Type u_2)
              (Localization.Away
                (s
                  (have this := H;
                  this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal))))))))
    x

Tactic:
exact (eq_iff_iff.mp congr(x ∈ $this)).mpr H.choose_spec

Premises used: Iff.mpr, Exists.choose_spec, congrArg, Membership.mem, id, Iff.mp, eq_iff_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
x : ↥X
hx : x ∈ U
hcover : (∃ (x_1 : ↥X) (y : ↥(𝒰.X (Cover.idx 𝒰 x_1))), (𝒰.f (Cover.idx 𝒰 x_1)) y = x) ∧ x ∈ U
⊢ Membership.mem (γ := TopologicalSpace.Opens ↥X)
    (⨆ (i : ↥X), Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U) x

Tactic:
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.coe_opensRange, Opens.mem_mk,
      Set.mem_iUnion, Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]

Premises used: Set.mem_range, TopologicalSpace.Opens.iSup_mk, Set.mem_inter_iff, Set.mem_iUnion, exists_and_right, TopologicalSpace.Opens.carrier_eq_coe, SetLike.mem_coe, TopologicalSpace.Opens.coe_inf, AlgebraicGeometry.Scheme.Hom.coe_opensRange, TopologicalSpace.Opens.mem_mk
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
x : ↥X
hx : x ∈ U
⊢ (∃ (x_1 : ↥X) (y : ↥(𝒰.X (Cover.idx 𝒰 x_1))), (𝒰.f (Cover.idx 𝒰 x_1)) y = x) ∧ x ∈ U

Tactic:
⟨?_, hx⟩

Premises used: And.intro
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
x : ↥X
hx : x ∈ U
hcover : ∃ (x_1 : ↥X) (y : ↥(𝒰.X (Cover.idx 𝒰 x_1))), (𝒰.f (Cover.idx 𝒰 x_1)) y = x
⊢ (∃ (x_1 : ↥X) (y : ↥(𝒰.X (Cover.idx 𝒰 x_1))), (𝒰.f (Cover.idx 𝒰 x_1)) y = x) ∧ x ∈ U

Tactic:
refine ⟨?_, hx⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
x : ↥X
hx : x ∈ U
⊢ ∃ (x_1 : ↥X) (y : ↥(𝒰.X (Cover.idx 𝒰 x_1))), (𝒰.f (Cover.idx 𝒰 x_1)) y = x

Tactic:
simpa using ⟨_, 𝒰.covers x⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
x : ↥X
⊢ Eq (α := (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
            (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
        f :
      (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
            (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
        g :
      (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))

Tactic:
replace h := h (𝒰.idx x)
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
x : ↥X
h :
  Eq (α := (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
            (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
        f :
      (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
            (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
        g :
      (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
⊢ Eq (α := (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
            (CategoryStruct.comp (Y :=
              X.presheaf.obj (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 x)) (𝒰.f (Cover.idx 𝒰 x)) ⊓ U)))
              (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (Iso.inv (IsOpenImmersion.ΓIso (𝒰.f (Cover.idx 𝒰 x)) U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
        f :
      (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
            (CategoryStruct.comp (Y :=
              X.presheaf.obj (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 x)) (𝒰.f (Cover.idx 𝒰 x)) ⊓ U)))
              (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (Iso.inv (IsOpenImmersion.ΓIso (𝒰.f (Cover.idx 𝒰 x)) U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
        g :
      (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))

Tactic:
rw [← IsOpenImmersion.map_ΓIso_inv] at h

Premises used: AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
i : 𝒰.I₀
rw :
  Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
⊢ Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        0 :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
i : 𝒰.I₀
⊢ Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))

Tactic:
h i
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
i : 𝒰.I₀
⊢ Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))

Tactic:
exact h i
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
h :
  ∀ (i : 𝒰.I₀),
    IsNilpotent (R := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
choose :
  ∀ (fn : (i : 𝒰.I₀) → ℕ)
    (hfn :
      ∀ (i : 𝒰.I₀),
        HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
                  (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
                s :
              (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            (fn i) =
          0),
    IsNilpotent s
⊢ IsNilpotent s

Tactic:
choose fn hfn using h
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
have : ∀ (this : Fintype 𝒰.I₀), IsNilpotent s
⊢ IsNilpotent s

Tactic:
have : Fintype 𝒰.I₀ := Fintype.ofFinite 𝒰.I₀
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
⊢ ∀ (i : 𝒰.I₀), fn i ≤ N

Tactic:
have hfnleN (i : 𝒰.I₀) : fn i ≤ N := Finset.le_sup (Finset.mem_univ i)
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
h : s ^ N = 0
⊢ IsNilpotent s

Tactic:
use N
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          (s ^ N) :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
⊢ s ^ N = 0

Tactic:
apply zero_of_zero_cover (𝒰 := 𝒰)

Premises used: AlgebraicGeometry.Scheme.zero_of_zero_cover
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
i : 𝒰.I₀
h :
  HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      N =
    0
⊢ Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (s ^ N) :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))

Tactic:
simp only [map_pow]

Premises used: map_pow
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
h :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        N =
      0
⊢ ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          (s ^ N) :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))

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

Premises used: map_pow
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
i : 𝒰.I₀
⊢ HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      N =
    0

Tactic:
pow_eq_zero_of_le (hfnleN i) (hfn i)

Premises used: pow_eq_zero_of_le
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
i : 𝒰.I₀
⊢ HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      N =
    0

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

Premises used: pow_eq_zero_of_le