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
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCat
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)
⊢ 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 rw : IsIso (Y := Scheme.Spec.obj (op R ⨿ op S))
  (coprodSpec (↑R : Type u) (↑S : Type u) ≫
      inv
        (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))))) :
    Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
Tactic: rw [(IsIso.eq_comp_inv _).mpr this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
⊢ PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec
have this : IsEmpty.{u + 1} ↥(Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ))
Tactic: have : IsEmpty (Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ)) :=
    @Function.isEmpty _ _ spec_punit_isEmpty (Scheme.Spec.mapIso
      (initialIsoIsInitial (initialOpOfTerminal CommRingCat.punitIsTerminal))).hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
this : IsEmpty.{u + 1} ↥(Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ))
⊢ PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec
have this₁ : PreservesColimit (Functor.empty CommRingCatᵒᵖ) Scheme.Spec
Tactic: have := preservesInitial_of_iso Scheme.Spec (asIso (initial.to _))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
⊢ IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)
have he : IsIdempotentElem (M := (a : ι) → R a) (Function.update (β := R) 0 i 1)
Tactic: apply IsLocalization.away_of_isIdempotentElem_of_mul
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
he : IsIdempotentElem (M := (a : ι) → R a) (Function.update (β := R) 0 i 1)
⊢ IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)
have H : ∀ (x y : (a : ι) → R a),
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
      ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i) ↔
    Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
Tactic: apply IsLocalization.away_of_isIdempotentElem_of_mul
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
he : IsIdempotentElem (M := (a : ι) → R a) (Function.update (β := R) 0 i 1)
H :
  ∀ (x y : (a : ι) → R a),
    Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
        ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i) ↔
      Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
⊢ IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)
have H' : Function.Surjective (α := (a : ι) → R a) (β := R i) (⇑(algebraMap ((a : ι) → R a) (R i)) : (a : (a : ι) → R a) → R i)
Tactic: apply IsLocalization.away_of_isIdempotentElem_of_mul
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
⊢ IsIdempotentElem (M := (a : ι) → R a) (Function.update (β := R) 0 i 1)
have he : ∀ (j : ι),
  HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1) (Function.update (β := R) 0 i 1)
      j =
    Function.update (β := R) 0 i 1 j
Tactic: ext j
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
j : ι
⊢ HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1) (Function.update (β := R) 0 i 1)
      j =
    Function.update (β := R) 0 i 1 j
have pos : ∀ (h : j = i),
  HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1) (Function.update (β := R) 0 i 1)
      j =
    Function.update (β := R) 0 i 1 j
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
j : ι
pos :
  ∀ (h : j = i),
    HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1)
        (Function.update (β := R) 0 i 1) j =
      Function.update (β := R) 0 i 1 j
⊢ HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1) (Function.update (β := R) 0 i 1)
      j =
    Function.update (β := R) 0 i 1 j
have neg : ∀ (h : ¬j = i),
  HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1) (Function.update (β := R) 0 i 1)
      j =
    Function.update (β := R) 0 i 1 j
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
⊢ Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
      ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i) ↔
    Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
have H : Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i) →
  Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
H :
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
      ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i) →
    Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
⊢ Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
      ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i) ↔
    Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
have H₁ : Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y →
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
e :
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)
⊢ Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
have H : ∀ (j : ι),
  HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j
Tactic: ext j
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
e :
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)
j : ι
⊢ HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j
have pos : ∀ (h : j = i),
  HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
e :
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)
j : ι
pos :
  ∀ (h : j = i),
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
      HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j
⊢ HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j
have neg : ∀ (h : ¬j = i),
  HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
⊢ IsOpenImmersion (X := Spec (CommRingCat.of (R i))) (Y := Spec (CommRingCat.of ((i : ι) → R i)))
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ R x) i)))
have this₁ : IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)
Tactic: have : IsLocalization.Away (Function.update (β := R) 0 i 1) (R i) := by
    apply IsLocalization.away_of_isIdempotentElem_of_mul
    · ext j; by_cases h : j = i <;> aesop
    · intro x y
      constructor
      · intro e; ext j; by_cases h : j = i <;> aesop
      · intro e; simpa using congr_fun e i
    · exact Function.surjective_eval _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
letI letI₁ letI₂ :
  IsOpenImmersion (X := Spec (CommRingCat.of (R i))) (Y := Spec (CommRingCat.of ((i : ι) → R i)))
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ R x) i)))
⊢ IsOpenImmersion (X := Spec (CommRingCat.of (R i))) (Y := Spec (CommRingCat.of ((i : ι) → R i)))
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ R x) i)))
have letI₃ : let this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i);
∀ (this : IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)),
  IsOpenImmersion (X := Spec (CommRingCat.of (R i))) (Y := Spec (CommRingCat.of ((i : ι) → R i)))
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ R x) i)))
Tactic: classical
  letI := (Pi.evalRingHom R i).toAlgebra
  have : IsLocalization.Away (Function.update (β := R) 0 i 1) (R i) := by
    apply IsLocalization.away_of_isIdempotentElem_of_mul
    · ext j; by_cases h : j = i <;> aesop
    · intro x y
      constructor
      · intro e; ext j; by_cases h : j = i <;> aesop
      · intro e; simpa using congr_fun e i
    · exact Function.surjective_eval _
  exact IsOpenImmersion.of_isLocalization (Function.update 0 i 1)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
⊢ IsOpenImmersion (sigmaSpec R)
have hα : _root_.Pairwise.{u} (α := ι)
  (Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint fun (x : ι) ↦
    Set.range (ι := ↥(Spec (R x))) ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
Tactic: apply isOpenImmersion_sigmaDesc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
ix iy : ι
h : ix ≠ iy
⊢ Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint
    (fun (x : ι) ↦
      Set.range (ι := ↥(Spec (R x)))
        ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
    ix iy
have hα : ∀ ⦃a : ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))⦄,
  Membership.mem (γ := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
      ((fun (x : ι) ↦
          (Set.range (ι := ↥(Spec (R x)))
              ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))) :
            Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))))
        ix)
      a →
    ∀ ⦃b : ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))⦄,
      Membership.mem (γ := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
          ((fun (x : ι) ↦
              (Set.range (ι := ↥(Spec (R x)))
                  ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))) :
                Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))))
            iy)
          b →
        a ≠ b
Tactic: refine Set.disjoint_iff_forall_ne.mpr ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
ix iy : ι
h : ix ≠ iy
x : ↥(Spec (R ix))
y : ↥(Spec (R iy))
e :
  Eq (α := ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
    ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) ix))) x :
      ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
    ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) iy))) y :
      ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
⊢ False
have this : (DFinsupp.single (β := fun (x : ι) ↦ (↑(R x) : Type u)) iy 1 : (a : ι) → (↑(R a) : Type u)) iy ∈ y.asIdeal
Tactic: have : DFinsupp.single (β := (R ·)) iy 1 iy ∈ y.asIdeal :=
    (PrimeSpectrum.ext_iff.mp e).le (x := DFinsupp.single iy 1)
      (show DFinsupp.single (β := (R ·)) iy 1 ix ∈ x.asIdeal by simp [h.symm])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
⊢ IsOpenImmersion (sigmaSpec R)
have hα : _root_.Pairwise.{u} (α := ι)
  (Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint fun (x : ι) ↦
    Set.range (ι := ↥(Spec (R x))) ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
Tactic: classical
  apply isOpenImmersion_sigmaDesc
  intro ix iy h
  refine Set.disjoint_iff_forall_ne.mpr ?_
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ e
  have : DFinsupp.single (β := (R ·)) iy 1 iy ∈ y.asIdeal :=
    (PrimeSpectrum.ext_iff.mp e).le (x := DFinsupp.single iy 1)
      (show DFinsupp.single (β := (R ·)) iy 1 ix ∈ x.asIdeal by simp [h.symm])
  simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
hα :
  _root_.Pairwise.{u} (α := ι)
    (Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint fun (x : ι) ↦
      Set.range (ι := ↥(Spec (R x)))
        ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
⊢ IsOpenImmersion (sigmaSpec R)
have hα₁ : ∀ ⦃ix iy : ι⦄ (h : ix ≠ iy),
  Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint
    (fun (x : ι) ↦
      Set.range (ι := ↥(Spec (R x)))
        ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
    ix iy
Tactic: classical
  apply isOpenImmersion_sigmaDesc
  intro ix iy h
  refine Set.disjoint_iff_forall_ne.mpr ?_
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ e
  have : DFinsupp.single (β := (R ·)) iy 1 iy ∈ y.asIdeal :=
    (PrimeSpectrum.ext_iff.mp e).le (x := DFinsupp.single iy 1)
      (show DFinsupp.single (β := (R ·)) iy 1 ix ∈ x.asIdeal by simp [h.symm])
  simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
hα :
  _root_.Pairwise.{u} (α := ι)
    (Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint fun (x : ι) ↦
      Set.range (ι := ↥(Spec (R x)))
        ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
hα₁ :
  ∀ ⦃ix iy : ι⦄ (h : ix ≠ iy),
    Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint
      (fun (x : ι) ↦
        Set.range (ι := ↥(Spec (R x)))
          ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
      ix iy
⊢ IsOpenImmersion (sigmaSpec R)
have hα₂ : ∀ ⦃ix iy : ι⦄ (h : ix ≠ iy) ⦃a : ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))⦄,
  Membership.mem (γ := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
      ((fun (x : ι) ↦
          (Set.range (ι := ↥(Spec (R x)))
              ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))) :
            Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))))
        ix)
      a →
    ∀ ⦃b : ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))⦄,
      Membership.mem (γ := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
          ((fun (x : ι) ↦
              (Set.range (ι := ↥(Spec (R x)))
                  ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))) :
                Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))))
            iy)
          b →
        a ≠ b
Tactic: classical
  apply isOpenImmersion_sigmaDesc
  intro ix iy h
  refine Set.disjoint_iff_forall_ne.mpr ?_
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ e
  have : DFinsupp.single (β := (R ·)) iy 1 iy ∈ y.asIdeal :=
    (PrimeSpectrum.ext_iff.mp e).le (x := DFinsupp.single iy 1)
      (show DFinsupp.single (β := (R ·)) iy 1 ix ∈ x.asIdeal by simp [h.symm])
  simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
hα :
  _root_.Pairwise.{u} (α := ι)
    (Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint fun (x : ι) ↦
      Set.range (ι := ↥(Spec (R x)))
        ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
hα₁ :
  ∀ ⦃ix iy : ι⦄ (h : ix ≠ iy),
    Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint
      (fun (x : ι) ↦
        Set.range (ι := ↥(Spec (R x)))
          ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
      ix iy
hα₂ :
  ∀ ⦃ix iy : ι⦄ (h : ix ≠ iy) ⦃a : ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))⦄,
    Membership.mem (γ := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
        ((fun (x : ι) ↦
            (Set.range (ι := ↥(Spec (R x)))
                ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))) :
              Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))))
          ix)
        a →
      ∀ ⦃b : ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))⦄,
        Membership.mem (γ := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
            ((fun (x : ι) ↦
                (Set.range (ι := ↥(Spec (R x)))
                    ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))) :
                  Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))))
              iy)
            b →
          a ≠ b
⊢ IsOpenImmersion (sigmaSpec R)
have hα₃ : ∀ ⦃ix iy : ι⦄ (h : ix ≠ iy) (x : ↥(Spec (R ix))) (y : ↥(Spec (R iy)))
  (e :
    Eq (α := ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
      ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) ix))) x :
        ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
      ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) iy))) y :
        ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))),
  False
Tactic: classical
  apply isOpenImmersion_sigmaDesc
  intro ix iy h
  refine Set.disjoint_iff_forall_ne.mpr ?_
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ e
  have : DFinsupp.single (β := (R ·)) iy 1 iy ∈ y.asIdeal :=
    (PrimeSpectrum.ext_iff.mp e).le (x := DFinsupp.single iy 1)
      (show DFinsupp.single (β := (R ·)) iy 1 ix ∈ x.asIdeal by simp [h.symm])
  simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this