awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
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)
⊢ 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))
have this₁ : 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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
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)))
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
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)
⊢ 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)))
have 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 sorry))
      (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
⊢ 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)))
have 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 sorry))
      (Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
    inv (Scheme.Hom.stalkMap coprod.inr x))
Tactic: rw [coprodMk_inr, ← this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
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)
⊢ 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))
have this₁ : 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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)) (coprodSpec R S)
have 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)
Tactic: rw [isIso_iff_isIso_stalkMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)
have 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))))
Tactic: refine ⟨?_, isIso_stalkMap_coprodSpec R S⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))))
have 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))))))
Tactic: convert_to IsIso (TopCat.isoOfHomeo (X := Spec (.of <| R × S)) <|
    PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec <| .of R) (Spec <| .of S))).inv
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))))))
⊢ IsIso (X := (↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (coprodSpec R S))))
have 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))))))
Tactic: convert_to IsIso (TopCat.isoOfHomeo (X := Spec (.of <| R × S)) <|
    PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec <| .of R) (Spec <| .of S))).inv
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing 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))))))
have 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))))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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ᵒᵖ
⊢ IsIso (X := Scheme.Spec.obj R ⨿ Scheme.Spec.obj S) (Y := Scheme.Spec.obj (R ⨿ S)) (coprodComparison Scheme.Spec R S)
have 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)
Tactic: obtain ⟨R⟩ := R
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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
⊢ IsIso (X := Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj S) (Y := Scheme.Spec.obj (op R ⨿ S))
    (coprodComparison Scheme.Spec (op R) S)
have 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))
Tactic: obtain ⟨S⟩ := S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)
have 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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)
⊢ 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)
have 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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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) ⨿ 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)
have 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))))
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_π]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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) ⨿ 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)
have 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))))
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_π]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
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
⊢ 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))
have this : 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