awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
this :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X) (hZ : IsClosed Z)
    (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    IsClosed (X := ↥(Spec S)) (⇑f '' Z)
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective (α := ↥(Spec R)) (β := ↥X) ⇑g
inst : QuasiCompact (g ≫ f)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)
have this₁ : ∀ (H : StableUnderSpecialization (X := ↥(Spec S)) (Set.image (α := ↥(Spec R)) (⇑(g ≫ f)) (⇑g ⁻¹' Z)))
  (hX : ∃ (R_1 : CommRingCat.{u}), Spec R = Spec R_1),
  IsClosed (X := ↥(Spec S)) (Set.image (α := ↥(Spec R)) (⇑(g ≫ f)) (⇑g ⁻¹' Z))
Tactic: have := this _ (g ≫ f) (g ⁻¹' Z) (hZ.preimage g.continuous)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
this_1 :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X) (hZ : IsClosed Z)
    (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    IsClosed (X := ↥(Spec S)) (⇑f '' Z)
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective (α := ↥(Spec R)) (β := ↥X) ⇑g
inst : QuasiCompact (g ≫ f)
this :
  ∀ (H : StableUnderSpecialization (X := ↥(Spec S)) (Set.image (α := ↥(Spec R)) (⇑(g ≫ f)) (⇑g ⁻¹' Z)))
    (hX : ∃ (R_1 : CommRingCat.{u}), Spec R = Spec R_1),
    IsClosed (X := ↥(Spec S)) (Set.image (α := ↥(Spec R)) (⇑(g ≫ f)) (⇑g ⁻¹' Z))
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)
have this₁ : ∀ (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R_1 : CommRingCat.{u}), Spec R = Spec R_1),
  IsClosed (X := ↥(Spec S)) (⇑f '' Z)
Tactic: simp_rw [Scheme.Hom.comp_base, TopCat.comp_app, ← Set.image_image,
      Set.image_preimage_eq _ hg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
hX : ∃ (R : CommRingCat.{u}), X = Spec R
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)
have obtain : ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ Spec S) [QuasiCompact f] (Z : Set ↥(Spec R)) (hZ : IsClosed Z)
  (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)), IsClosed (X := ↥(Spec S)) (⇑f '' Z)
Tactic: obtain ⟨R, rfl⟩ := hX
Cleared hypotheses: X, f, inst, Z, hZ, H, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
S R : CommRingCat
f : Spec R ⟶ Spec S
inst : QuasiCompact f
Z : Set ↥(Spec R)
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)
have obtain : ∀ (φ : S ⟶ R)
  [QuasiCompact.{u} (X := Spec R) (Y := Spec S) ((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ)]
  (H :
    StableUnderSpecialization (X := ↥(Spec S)) (⇑((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ) '' Z)),
  IsClosed (X := ↥(Spec S)) (⇑((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ) '' Z)
Tactic: obtain ⟨φ, rfl⟩ := Spec.homEquiv.symm.surjective f
Cleared hypotheses: f, inst, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
P : X.Opens → Prop
S : X.Opens
hS : IsCompact (↑S : Set ↥X)
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : (↑X.affineOpens : Type u)), P S → P (S ⊔ (↑U : X.Opens))
⊢ P S
have obtain : ∀ (s : Set (↑X.affineOpens : Type u)) (hs : s.Finite) (hS : IsCompact (↑(⨆ i ∈ s, (↑i : X.Opens)) : Set ↥X)),
  P (⨆ i ∈ s, (↑i : X.Opens))
Tactic: obtain ⟨s, hs, rfl⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hS
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : (↑X.affineOpens : Type u)), P S → P (S ⊔ (↑U : X.Opens))
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
hS : IsCompact (↑(⨆ i ∈ s, (↑i : X.Opens)) : Set ↥X)
⊢ P (⨆ i ∈ s, (↑i : X.Opens))
have refine : ∀ {x : (↑X.affineOpens : Type u)} {s : Set (↑X.affineOpens : Type u)},
  x ∉ s → ∀ (hs : s.Finite) (h₄ : P (⨆ i ∈ s, (↑i : X.Opens))), P (⨆ i ∈ insert x s, (↑i : X.Opens))
Tactic: refine hs.induction_on _ (by simpa using h₁) fun {x s} _ hs h₄ ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : (↑X.affineOpens : Type u)), P S → P (S ⊔ (↑U : X.Opens))
s_1 : Set (↑X.affineOpens : Type u)
hs_1 : s_1.Finite
hS : IsCompact (↑(⨆ i ∈ s_1, (↑i : X.Opens)) : Set ↥X)
x : (↑X.affineOpens : Type u)
s : Set (↑X.affineOpens : Type u)
h : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, (↑i : X.Opens))
⊢ P (⨆ i ∈ insert x s, (↑i : X.Opens))
have rw : P ((⨆ x ∈ s, (↑x : X.Opens)) ⊔ (↑x : X.Opens))
Tactic: rw [iSup_insert, sup_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
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) ⋯)
    0
⊢ ∃ (n : ℕ), f ^ n * x = 0
have 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) sorry)
  ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op) :
      (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
    0)
Tactic: rw [← map_zero (X.presheaf.map (homOfLE <| X.basicOpen_le f : X.basicOpen f ⟶ U).op).hom] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
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 : ℕ), f ^ n * x = 0
have obtain : ∀ (n : ℕ) (e : f ^ n * x = f ^ n * 0), ∃ (n : ℕ), f ^ n * x = 0
Tactic: obtain ⟨n, e⟩ := (hU.isLocalization_basicOpen f).exists_of_eq _ H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
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
⊢ ∃ (n : ℕ), f ^ n * x = 0
have 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
Tactic: obtain ⟨s, hs, e⟩ := isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens.mp ⟨hU, U.2⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
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)
have h : (↑U : Set ↥X) = (↑(⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Set ↥X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
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)
⊢ ∃ (n : ℕ), f ^ n * x = 0
have e₁ : 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
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
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
have rw : (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
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)
⊢ ∃ (n : ℕ), f ^ n * x = 0
have h₁ : ∀ (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))) _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
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 : ℕ), f ^ n * x = 0
have refine_2 : ∀
  (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 sorry).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 sorry).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
Tactic: have H' := fun i : s =>
    exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen X i.1.2
      (X.presheaf.map (homOfLE (h₁ i)).op x) (X.presheaf.map (homOfLE (h₁ i)).op f) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
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
⊢ ∃ (n : ℕ), f ^ n * x = 0
have 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 sorry).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 sorry).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
Tactic: choose n hn using H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
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
⊢ ∃ (n : ℕ), f ^ n * x = 0
have this : Finite.{u + 1} (↑s : Type u)
Tactic: haveI := hs.to_subtype
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
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)
⊢ ∃ (n : ℕ), f ^ n * x = 0
have refine_2 : ∀ (val : Fintype (↑s : Type u)), ∃ (n : ℕ), f ^ n * x = 0
Tactic: cases nonempty_fintype s
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
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)
⊢ ∃ (n : ℕ), f ^ n * x = 0
have h : f ^ Finset.sup Finset.univ n * x = 0
Tactic: use Finset.univ.sup n