-- 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
⊢ 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 := IsLocalization.away_snd (R := R) (S := S)

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
⊢ 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
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))

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

Result:
case intro.inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace
this :
  Scheme.Hom.stalkMap (coprod.inr ≫ coprodSpec R S) x =
    Scheme.Hom.stalkMap (coprodSpec R S) ((ConcreteCategory.hom coprod.inr.base) x) ≫ Scheme.Hom.stalkMap coprod.inr x
⊢ 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 :
  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)))

Tactic:
rw [← IsIso.comp_inv_eq, Scheme.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inl R S)] at 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
    (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 :
  Scheme.Hom.stalkMap (coprod.inr ≫ coprodSpec R S) x =
    Scheme.Hom.stalkMap (coprodSpec R S) ((ConcreteCategory.hom coprod.inr.base) x) ≫ Scheme.Hom.stalkMap coprod.inr x
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))

Tactic:
rw [← IsIso.comp_inv_eq, Scheme.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inr R S)] at 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
    (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)
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))

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

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
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.fst R S)))
⊢ 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
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
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.fst R S)))
⊢ 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:
infer_instance

Result:
no goals