awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
⊢ Hom.opensRange ι₁ ⊓ U ⊔ Hom.opensRange ι₂ ⊓ U = U
have rw : (Hom.opensRange ι₁ ⊔ Hom.opensRange ι₂) ⊓ U = U
Tactic: rw [← inf_sup_right, (isCompl_opensRange_inl_inr X Y).sup_eq_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
rw : (Hom.opensRange ι₁ ⊔ Hom.opensRange ι₂) ⊓ U = U
⊢ Hom.opensRange ι₁ ⊓ U ⊔ Hom.opensRange ι₂ ⊓ U = U
have rw₁ : ⊤ ⊓ U = U
Tactic: rw [← inf_sup_right, (isCompl_opensRange_inl_inr X Y).sup_eq_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
rw : (Hom.opensRange ι₁ ⊔ Hom.opensRange ι₂) ⊓ U = U
rw₁ : ⊤ ⊓ U = U
⊢ Hom.opensRange ι₁ ⊓ U ⊔ Hom.opensRange ι₂ ⊓ U = U
have rw₂ : U = U
Tactic: rw [← inf_sup_right, (isCompl_opensRange_inl_inr X Y).sup_eq_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
h₁ : ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
⊢ ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊓ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = ⊥
have simp_rw : Hom.opensRange ι₁ ⊓ U ⊓ (Hom.opensRange ι₂ ⊓ U) = ⊥
Tactic: simp_rw [Scheme.Hom.image_preimage_eq_opensRange_inf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
h₁ : ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
⊢ Hom.opensRange ι₁ ⊓ U ⊓ (Hom.opensRange ι₂ ⊓ U) = ⊥
have rw : Hom.opensRange ι₁ ⊓ Hom.opensRange ι₂ ⊓ U = ⊥
Tactic: rw [← inf_inf_distrib_right, (isCompl_opensRange_inl_inr X Y).inf_eq_bot, bot_inf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
h₁ : ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
rw : Hom.opensRange ι₁ ⊓ Hom.opensRange ι₂ ⊓ U = ⊥
⊢ Hom.opensRange ι₁ ⊓ U ⊓ (Hom.opensRange ι₂ ⊓ U) = ⊥
have rw₁ : ⊥ ⊓ U = ⊥
Tactic: rw [← inf_inf_distrib_right, (isCompl_opensRange_inl_inr X Y).inf_eq_bot, bot_inf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
h₁ : ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
rw : Hom.opensRange ι₁ ⊓ Hom.opensRange ι₂ ⊓ U = ⊥
rw₁ : ⊥ ⊓ U = ⊥
⊢ Hom.opensRange ι₁ ⊓ U ⊓ (Hom.opensRange ι₂ ⊓ U) = ⊥
have rw₂ : Eq.{u + 1} (α := (X ⨿ Y).Opens) ⊥ ⊥
Tactic: rw [← inf_inf_distrib_right, (isCompl_opensRange_inl_inr X Y).inf_eq_bot, bot_inf_eq]
-- 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 R)) ⊕ ↥(Spec (CommRingCat.of S))
⊢ Eq (α := ↥(Spec (CommRingCat.of (R × S))))
    ((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)))
          x) :
      ↥(Spec (CommRingCat.of (R × S))))
    ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        x :
      PrimeSpectrum (R × S))
have asIdeal : Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
  (PrimeSpectrum.asIdeal
    ((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)))
        x)))
  (PrimeSpectrum.asIdeal
    ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
        (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
      x))
Tactic: apply PrimeSpectrum.ext
-- 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 R)) ⊕ ↥(Spec (CommRingCat.of S))
⊢ Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((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)))
          x)))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        x))
have asIdeal : ∀ (x : ↥(Spec (CommRingCat.of R))),
  Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((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.inl x))))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl x)))
Tactic: obtain (x | x) := x
Cleared hypotheses: x
-- 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 R)) ⊕ ↥(Spec (CommRingCat.of S))
asIdeal :
  ∀ (x : ↥(Spec (CommRingCat.of R))),
    Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
      (PrimeSpectrum.asIdeal
        ((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.inl x))))
      (PrimeSpectrum.asIdeal
        ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
            (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
          (Sum.inl x)))
⊢ Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((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)))
          x)))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        x))
have asIdeal₁ : ∀ (x : ↥(Spec (CommRingCat.of S))),
  Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((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))))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr x)))
Tactic: obtain (x | x) := x
Cleared hypotheses: x
-- 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 R))
⊢ Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((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.inl x))))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl x)))
have asIdeal : Eq.{u + 1} (α := Ideal (R × S)) (PrimeSpectrum.asIdeal ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
  (PrimeSpectrum.asIdeal
    ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
        (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
      (Sum.inl x)))
Tactic: simp only [coprodMk_inl, coprodMk_inr, ← Scheme.Hom.comp_apply,
      coprodSpec, coprod.inl_desc, coprod.inr_desc]
-- 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))
⊢ Eq.{u + 1} (α := Ideal (↑(CommRingCat.of (R × S)) : Type u))
    (PrimeSpectrum.asIdeal
      ((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))))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr x)))
have asIdeal : Eq.{u + 1} (α := Ideal (R × S)) (PrimeSpectrum.asIdeal ((Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x))
  (PrimeSpectrum.asIdeal
    ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
        (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
      (Sum.inr x)))
Tactic: simp only [coprodMk_inl, coprodMk_inr, ← Scheme.Hom.comp_apply,
      coprodSpec, coprod.inl_desc, coprod.inr_desc]
-- 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 R))
⊢ Eq.{u + 1} (α := Ideal (R × S)) (PrimeSpectrum.asIdeal ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl x)))
have asIdeal : Eq (α := Ideal ((↑(CommRingCat.of R) : Type u) × S))
  (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of R) : Type u))
    (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal)
  (x.asIdeal.prod ⊤)
Tactic: change Ideal.comap _ _ = x.asIdeal.prod ⊤
-- 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 R))
⊢ Eq (α := Ideal ((↑(CommRingCat.of R) : Type u) × S))
    (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of R) : Type u))
      (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal)
    (x.asIdeal.prod ⊤)
have asIdeal : ∀ (x_1 : (↑(CommRingCat.of R) : Type u) × S),
  Membership.mem (γ := Ideal ((↑(CommRingCat.of R) : Type u) × S))
      (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of R) : Type u))
        (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal)
      x_1 ↔
    Membership.mem (γ := Ideal ((↑(CommRingCat.of R) : Type u) × S)) (x.asIdeal.prod ⊤) x_1
Tactic: ext
-- 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))
⊢ Eq.{u + 1} (α := Ideal (R × S)) (PrimeSpectrum.asIdeal ((Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr x)))
have asIdeal : Eq (α := Ideal (R × (↑(CommRingCat.of S) : Type u)))
  (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
    (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal)
  (Ideal.prod ⊤ x.asIdeal)
Tactic: change Ideal.comap _ _ = Ideal.prod ⊤ x.asIdeal
-- 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))
⊢ Eq (α := Ideal (R × (↑(CommRingCat.of S) : Type u)))
    (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
      (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal)
    (Ideal.prod ⊤ x.asIdeal)
have asIdeal : ∀ (x_1 : R × (↑(CommRingCat.of S) : Type u)),
  Membership.mem (γ := Ideal (R × (↑(CommRingCat.of S) : Type u)))
      (Ideal.comap (F := (↑(CommRingCat.of (R × S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
        (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal)
      x_1 ↔
    Membership.mem (γ := Ideal (R × (↑(CommRingCat.of S) : Type u))) (Ideal.prod ⊤ x.asIdeal) x_1
Tactic: ext
-- 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 R) ⨿ Spec (CommRingCat.of S))
⊢ Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
    ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        ((Homeomorph.symm (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)))
          x) :
      PrimeSpectrum (R × S))
have rw : Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
  ((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)))
        ((Homeomorph.symm (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)))
            x :
          ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S)))) :
    ↥(Spec (CommRingCat.of (R × S))))
Tactic: rw [← coprodSpec_coprodMk, Homeomorph.apply_symm_apply]
-- 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 R) ⨿ Spec (CommRingCat.of S))
rw :
  Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
    ((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)))
          ((Homeomorph.symm (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)))
              x :
            ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S)))) :
      ↥(Spec (CommRingCat.of (R × S))))
⊢ Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
    ((Equiv.symm (PrimeSpectrum.primeSpectrumProd R S) :
          (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        ((Homeomorph.symm (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)))
          x) :
      PrimeSpectrum (R × S))
have rw₁ : Eq (α := ↥(Spec (CommRingCat.of (R × S)))) ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
  ((coprodSpec R S) x : ↥(Spec (CommRingCat.of (R × S))))
Tactic: rw [← coprodSpec_coprodMk, Homeomorph.apply_symm_apply]
-- 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 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 inl : ∀ (x : ↥(Spec (CommRingCat.of R))),
  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.inl 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.inl x)))
Tactic: obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: x
-- 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 R) ⨿ Spec (CommRingCat.of S))
inl :
  ∀ (x : ↥(Spec (CommRingCat.of R))),
    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.inl 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.inl x)))
⊢ IsIso (X := (Spec (CommRingCat.of (R × S))).presheaf.stalk ((coprodSpec R S) x))
    (Scheme.Hom.stalkMap (coprodSpec R S) x)
have inr : ∀ (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)))
Tactic: obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: 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 R))
⊢ 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.inl 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.inl x)))
have this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: have := Scheme.Hom.stalkMap_comp coprod.inl (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 R))
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.inl 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.inl x)))
have this₁ : 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 sorry))
      (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))
Tactic: rw [← IsIso.comp_inv_eq,
      Scheme.Hom.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inl 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 R))
this :
  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))
⊢ 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.inl 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.inl x)))
have inl : 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 sorry))
      (Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
    inv (Scheme.Hom.stalkMap coprod.inl x))
Tactic: rw [coprodMk_inl, ← this]