-- 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
⊢ 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)
have 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
Tactic: congr! with _ _ C