-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
n : (i : (↑s : Type u)) → ℕ
this_1 : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
hU : IsCompact.{u} (X := ↥X) (Opens.carrier (⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)))
x f : (↑Γ(X, ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : 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
h₁ :
  ∀ (i : (↑s : Type u)),
    (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
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, ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : 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, ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : 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 :
  ∀ (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, ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : 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))
h :
  ∀ (i : (↑s : Type u)),
    Eq (α :=
      (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
            (op (↑(↑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 :=
              X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
                (op (⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))))
              (X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).map
                (Quiver.Hom.op
                  (Opens.leSupr (X := (↑X.toPresheafedSpace : TopCat))
                    (fun (i : (↑s : Type u)) ↦ (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) i))) :
            (a :
                (↑(X.sheaf.obj.obj (op (⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)))) :
                  Type u)) →
              (↑(X.sheaf.obj.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) : Type u))
          (f ^ Finset.sup Finset.univ n * x) :
        (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
              (op (↑(↑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 :=
              X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
                (op (⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))))
              (X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).map
                (Quiver.Hom.op
                  (Opens.leSupr (X := (↑X.toPresheafedSpace : TopCat))
                    (fun (i : (↑s : Type u)) ↦ (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) i))) :
            (a :
                (↑(X.sheaf.obj.obj (op (⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)))) :
                  Type u)) →
              (↑(X.sheaf.obj.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) : Type u))
          0 :
        (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
              (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) :
          Type u))
⊢ f ^ Finset.sup Finset.univ n * x = 0

Tactic:
apply TopCat.Sheaf.eq_of_locally_eq X.sheaf fun i : s => (i : X.Opens)

Premises used: TopCat.Sheaf.eq_of_locally_eq, AlgebraicGeometry.Scheme.sheaf, Subtype.val