-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfopen : IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f
hfinj₁ : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
hfinj₂ :
  Function.Injective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun (i : 𝒰.I₀) ↦ Scheme.Hom.appTop (𝒰.f i)
g : (↑Γ(Y, ⊤) : Type u)
h :
  Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) (Y := X.presheaf.stalk x)
            (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro) :
          (a : (↑(X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
            g :
          (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))
U : Opens (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)
w : U ⟶ ⊤
hx : x ∈ U
hg :
  Eq (α := (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.toRingedSpace.presheaf.map w.op) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op ⊤)) : Type u)) → (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) φ :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            g :
          (↑Γ(X, ⊤) : Type u)) :
      (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
    (0 : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
s : (↑Γ(Y, ⊤) : Type u)
hyv : Membership.mem (α := ↥Y) (Y.basicOpen s) (f x : ↥Y)
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun (i : 𝒰.I₀) ↦
    (𝒰.X i).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (res i) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(𝒰.X i, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, W i) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(𝒰.X i, W i)) (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(𝒰.X i, W i) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) φ :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            g) :
        (↑Γ(𝒰.X i, W i) : Type u))
      (0 : (↑Γ(𝒰.X i, W i) : Type u))
h1 :
  ∀ (i : 𝒰.I₀),
    ∃ (n : ℕ),
      Eq (α := (↑Γ(𝒰.X i, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (res i) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(𝒰.X i, ⊤) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) φ :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (s ^ n * g)) :
          (↑Γ(𝒰.X i, ⊤) : Type u))
        (0 : (↑Γ(𝒰.X i, ⊤) : Type u))
⊢ ∃ (n : ℕ),
    ∀ (i : 𝒰.I₀),
      Eq (α := (↑Γ(𝒰.X i, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (res i) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(𝒰.X i, ⊤) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) φ :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (s ^ n * g)) :
          (↑Γ(𝒰.X i, ⊤) : Type u))
        (0 : (↑Γ(𝒰.X i, ⊤) : Type u))

Tactic:
have h2 : ∃ n, ∀ i, (res i) (φ (s ^ n * g)) = 0 := by
    choose fn hfn using h1
    refine ⟨Finset.sup Finset.univ fn, fun i ↦ ?_⟩
    rw [map_mul, map_pow, map_mul, map_pow]
    simp only [map_mul, map_pow, map_mul, map_pow] at hfn
    apply pow_mul_eq_zero_of_le (Finset.le_sup (Finset.mem_univ i)) (hfn i)