-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
a :
  Membership.mem (α := ↥Y)
    (Y.zeroLocus
        (↑((ker f).ideal
              (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens)
                (𝒰.f i ''ᵁ
                  (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦
                        Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤ ⋯) :
                    (𝒰.X i).Opens))
                ⋯)) :
          Set (↑Γ(Y, (↑⟨𝒰.f i ''ᵁ (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens), ⋯⟩ : Y.Opens)) : Type u)) ∩
      Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))
    ((𝒰.f i) x : ↥Y)
a₁ :
  Function.Surjective (α :=
    (↑Γ(𝒰.X i,
          (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦ Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤
                ⋯) :
            (𝒰.X i).Opens)) :
      Type u))
    (β :=
    (↑Γ(Y,
          𝒰.f i ''ᵁ
            (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦ Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x)
                  ⊤ ⋯) :
              (𝒰.X i).Opens)) :
      Type u))
    (⇑(CommRingCat.Hom.hom
          (Iso.inv
            (appIso (𝒰.f i)
              (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦
                    Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤ ⋯) :
                (𝒰.X i).Opens)))) :
      (a : (↑Γ(𝒰.X i, (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens)) : Type u)) → (↑Γ(Y, 𝒰.f i ''ᵁ (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens)) : Type u))
a₂ :
  IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f
⊢ x ∈
    (𝒰.X i).zeroLocus
      (↑((ker (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)).ideal
            (Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦ Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤
              ⋯)) :
        Set (↑Γ(𝒰.X i, (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens)) : Type u))

Tactic:
rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
          ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
            ((𝒰.pullback₁ f).f i) (𝒰.f i),
          Ideal.coe_comap, Set.image_preimage_eq]

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, Set.image_preimage_eq, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Ideal.coe_comap, Topology.IsEmbedding.injective, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.image_zeroLocus, Function.Injective.mem_set_image, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover