-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
h :
  ↥s = (↑(↑s : Set (BasicConstructibleSetData R)) : Type u) →
    ∀ (C : ↥s),
      Eq (α := Set (PrimeSpectrum R))
        (Set.range (ι :=
          PrimeSpectrum
            (Localization.Away (M :=
              HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)))
              ((Ideal.Quotient.mk (Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)) :
                    (a : R) → R ⧸ Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g))
                  (↑C : BasicConstructibleSetData R).f :
                HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑C : 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))))
                C)
              (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 : 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))))))))
    (⋃ (x : (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)), (↑x : BasicConstructibleSetData R).toSet)

Tactic:
congr! with _ _ C