awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
U : (X ⨿ Y).Opens
⊢ (coprodPresheafObjIso U).hom ≫ prod.fst = Hom.app coprod.inl U

Tactic:
simp [coprodPresheafObjIso, Hom.appIso_hom, ← Functor.map_comp, Subsingleton.elim _ (𝟙 _)]

Premises used: CategoryTheory.CategoryStruct.id, AlgebraicGeometry.Scheme.Hom.appIso_hom, CategoryTheory.Functor.map_comp, Subsingleton.elim, AlgebraicGeometry.Scheme.coprodPresheafObjIso
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
U : (X ⨿ Y).Opens
⊢ (coprodPresheafObjIso U).hom ≫ prod.snd = Hom.app coprod.inr U

Tactic:
simp [coprodPresheafObjIso, Hom.appIso_hom, ← Functor.map_comp, Subsingleton.elim _ (𝟙 _)]

Premises used: CategoryTheory.CategoryStruct.id, AlgebraicGeometry.Scheme.Hom.appIso_hom, CategoryTheory.Functor.map_comp, Subsingleton.elim, AlgebraicGeometry.Scheme.coprodPresheafObjIso
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
⊢ Eq (α := Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of (R × S))) (coprod.inl ≫ coprodSpec R S)
    (Spec.map (CommRingCat.ofHom (RingHom.fst R S)))

Tactic:
coprod.inl_desc _ _

Premises used: CategoryTheory.Limits.coprod.inl_desc
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
⊢ Eq (α := Spec (CommRingCat.of S) ⟶ Spec (CommRingCat.of (R × S))) (coprod.inr ≫ coprodSpec R S)
    (Spec.map (CommRingCat.ofHom (RingHom.snd R S)))

Tactic:
coprod.inr_desc _ _

Premises used: CategoryTheory.Limits.coprod.inr_desc
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))
asIdeal :
  Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((coprodSpec R S)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
            (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
          x)))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        x))
⊢ Eq (α := ↥(Spec (CommRingCat.of (R × S))))
    ((coprodSpec R S)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
            (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
          x) :
      ↥(Spec (CommRingCat.of (R × S))))
    ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        x :
      PrimeSpectrum (R × S))

Tactic:
apply PrimeSpectrum.ext

Premises used: PrimeSpectrum.ext
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))
asIdeal :
  ∀ (x : ↥(Spec (CommRingCat.of R))),
    Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
      (PrimeSpectrum.asIdeal
        ((coprodSpec R S)
          ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
              (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
                ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
            (Sum.inl x))))
      (PrimeSpectrum.asIdeal
        ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
            (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
          (Sum.inl x)))
asIdeal₁ :
  ∀ (x : ↥(Spec (CommRingCat.of S))),
    Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
      (PrimeSpectrum.asIdeal
        ((coprodSpec R S)
          ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
              (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
                ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
            (Sum.inr x))))
      (PrimeSpectrum.asIdeal
        ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
            (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
          (Sum.inr x)))
⊢ Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((coprodSpec R S)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
            (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
          x)))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        x))

Tactic:
obtain (x | x) := x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R))
asIdeal :
  Eq.{u + 1} (α := Ideal (R × S)) (PrimeSpectrum.asIdeal ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl x)))
⊢ Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((coprodSpec R S)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
            (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
          (Sum.inl x))))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl x)))

Tactic:
simp only [coprodMk_inl, coprodMk_inr, ← Scheme.Hom.comp_apply,
      coprodSpec, coprod.inl_desc, coprod.inr_desc]

Premises used: AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.coprod.inl_desc, AlgebraicGeometry.coprodSpec, CategoryTheory.Limits.coprod.inr_desc, AlgebraicGeometry.coprodMk_inr
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of S))
asIdeal :
  Eq.{u + 1} (α := Ideal (R × S)) (PrimeSpectrum.asIdeal ((Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr x)))
⊢ Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((coprodSpec R S)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
            (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
          (Sum.inr x))))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr x)))

Tactic:
simp only [coprodMk_inl, coprodMk_inr, ← Scheme.Hom.comp_apply,
      coprodSpec, coprod.inl_desc, coprod.inr_desc]

Premises used: AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.coprod.inl_desc, AlgebraicGeometry.coprodSpec, CategoryTheory.Limits.coprod.inr_desc, AlgebraicGeometry.coprodMk_inr
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R))
asIdeal :
  Eq (α := Ideal ((↑(CommRingCat.of R) : Type u) × S))
    (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of R) : Type u))
      (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal)
    (x.asIdeal.prod ⊤)
⊢ Eq.{u + 1} (α := Ideal (R × S)) (PrimeSpectrum.asIdeal ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl x)))

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

Premises used: Ideal.prod, Ideal.comap, Top.top, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R))
asIdeal :
  ∀ (x_1 : (↑(CommRingCat.of R) : Type u) × S),
    Membership.mem (γ := Ideal ((↑(CommRingCat.of R) : Type u) × S))
        (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of R) : Type u))
          (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal)
        x_1 ↔
      Membership.mem (γ := Ideal ((↑(CommRingCat.of R) : Type u) × S)) (x.asIdeal.prod ⊤) x_1
⊢ Eq (α := Ideal ((↑(CommRingCat.of R) : Type u) × S))
    (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of R) : Type u))
      (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal)
    (x.asIdeal.prod ⊤)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R))
x_1 : (↑(CommRingCat.of R) : Type u) × S
⊢ Membership.mem (γ := Ideal ((↑(CommRingCat.of R) : Type u) × S))
      (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of R) : Type u))
        (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal)
      x_1 ↔
    Membership.mem (γ := Ideal ((↑(CommRingCat.of R) : Type u) × S)) (x.asIdeal.prod ⊤) x_1

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

Premises used: CommRingCat.ofHom, Ideal.prod
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of S))
asIdeal :
  Eq (α := Ideal (R × (↑(CommRingCat.of S) : Type u)))
    (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
      (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal)
    (Ideal.prod ⊤ x.asIdeal)
⊢ Eq.{u + 1} (α := Ideal (R × S)) (PrimeSpectrum.asIdeal ((Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr x)))

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

Premises used: Ideal.prod, Ideal.comap, Top.top, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of S))
asIdeal :
  ∀ (x_1 : R × (↑(CommRingCat.of S) : Type u)),
    Membership.mem (γ := Ideal (R × (↑(CommRingCat.of S) : Type u)))
        (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
          (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal)
        x_1 ↔
      Membership.mem (γ := Ideal (R × (↑(CommRingCat.of S) : Type u))) (Ideal.prod ⊤ x.asIdeal) x_1
⊢ Eq (α := Ideal (R × (↑(CommRingCat.of S) : Type u)))
    (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
      (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal)
    (Ideal.prod ⊤ x.asIdeal)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of S))
x_1 : R × (↑(CommRingCat.of S) : Type u)
⊢ Membership.mem (γ := Ideal (R × (↑(CommRingCat.of S) : Type u)))
      (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
        (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal)
      x_1 ↔
    Membership.mem (γ := Ideal (R × (↑(CommRingCat.of S) : Type u))) (Ideal.prod ⊤ x.asIdeal) x_1

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

Premises used: CommRingCat.ofHom, Ideal.prod
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))
rw :
  Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
    ((coprodSpec R S)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
            (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
          ((Homeomorph.symm (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) :
                (a : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))) →
                  ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S)))
              x :
            ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S)))) :
      ↥(Spec (CommRingCat.of (R × S))))
rw₁ rw₂ :
  Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
    ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
⊢ Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
    ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        ((Homeomorph.symm (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) :
            (a : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S)))
          x) :
      PrimeSpectrum (R × S))

Tactic:
rw [← coprodSpec_coprodMk, Homeomorph.apply_symm_apply]

Premises used: AlgebraicGeometry.coprodSpec_coprodMk, Homeomorph.apply_symm_apply
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))
inl :
  ∀ (x : ↥(Spec (CommRingCat.of R))),
    IsIso (X :=
      (Spec (CommRingCat.of (R × S))).presheaf.stalk
        ((coprodSpec R S)
          ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
              (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
                ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
            (Sum.inl x))))
      (Scheme.Hom.stalkMap (coprodSpec R S)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
            (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
          (Sum.inl x)))
inr :
  ∀ (x : ↥(Spec (CommRingCat.of S))),
    IsIso (X :=
      (Spec (CommRingCat.of (R × S))).presheaf.stalk
        ((coprodSpec R S)
          ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
              (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
                ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
            (Sum.inr x))))
      (Scheme.Hom.stalkMap (coprodSpec R S)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
            (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
          (Sum.inr x)))
⊢ IsIso (X := (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprodSpec R S) x))
    (Scheme.Hom.stalkMap (coprodSpec R S) x)

Tactic:
obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x

Premises used: AlgebraicGeometry.coprodMk, Homeomorph.surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := Scheme.Hom.stalkMap_comp coprod.inl (coprodSpec R S) x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R))
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α :=
    (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprod.inl ≫ coprodSpec R S) x) ⟶
      (Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).presheaf.stalk (coprod.inl x))
    (CategoryStruct.comp (Y :=
        (Spec (CommRingCat.of (R × S))).presheaf.stalk ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
        (Iso.hom ((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯))
        (Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))
    (Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x))

Tactic:
rw [← IsIso.comp_inv_eq,
      Scheme.Hom.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inl R S)] at this

Premises used: AlgebraicGeometry.Spec.map, CategoryTheory.IsIso.comp_inv_eq, AlgebraicGeometry.coprodSpec_inl, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R))
this :
  Eq (α :=
    (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprod.inl ≫ coprodSpec R S) x) ⟶
      (Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).presheaf.stalk (coprod.inl x))
    (CategoryStruct.comp (Y :=
        (Spec (CommRingCat.of (R × S))).presheaf.stalk ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
        (Iso.hom ((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯))
        (Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))
    (Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x))
inl :
  IsIso (X := (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprodSpec R S) (coprod.inl x))) (Y :=
    (Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).presheaf.stalk (coprod.inl x))
    (CategoryStruct.comp (Y :=
        (Spec (CommRingCat.of (R × S))).presheaf.stalk ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
        (Iso.hom ((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯))
        (Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))
⊢ IsIso (X :=
    (Spec (CommRingCat.of (R × S))).presheaf.stalk
      ((coprodSpec R S)
        ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
            (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
              ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
          (Sum.inl x))))
    (Scheme.Hom.stalkMap (coprodSpec R S)
      ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)) :
          (a : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) →
            ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)))
        (Sum.inl x)))

Tactic:
rw [coprodMk_inl, ← this]

Premises used: AlgebraicGeometry.coprodMk_inl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R))
this_1 :
  Eq (α :=
    (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprod.inl ≫ coprodSpec R S) x) ⟶
      (Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).presheaf.stalk (coprod.inl x))
    (CategoryStruct.comp (Y :=
        (Spec (CommRingCat.of (R × S))).presheaf.stalk ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
        (Iso.hom ((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯))
        (Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))
    (Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x))
this : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
⊢ IsOpenImmersion.{u} (X := Spec (CommRingCat.of R)) (Y := Spec (CommRingCat.of (R × S)))
    (Spec.map (CommRingCat.ofHom (RingHom.fst R S)))

Tactic:
have : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) :=
      IsOpenImmersion.of_isLocalization (1, 0)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R))
this_1 :
  Eq (α :=
    (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprod.inl ≫ coprodSpec R S) x) ⟶
      (Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).presheaf.stalk (coprod.inl x))
    (CategoryStruct.comp (Y :=
        (Spec (CommRingCat.of (R × S))).presheaf.stalk ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
        (Iso.hom ((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯))
        (Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))
    (Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x))
this_2 : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
this :
  IsOpenImmersion.{u} (X := Spec (CommRingCat.of R)) (Y := Spec (CommRingCat.of (R × S)))
    (Spec.map (CommRingCat.ofHom (RingHom.fst R S)))
⊢ IsIso (X := (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprodSpec R S) (coprod.inl x))) (Y :=
    (Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).presheaf.stalk (coprod.inl x))
    (CategoryStruct.comp (Y :=
        (Spec (CommRingCat.of (R × S))).presheaf.stalk ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
        (Iso.hom ((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯))
        (Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of S))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := Scheme.Hom.stalkMap_comp coprod.inr (coprodSpec R S) x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of S))
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α :=
    (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprod.inr ≫ coprodSpec R S) x) ⟶
      (Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).presheaf.stalk (coprod.inr x))
    (CategoryStruct.comp (Y :=
        (Spec (CommRingCat.of (R × S))).presheaf.stalk ((Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x))
        (Iso.hom ((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯))
        (Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inr x))
    (Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x))

Tactic:
rw [← IsIso.comp_inv_eq,
      Scheme.Hom.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inr R S)] at this

Premises used: AlgebraicGeometry.coprodSpec_inr, AlgebraicGeometry.Spec.map, CategoryTheory.IsIso.comp_inv_eq, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom