awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : (↑Γ(X, U) : Type u_1)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
        (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
      0)
n : ℕ
e : f ^ n * x = f ^ n * 0
⊢ ∃ (n : ℕ), f ^ n * x = 0

Tactic:
exact ⟨n, by simpa [mul_comm x] using e⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
obtain :
  ∀ (s : Set (↑X.affineOpens : Type u)) (hs : s.Finite) (e : U.carrier = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)),
    ∃ (n : ℕ), f ^ n * x = 0
⊢ ∃ (n : ℕ), f ^ n * x = 0

Tactic:
obtain ⟨s, hs, e⟩ := isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens.mp ⟨hU, U.2⟩

Premises used: AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, And.intro, Iff.mp, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U.carrier = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)
h : (↑U : Set ↥X) = (↑(⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Set ↥X)
⊢ U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U.carrier = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)
⊢ (↑U : Set ↥X) = (↑(⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Set ↥X)

Tactic:
simpa using e
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U.carrier = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)
⊢ U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)

Tactic:
replace e : U = iSup fun i : s => (i : X.Opens) := by
    ext1; simpa using e
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
i : (↑s : Type u)
rw :
  (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
⊢ (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U

Tactic:
rw [e]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
i : (↑s : Type u)
⊢ (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)

Tactic:
le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _

Premises used: Set.Mem, le_iSup, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
i : (↑s : Type u)
⊢ (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)

Tactic:
exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _

Premises used: le_iSup, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
⊢ ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U

Tactic:
have h₁ (i : s) : i.1.1 ≤ U := by
    rw [e]
    exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
i : (↑s : Type u)
⊢ Eq (α := (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
        x :
      (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
    (0 : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))

Tactic:
have H : (X.presheaf.map (homOfLE _).op) x = 0 := H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H_1 :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
i : (↑s : Type u)
H :
  Eq (α := (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
        x :
      (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
    (0 : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
⊢ X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        f) ≤
    X.basicOpen f

Tactic:
simp only [Scheme.basicOpen_res, inf_le_right]

Premises used: inf_le_right, AlgebraicGeometry.Scheme.basicOpen_res
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
H' :
  ∀ (i : (↑s : Type u)),
    ∃ (n : ℕ),
      HMul.hMul (β := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (HPow.hPow (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                  (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                f :
              (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
            n)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              x :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) =
        0
refine_2 :
  ∀ (n : (i : (↑s : Type u)) → ℕ)
    (hn :
      ∀ (i : (↑s : Type u)),
        HMul.hMul (β := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
            (HPow.hPow (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                    (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                  f :
                (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              (n i))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                  (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                x :
              (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) =
          0),
    ∃ (n : ℕ), f ^ n * x = 0
⊢ ∃ (n : ℕ), f ^ n * x = 0

Tactic:
choose n hn using H'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
n : (i : (↑s : Type u)) → ℕ
hn :
  ∀ (i : (↑s : Type u)),
    HMul.hMul (β := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (HPow.hPow (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              f :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (n i))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
            x :
          (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) =
      0
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
haveI := hs.to_subtype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
n : (i : (↑s : Type u)) → ℕ
hn :
  ∀ (i : (↑s : Type u)),
    HMul.hMul (β := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (HPow.hPow (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              f :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (n i))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
            x :
          (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) =
      0
this : Finite.{u + 1} (↑s : Type u)
refine_2 : ∀ (val : Fintype (↑s : Type u)), ∃ (n : ℕ), f ^ n * x = 0
⊢ ∃ (n : ℕ), f ^ n * x = 0

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
n : (i : (↑s : Type u)) → ℕ
hn :
  ∀ (i : (↑s : Type u)),
    HMul.hMul (β := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (HPow.hPow (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              f :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (n i))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
            x :
          (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) =
      0
this : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
h : f ^ Finset.sup Finset.univ n * x = 0
⊢ ∃ (n : ℕ), f ^ n * x = 0

Tactic:
use Finset.univ.sup n

Premises used: Finset.univ, Finset.sup
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
n : (i : (↑s : Type u)) → ℕ
hn :
  ∀ (i : (↑s : Type u)),
    HMul.hMul (β := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (HPow.hPow (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              f :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (n i))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
            x :
          (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) =
      0
this : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
h :
  ∀ (i : (↑s : Type u)),
    Eq (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (f ^ Finset.sup Finset.univ n * x) :
        (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      (0 : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
⊢ f ^ Finset.sup Finset.univ n * x = 0

Tactic:
suffices ∀ i : s, X.presheaf.map (homOfLE (h₁ i)).op (f ^ Finset.univ.sup n * x) = 0 by
    subst e
    apply TopCat.Sheaf.eq_of_locally_eq X.sheaf fun i : s => (i : X.Opens)
    intro i
    change _ = (X.sheaf.obj.map _) 0
    rw [map_zero]
    apply this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
n : (i : (↑s : Type u)) → ℕ
this : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
i : (↑s : Type u)
hn :
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      (f ^ (Finset.sup Finset.univ n - n i) * (f ^ n i * x)) =
    HMul.hMul (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) (β :=
      (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (f ^ (Finset.sup Finset.univ n - n i)) :
        (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
      (0 : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
h :
  ∀
    (hn :
      Eq (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
            (f ^ (Finset.sup Finset.univ n - n i + n i) * x) :
          (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (0 : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))),
    n i ≤ Finset.sup Finset.univ n
⊢ Eq (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (f ^ Finset.sup Finset.univ n * x) :
      (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
    (0 : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))

Tactic:
rwa [mul_zero, ← mul_assoc, ← pow_add, tsub_add_cancel_of_le] at hn

Premises used: mul_assoc, pow_add, tsub_add_cancel_of_le, MulZeroClass.mul_zero