-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
e_2 : ↥s = (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)
f : R ⧸ I := (Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑C : BasicConstructibleSetData R).f
rw :
  Eq (α := Set (PrimeSpectrum R)) (comap (Ideal.Quotient.mk I) '' (↑(basicOpen f) : Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₁ :
  Eq (α := Set (PrimeSpectrum R))
    (comap (Ideal.Quotient.mk I) ''
      (↑((TopologicalSpace.Opens.comap
                  { toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ :
                    C(PrimeSpectrum (R ⧸ I), PrimeSpectrum R) } :
                (a : TopologicalSpace.Opens (PrimeSpectrum R)) → TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I)))
              (basicOpen (↑C : BasicConstructibleSetData R).f) :
            TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I))) :
        Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₂ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      ((⇑{ toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ } :
          (a : PrimeSpectrum (R ⧸ I)) → PrimeSpectrum R) ⁻¹'
        (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
    (↑C : BasicConstructibleSetData R).toSet
rw₃ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (comap (Ideal.Quotient.mk I) ⁻¹' (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
    (↑C : BasicConstructibleSetData R).toSet
rw₄ :
  (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
      Set.range (ι := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I)) =
    (↑C : BasicConstructibleSetData R).toSet
rw₅ :
  (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
      zeroLocus (↑(RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)) : Set R) =
    (↑C : BasicConstructibleSetData R).toSet
rw₆ :
  (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
      zeroLocus (↑(RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)) : Set R) =
    zeroLocus (Set.range (↑C : BasicConstructibleSetData R).g) \ zeroLocus {(↑C : BasicConstructibleSetData R).f}
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
    (↑C : BasicConstructibleSetData R).toSet
have rw₇ : (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
    zeroLocus (↑(RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)) : Set R) =
  (zeroLocus {(↑C : BasicConstructibleSetData R).f})ᶜ ∩ zeroLocus (Set.range (↑C : BasicConstructibleSetData R).g)
Tactic: rw [localization_away_comap_range _ f, ← comap_basicOpen, TopologicalSpace.Opens.coe_comap,
      ContinuousMap.coe_mk, Set.image_preimage_eq_inter_range,
      range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective, BasicConstructibleSetData.toSet,
      Set.diff_eq_compl_inter, basicOpen_eq_zeroLocus_compl, Ideal.mk_ker, zeroLocus_span]