-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I_1 : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, (↑U : X.Opens)))
I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (PrimeSpectrum.zeroLocus
        ((⇑(CommRingCat.Hom.hom F) : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) ''
          (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
a :
  ∀
    (hx :
      Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (PrimeSpectrum.vanishingIdeal
          (PrimeSpectrum.zeroLocus
            (↑(Ideal.span
                  ((⇑(CommRingCat.Hom.hom F) :
                      (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) ''
                    (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))) :
              Set (↑Γ(X, X.basicOpen f) : Type u))))
        x)
    (hI : I.IsRadical) (e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))),
    Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
        (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
      x
a₁ :
  ∀
    (hx :
      Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (PrimeSpectrum.vanishingIdeal
          (PrimeSpectrum.zeroLocus (↑(Ideal.map (CommRingCat.Hom.hom F) I) : Set (↑Γ(X, X.basicOpen f) : Type u))))
        x)
    (hI : I.IsRadical) (e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))),
    Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
        (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
      x
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
have a₂ : ∀
  (hx :
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u)) (Ideal.radical (Ideal.map (CommRingCat.Hom.hom F) I)) x)
  (hI : I.IsRadical) (e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))),
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op))
      (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
Tactic: rwa [← PrimeSpectrum.zeroLocus_span, ← Ideal.map, vanishingIdeal_zeroLocus_eq_radical,
          ← RingHom.algebraMap_toAlgebra (X.presheaf.map _).hom,
          ← IsLocalization.map_radical (.powers f), ← vanishingIdeal_zeroLocus_eq_radical] at hx
Cleared hypotheses: hx, hI, e