-- 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
⊢ 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
have trans : Eq.{u + 1} (α := 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))))))))
  (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
    (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
Tactic: trans comap (Ideal.Quotient.mk I) '' (Set.range (comap (algebraMap _ (Localization.Away f))))