∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (φ : S →+* T) (ψ : R →+* S) (C : PrimeSpectrum.BasicConstructibleSetData R),
  PrimeSpectrum.BasicConstructibleSetData.map (φ.comp ψ) C =
    PrimeSpectrum.BasicConstructibleSetData.map φ (PrimeSpectrum.BasicConstructibleSetData.map ψ C)