awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of S))
this :
  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))
inr :
  IsIso (X := (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprodSpec R S) (coprod.inr x))) (Y :=
    (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))
⊢ 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)))

Tactic:
rw [coprodMk_inr, ← this]

Premises used: AlgebraicGeometry.coprodMk_inr
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of S))
this_1 :
  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))
this : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
⊢ IsOpenImmersion.{u} (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of (R × S)))
    (Spec.map (CommRingCat.ofHom (RingHom.snd R S)))

Tactic:
have : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) :=
      IsOpenImmersion.of_isLocalization (0, 1)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of S))
this_1 :
  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))
this_2 : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
this :
  IsOpenImmersion.{u} (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of (R × S)))
    (Spec.map (CommRingCat.ofHom (RingHom.snd R S)))
⊢ IsIso (X := (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprodSpec R S) (coprod.inr x))) (Y :=
    (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))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
rw :
  IsIso (X := (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat))
      (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (coprodSpec R S)))) ∧
    ∀ (x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))),
      IsIso (X := (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprodSpec R S) x))
        (Scheme.Hom.stalkMap (coprodSpec R S) x)
⊢ IsIso (X := Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)) (coprodSpec R S)

Tactic:
rw [isIso_iff_isIso_stalkMap]

Premises used: AlgebraicGeometry.isIso_iff_isIso_stalkMap
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
⊢ IsIso (X := (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat))
      (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (coprodSpec R S)))) ∧
    ∀ (x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))),
      IsIso (X := (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprodSpec R S) x))
        (Scheme.Hom.stalkMap (coprodSpec R S) x)

Tactic:
⟨?_, isIso_stalkMap_coprodSpec R S⟩

Premises used: AlgebraicGeometry.isIso_stalkMap_coprodSpec, And.intro
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
refine :
  IsIso (X := (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (coprodSpec R S))))
⊢ IsIso (X := (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat))
      (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (coprodSpec R S)))) ∧
    ∀ (x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))),
      IsIso (X := (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprodSpec R S) x))
        (Scheme.Hom.stalkMap (coprodSpec R S) x)

Tactic:
refine ⟨?_, isIso_stalkMap_coprodSpec R S⟩
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
h :
  Eq (α :=
    (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat) ⟶
      (↑(Spec (CommRingCat.of (R × S))).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (coprodSpec R S))))
    (Iso.inv
      (TopCat.isoOfHomeo
        (Homeomorph.trans PrimeSpectrum.primeSpectrumProdHomeo
          (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))))
convert_to :
  IsIso.{u, u + 1} (X := (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat)) (Y :=
    (↑(Spec (CommRingCat.of (R × S))).toPresheafedSpace : TopCat))
    (Iso.inv
      (TopCat.isoOfHomeo
        (Homeomorph.trans PrimeSpectrum.primeSpectrumProdHomeo
          (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))))
⊢ IsIso (X := (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (coprodSpec R S))))

Tactic:
convert_to IsIso (TopCat.isoOfHomeo (X := Spec (.of <| R × S)) <|
    PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec <| .of R) (Spec <| .of S))).inv

Premises used: AlgebraicGeometry.Spec, CategoryTheory.IsIso, AlgebraicGeometry.coprodMk, TopCat.isoOfHomeo, CommRingCat.of, Homeomorph.trans, CategoryTheory.Iso.inv, PrimeSpectrum.primeSpectrumProdHomeo
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
h :
  ∀ (x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))),
    Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat)) (Y :=
              (↑(Spec (CommRingCat.of (R × S))).toPresheafedSpace : TopCat))
              (Iso.inv
                (TopCat.isoOfHomeo
                  (Homeomorph.trans PrimeSpectrum.primeSpectrumProdHomeo
                    (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)))))) :
            (a : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))) → ↥(Spec (CommRingCat.of (R × S))))
          x :
        ↥(Spec (CommRingCat.of (R × S))))
⊢ Eq (α :=
    (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat) ⟶
      (↑(Spec (CommRingCat.of (R × S))).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (coprodSpec R S))))
    (Iso.inv
      (TopCat.isoOfHomeo
        (Homeomorph.trans PrimeSpectrum.primeSpectrumProdHomeo
          (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))
⊢ Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat)) (Y :=
            (↑(Spec (CommRingCat.of (R × S))).toPresheafedSpace : TopCat))
            (Iso.inv
              (TopCat.isoOfHomeo
                (Homeomorph.trans PrimeSpectrum.primeSpectrumProdHomeo
                  (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)))))) :
          (a : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))) → ↥(Spec (CommRingCat.of (R × S))))
        x :
      ↥(Spec (CommRingCat.of (R × S))))

Tactic:
coprodSpec_apply R S x

Premises used: AlgebraicGeometry.coprodSpec_apply, PrimeSpectrum.primeSpectrumProdOfSum
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))
⊢ Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat)) (Y :=
            (↑(Spec (CommRingCat.of (R × S))).toPresheafedSpace : TopCat))
            (Iso.inv
              (TopCat.isoOfHomeo
                (Homeomorph.trans PrimeSpectrum.primeSpectrumProdHomeo
                  (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S)))))) :
          (a : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))) → ↥(Spec (CommRingCat.of (R × S))))
        x :
      ↥(Spec (CommRingCat.of (R × S))))

Tactic:
exact coprodSpec_apply R S x

Premises used: AlgebraicGeometry.coprodSpec_apply
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
⊢ IsIso.{u, u + 1} (X := (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat)) (Y :=
    (↑(Spec (CommRingCat.of (R × S))).toPresheafedSpace : TopCat))
    (Iso.inv
      (TopCat.isoOfHomeo
        (Homeomorph.trans PrimeSpectrum.primeSpectrumProdHomeo
          (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCatᵒᵖ
obtain :
  ∀ (R : CommRingCat.{u}),
    IsIso (X := Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj S) (Y := Scheme.Spec.obj (op R ⨿ S))
      (coprodComparison Scheme.Spec (op R) S)
⊢ IsIso (X := Scheme.Spec.obj R ⨿ Scheme.Spec.obj S) (Y := Scheme.Spec.obj (R ⨿ S)) (coprodComparison Scheme.Spec R S)

Tactic:
obtain ⟨R⟩ := R
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
S : CommRingCatᵒᵖ
R : CommRingCat
obtain :
  ∀ (S : CommRingCat.{u}),
    IsIso (X := Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S)) (Y := Scheme.Spec.obj (op R ⨿ op S))
      (coprodComparison Scheme.Spec (op R) (op S))
⊢ IsIso (X := Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj S) (Y := Scheme.Spec.obj (op R ⨿ S))
    (coprodComparison Scheme.Spec (op R) S)

Tactic:
obtain ⟨S⟩ := S
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCat
h₁ :
  CategoryStruct.comp (Y := Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S)) coprod.inl
      (CategoryStruct.comp (Y := Scheme.Spec.obj (op R ⨿ op S))
        (coprodComparison Scheme.Spec (op R) (op S) :
          Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
        (Spec.map
            (CategoryStruct.comp (Y := limit (pair R S))
              (Iso.inv
                (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }))
              (Iso.inv (Iso.unop (opProdIsoCoprod R S)))) :
          Spec (unop (op R ⨿ op S)) ⟶
            Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)) =
    coprod.inl ≫ coprodSpec (↑R : Type u) (↑S : Type u)
h₂ :
  CategoryStruct.comp (Y := Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S)) coprod.inr
      (CategoryStruct.comp (Y := Scheme.Spec.obj (op R ⨿ op S))
        (coprodComparison Scheme.Spec (op R) (op S) :
          Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
        (Spec.map
            (CategoryStruct.comp (Y := limit (pair R S))
              (Iso.inv
                (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }))
              (Iso.inv (Iso.unop (opProdIsoCoprod R S)))) :
          Spec (unop (op R ⨿ op S)) ⟶
            Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)) =
    coprod.inr ≫ coprodSpec (↑R : Type u) (↑S : Type u)
⊢ CategoryStruct.comp (Y := Scheme.Spec.obj (op R ⨿ op S))
      (coprodComparison Scheme.Spec (op R) (op S) :
        Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
      (Spec.map
          (CategoryStruct.comp (Y := limit (pair R S))
            (Iso.inv (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }))
            (Iso.inv (Iso.unop (opProdIsoCoprod R S)))) :
        Spec (unop (op R ⨿ op S)) ⟶
          Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt) =
    coprodSpec (↑R : Type u) (↑S : Type u)

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCat
h₁ :
  Eq (α :=
    Scheme.Spec.obj (op R) ⟶ Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)
    (Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.left }) :
      Spec (unop (op R)) ⟶ Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)
    (Spec.map (CommRingCat.ofHom (RingHom.fst (↑R : Type u) (↑S : Type u))) :
      Spec (CommRingCat.of (↑R : Type u)) ⟶ Spec (CommRingCat.of ((↑R : Type u) × (↑S : Type u))))
⊢ CategoryStruct.comp (Y := Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S)) coprod.inl
      (CategoryStruct.comp (Y := Scheme.Spec.obj (op R ⨿ op S))
        (coprodComparison Scheme.Spec (op R) (op S) :
          Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
        (Spec.map
            (CategoryStruct.comp (Y := limit (pair R S))
              (Iso.inv
                (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }))
              (Iso.inv (Iso.unop (opProdIsoCoprod R S)))) :
          Spec (unop (op R ⨿ op S)) ⟶
            Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)) =
    coprod.inl ≫ coprodSpec (↑R : Type u) (↑S : Type u)

Tactic:
rw [coprodComparison_inl_assoc, coprodSpec, coprod.inl_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inl,
        limit.isoLimitCone_inv_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.coprodComparison_inl_assoc, CategoryTheory.Limits.opProdIsoCoprod_inv_inl, CategoryTheory.Limits.coprod.inl_desc, CategoryTheory.Iso.unop_inv, AlgebraicGeometry.coprodSpec, AlgebraicGeometry.Spec.map_comp, CategoryTheory.Limits.limit.isoLimitCone_inv_π, AlgebraicGeometry.Scheme.Spec_map
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCat
⊢ Eq (α :=
    Scheme.Spec.obj (op R) ⟶ Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)
    (Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.left }) :
      Spec (unop (op R)) ⟶ Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)
    (Spec.map (CommRingCat.ofHom (RingHom.fst (↑R : Type u) (↑S : Type u))) :
      Spec (CommRingCat.of (↑R : Type u)) ⟶ Spec (CommRingCat.of ((↑R : Type u) × (↑S : Type u))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCat
h₂ :
  Eq (α :=
    Scheme.Spec.obj (op S) ⟶ Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)
    (Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.right }) :
      Spec (unop (op S)) ⟶ Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)
    (Spec.map (CommRingCat.ofHom (RingHom.snd (↑R : Type u) (↑S : Type u))) :
      Spec (CommRingCat.of (↑S : Type u)) ⟶ Spec (CommRingCat.of ((↑R : Type u) × (↑S : Type u))))
⊢ CategoryStruct.comp (Y := Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S)) coprod.inr
      (CategoryStruct.comp (Y := Scheme.Spec.obj (op R ⨿ op S))
        (coprodComparison Scheme.Spec (op R) (op S) :
          Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
        (Spec.map
            (CategoryStruct.comp (Y := limit (pair R S))
              (Iso.inv
                (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }))
              (Iso.inv (Iso.unop (opProdIsoCoprod R S)))) :
          Spec (unop (op R ⨿ op S)) ⟶
            Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)) =
    coprod.inr ≫ coprodSpec (↑R : Type u) (↑S : Type u)

Tactic:
rw [coprodComparison_inr_assoc, coprodSpec, coprod.inr_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inr,
        limit.isoLimitCone_inv_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.coprodComparison_inr_assoc, CategoryTheory.Iso.unop_inv, AlgebraicGeometry.coprodSpec, AlgebraicGeometry.Spec.map_comp, CategoryTheory.Limits.opProdIsoCoprod_inv_inr, CategoryTheory.Limits.limit.isoLimitCone_inv_π, CategoryTheory.Limits.coprod.inr_desc, AlgebraicGeometry.Scheme.Spec_map
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCat
⊢ Eq (α :=
    Scheme.Spec.obj (op S) ⟶ Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)
    (Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.right }) :
      Spec (unop (op S)) ⟶ Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt)
    (Spec.map (CommRingCat.ofHom (RingHom.snd (↑R : Type u) (↑S : Type u))) :
      Spec (CommRingCat.of (↑S : Type u)) ⟶ Spec (CommRingCat.of ((↑R : Type u) × (↑S : Type u))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCat
⊢ CategoryStruct.comp (Y := Scheme.Spec.obj (op R ⨿ op S))
      (coprodComparison Scheme.Spec (op R) (op S) :
        Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
      (Spec.map
          (CategoryStruct.comp (Y := limit (pair R S))
            (Iso.inv (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }))
            (Iso.inv (Iso.unop (opProdIsoCoprod R S)))) :
        Spec (unop (op R ⨿ op S)) ⟶
          Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt) =
    coprodSpec (↑R : Type u) (↑S : Type u)

Tactic:
have : coprodComparison Scheme.Spec (.op R) (.op S) ≫ (Spec.map
    ((limit.isoLimitCone ⟨_, CommRingCat.prodFanIsLimit R S⟩).inv ≫
      (opProdIsoCoprod R S).unop.inv)) = coprodSpec R S := by
    ext1
    · rw [coprodComparison_inl_assoc, coprodSpec, coprod.inl_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inl,
        limit.isoLimitCone_inv_π]
      rfl
    · rw [coprodComparison_inr_assoc, coprodSpec, coprod.inr_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inr,
        limit.isoLimitCone_inv_π]
      rfl