-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
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)))))
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
⊢ 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:
trans comap (Ideal.Quotient.mk I) '' (Set.range (comap (algebraMap _ (Localization.Away f))))

Premises used: Algebra.algebraMap, Ideal.Quotient.mk, Localization.Away, Set.range, PrimeSpectrum.comap