-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
simp_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))))))))
    (⋃ (x : (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)), (↑x : BasicConstructibleSetData R).toSet)
⊢ 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)

Tactic:
simp_rw [← Finset.mem_coe, Set.biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion, Finset.mem_coe