-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
rw :
  Eq.{u + 1} (α := Set (PrimeSpectrum R))
    (⋃ (i : ↥s),
      Set.range (ι :=
        PrimeSpectrum
          (Localization.Away (M :=
            HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
            ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                  (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                (↑i : BasicConstructibleSetData R).f :
              HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))))
        (comap
          (@RingHom.comp _
            ((i : ↥s) →
              Localization.Away (M :=
                HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
                ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                      (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                    (↑i : BasicConstructibleSetData R).f :
                  HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))))
            _ _
            (Pi.nonAssocSemiring (f := fun (i : ↥s) ↦
              Localization.Away (M :=
                HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
                ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                      (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                    (↑i : BasicConstructibleSetData R).f :
                  HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))))
            _
            (Pi.evalRingHom
              (fun (i : ↥s) ↦
                Localization.Away (M :=
                  HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
                  ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                        (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                      (↑i : BasicConstructibleSetData R).f :
                    HasQuotient.Quotient R (B := Ideal R)
                      (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))))
              i)
            (algebraMap R
              ((i : ↥s) →
                Localization.Away (M :=
                  HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
                  ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                        (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                      (↑i : BasicConstructibleSetData R).f :
                    HasQuotient.Quotient R (B := Ideal R)
                      (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))))))))
    (⋃ C ∈ s, C.toSet)
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.range (ι :=
      PrimeSpectrum
        ((i : ↥s) →
          Localization.Away (M :=
            HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
            ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                  (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                (↑i : BasicConstructibleSetData R).f :
              HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))))
      (comap
        (algebraMap R
          ((i : ↥s) →
            Localization.Away (M :=
              HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
              ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                    (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                  (↑i : BasicConstructibleSetData R).f :
                HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))))))
    s.toSet

Tactic:
rw [← iUnion_range_comap_comp_evalRingHom, ConstructibleSetData.toSet]

Premises used: PrimeSpectrum.iUnion_range_comap_comp_evalRingHom, PrimeSpectrum.ConstructibleSetData.toSet