-- Mathlib/AlgebraicGeometry/Limits.lean
lemma coprodSpec_coprodMk (x) :
    (coprodSpec R S).base (coprodMk _ _ x) = (PrimeSpectrum.primeSpectrumProd R S).symm x

Proof state:
case asIdeal.inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
⊢ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal = x.asIdeal.prod ⊤

Tactic:
ext

Result:
case asIdeal.inl.h
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
x✝ : ↑(CommRingCat.of R) × S
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal ↔ x✝ ∈ x.asIdeal.prod ⊤

Proof state:
case asIdeal.inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
⊢ ((ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (RingHom.snd R S))).base) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal

Tactic:
show Ideal.comap _ _ = Ideal.prod ⊤ x.asIdeal

Result:
case asIdeal.inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
⊢ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal = ⊤.prod x.asIdeal

Proof state:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace ⊕ ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
⊢ (ConcreteCategory.hom (coprodSpec R S).base) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) x) =
    (PrimeSpectrum.primeSpectrumProd R S).symm x

Tactic:
apply PrimeSpectrum.ext

Result:
case asIdeal
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace ⊕ ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
⊢ ((ConcreteCategory.hom (coprodSpec R S).base)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) x)).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm x).asIdeal

Proof state:
case asIdeal.inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
⊢ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal = ⊤.prod x.asIdeal

Tactic:
ext

Result:
case asIdeal.inr.h
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
x✝ : R × ↑(CommRingCat.of S)
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal ↔ x✝ ∈ ⊤.prod x.asIdeal

Proof state:
case asIdeal.inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
⊢ ((ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (RingHom.fst R S))).base) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal

Tactic:
show Ideal.comap _ _ = x.asIdeal.prod ⊤

Result:
case asIdeal.inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
⊢ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal = x.asIdeal.prod ⊤

Proof state:
case asIdeal.inr.h
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
x✝ : R × ↑(CommRingCat.of S)
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal ↔ x✝ ∈ ⊤.prod x.asIdeal

Tactic:
simp [Ideal.prod, CommRingCat.ofHom]

Result:
no goals

Proof state:
case asIdeal
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace ⊕ ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
⊢ ((ConcreteCategory.hom (coprodSpec R S).base)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) x)).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm x).asIdeal

Tactic:
obtain (x | x) := x <;>
  simp only [coprodMk_inl, coprodMk_inr, ← Scheme.comp_base_apply,
    coprodSpec, coprod.inl_desc, coprod.inr_desc]

Result:
case asIdeal.inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
⊢ ((ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (RingHom.fst R S))).base) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal

case asIdeal.inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
⊢ ((ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (RingHom.snd R S))).base) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal

Proof state:
case asIdeal.inl.h
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
x✝ : ↑(CommRingCat.of R) × S
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal ↔ x✝ ∈ x.asIdeal.prod ⊤

Tactic:
simp [Ideal.prod, CommRingCat.ofHom]

Result:
no goals