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

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

Tactic:
have : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) :=
  IsOpenImmersion.of_isLocalization (0, 1)

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

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

Tactic:
infer_instance

Result:
no goals

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
    ((((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:
letI := (RingHom.fst R S).toAlgebra

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
⊢ 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:
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)))

Tactic:
have := Scheme.stalkMap_comp coprod.inl (coprodSpec R S) x

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

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

Tactic:
rw [coprodMk_inr, ← this]

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

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

Tactic:
letI := (RingHom.snd R S).toAlgebra

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