-- Mathlib/AlgebraicGeometry/Limits.lean
lemma isIso_stalkMap_coprodSpec (x) :
    IsIso ((coprodSpec R S).stalkMap x)

Proof state:
case intro.inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
this✝ :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        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) ((ConcreteCategory.hom coprod.inl.base) x)
this : Algebra (R × S) R := (RingHom.fst R S).toAlgebra
⊢ IsIso
    ((((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))

Tactic:
have := IsLocalization.away_fst (R := R) (S := S)

Result:
case intro.inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
this✝¹ :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        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) ((ConcreteCategory.hom coprod.inl.base) x)
this✝ : Algebra (R × S) R := (RingHom.fst R S).toAlgebra
this : IsLocalization.Away (1, 0) R
⊢ IsIso
    ((((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))

Proof state:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace
⊢ IsIso (Scheme.Hom.stalkMap (coprodSpec R S) x)

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

Result:
case intro.inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x)))

case intro.inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))

Proof state:
case intro.inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
this :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        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) ((ConcreteCategory.hom coprod.inl.base) x)
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x)))

Tactic:
rw [coprodMk_inl, ← this]

Result:
case intro.inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
this :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        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) ((ConcreteCategory.hom coprod.inl.base) x)
⊢ IsIso
    ((((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))