case mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
asIdeal✝ : Ideal R
IsPrime✝ : Ideal.IsPrime asIdeal✝
⊢ (↑(primeSpectrumProd R S).symm (Sum.inl { asIdeal := asIdeal✝, IsPrime := IsPrime✝ })).asIdeal =
    Ideal.prod { asIdeal := asIdeal✝, IsPrime := IsPrime✝ }.asIdeal ⊤
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
⊢ (↑(primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = Ideal.prod x.asIdeal ⊤
cases x
no goals
case mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
asIdeal✝ : Ideal R
IsPrime✝ : Ideal.IsPrime asIdeal✝
⊢ (↑(primeSpectrumProd R S).symm (Sum.inl { asIdeal := asIdeal✝, IsPrime := IsPrime✝ })).asIdeal =
    Ideal.prod { asIdeal := asIdeal✝, IsPrime := IsPrime✝ }.asIdeal ⊤
rfl