-- 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
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)))))
⊢ 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 (α := Set (PrimeSpectrum R))
  (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
    (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
  (↑C : BasicConstructibleSetData R).toSet
Tactic: trans comap (Ideal.Quotient.mk I) '' (Set.range (comap (algebraMap _ (Localization.Away f))))