awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
⊢ X.basicOpen s = ⊥ ↔ s = 0
have refine : s = 0 → X.basicOpen s = ⊥
Tactic: refine ⟨eq_zero_of_basicOpen_eq_bot s, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
x : ↥X
hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x})
inst : IsReduced X
⊢ IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
have inr : ∀
  (this :
    ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
      [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1))
  (hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
Tactic: wlog hX : ∃ R, X = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
x : ↥X
hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x})
inst : IsReduced X
inr :
  ∀
    (this :
      ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
        [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1))
    (hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
⊢ IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
have wlog : ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
  [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
Tactic: wlog hX : ∃ R, X = Spec R
Cleared hypotheses: x, hx, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
x : ↥X
hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x})
inst : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
⊢ IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
have inr : ∀ (i : X.affineCover.I₀) (x : ↥(X.affineCover.X i))
  (hx :
    Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
      (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))),
  IsField.{u_1} (↑(X.presheaf.stalk ((X.affineCover.f i) x)) : Type u_1)
Tactic: obtain ⟨i, x, rfl⟩ := X.affineCover.exists_eq x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx :
  Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
    (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))
⊢ IsField.{u_1} (↑(X.presheaf.stalk ((X.affineCover.f i) x)) : Type u_1)
have inst : IsReduced.{u_1} (X.affineCover.X i)
Tactic: have inst : IsReduced (X.affineCover.X i) := isReduced_of_isOpenImmersion (X.affineCover.f i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst_1 : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx :
  Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
    (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))
inst : IsReduced.{u_1} (X.affineCover.X i)
⊢ IsField.{u_1} (↑(X.presheaf.stalk ((X.affineCover.f i) x)) : Type u_1)
have inr : Membership.mem (γ := Set (Set ↥(X.affineCover.X i))) (irreducibleComponents ↥(X.affineCover.X i)) (closure {x})
Tactic: refine (asIso <| (X.affineCover.f i).stalkMap x).commRingCatIsoToRingEquiv.isField
      (this _ x ?_ ⟨_, rfl⟩)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst_1 : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx :
  Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
    (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))
inst : IsReduced.{u_1} (X.affineCover.X i)
⊢ Membership.mem (γ := Set (Set ↥(X.affineCover.X i))) (irreducibleComponents ↥(X.affineCover.X i)) (closure {x})
have inr : Membership.mem (γ := Set (Set ↥(X.affineCover.X i))) (irreducibleComponents ↥(X.affineCover.X i))
  (Set.preimage (β := ↥X) (⇑(X.affineCover.f i)) (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X))))
Tactic: rw [(X.affineCover.f i).isOpenEmbedding.closure_eq_preimage_closure_image, Set.image_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X_1 X : Scheme
x : ↥X
hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x})
inst : IsReduced X
hX : ∃ (R : CommRingCat.{u_1}), X = Spec R
⊢ IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
have obtain : ∀ (R : CommRingCat.{u_1}) (x : ↥(Spec R))
  (hx : Membership.mem (γ := Set (Set ↥(Spec R))) (irreducibleComponents ↥(Spec R)) (closure {x}))
  [IsReduced.{u_1} (Spec R)], IsField.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1)
Tactic: obtain ⟨R, rfl⟩ := hX
Cleared hypotheses: X, x, hx, inst, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : Membership.mem (γ := Set (Set ↥(Spec R))) (irreducibleComponents ↥(Spec R)) (closure {x})
inst : IsReduced.{u_1} (Spec R)
⊢ Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) x.asIdeal
have rwa : Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) (PrimeSpectrum.vanishingIdeal {x})
Tactic: rwa [← PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : Membership.mem (γ := Set (Set ↥(Spec R))) (irreducibleComponents ↥(Spec R)) (closure {x})
inst : IsReduced.{u_1} (Spec R)
rwa :
  Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) (PrimeSpectrum.vanishingIdeal {x})
⊢ Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) x.asIdeal
have rwa₁ : Membership.mem (γ := Set (Set (PrimeSpectrum (↑R : Type u_1)))) (irreducibleComponents (PrimeSpectrum (↑R : Type u_1)))
  (closure {x})
Tactic: rwa [← PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : Membership.mem (γ := Set (Set ↥(Spec R))) (irreducibleComponents ↥(Spec R)) (closure {x})
inst : IsReduced.{u_1} (Spec R)
⊢ IsField.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1)
have hx₁ : Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) x.asIdeal
Tactic: replace hx : x.asIdeal ∈ minimalPrimes R := by
    rwa [← PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
inst : IsReduced.{u_1} (Spec R)
hx : Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) x.asIdeal
⊢ IsField.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1)
have rw : Subsingleton.{u_1 + 1} (PrimeSpectrum (↑((Spec R).presheaf.stalk x) : Type u_1))
Tactic: rw [← PrimeSpectrum.subsingleton_iff_isField_of_isReduced]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
⊢ IsReduced X
have component_reduced : autoParam (∀ (U : X.Opens), _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)) IsReduced.component_reduced._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
have component_reduced : ∀ (h : U.carrier = ∅), _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
Tactic: rcases U.1.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
component_reduced : ∀ (h : U.carrier = ∅), _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
have component_reduced₁ : ∀ (h : U.carrier.Nonempty), _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
Tactic: rcases U.1.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
h : U.carrier = ∅
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
have this : U = ⊥
Tactic: have : U = ⊥ := SetLike.ext' h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
h : U.carrier = ∅
this : U = ⊥
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
have this₁ : Subsingleton.{u_1 + 1} (↑Γ(X, U) : Type u_1)
Tactic: haveI : Subsingleton Γ(X, U) :=
      CommRingCat.subsingleton_of_isTerminal (X.sheaf.isTerminalOfEqEmpty this)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
h : U.carrier.Nonempty
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
have this : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
Tactic: haveI : Nonempty U := by simpa
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
⊢ IrreducibleSpace.{u_1} ↥X
have by_contra : ∀ (H : ¬IrreducibleSpace.{u_1} ↥X), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
H : ¬IrreducibleSpace.{u_1} ↥X
⊢ False
have H₁ : ¬IsPreirreducible.{u_1} (X := ↥X) Set.univ
Tactic: replace H : ¬IsPreirreducible .univ := fun h =>
    H { toPreirreducibleSpace := ⟨h⟩
        toNonempty := inferInstance }
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
H : ¬IsPreirreducible.{u_1} (X := ↥X) Set.univ
⊢ False
have H₁ : ∃ (x : Set ↥X) (x_1 : Set ↥X) (_ : IsClosed x) (_ : IsClosed x_1) (_ : Set.univ ⊆ x ∪ x_1),
  ¬Set.univ ⊆ x ∧ ¬Set.univ ⊆ x_1
Tactic: simp_rw [isPreirreducible_iff_isClosed_union_isClosed, not_forall, not_or] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
H :
  ∃ (x : Set ↥X) (x_1 : Set ↥X) (_ : IsClosed x) (_ : IsClosed x_1) (_ : Set.univ ⊆ x ∪ x_1),
    ¬Set.univ ⊆ x ∧ ¬Set.univ ⊆ x_1
⊢ False
have rcases : ∀ (S T : Set ↥X) (hS : IsClosed S) (hT : IsClosed T) (h₁ : Set.univ ⊆ S ∪ T) (h₂ : ¬Set.univ ⊆ S) (h₃ : ¬Set.univ ⊆ T),
  False
Tactic: rcases H with ⟨S, T, hS, hT, h₁, h₂, h₃⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ¬Set.univ ⊆ S
h₃ : ¬Set.univ ⊆ T
⊢ False
have h₄ : ∃ (a : ↥X), a ∉ S
Tactic: rw [Set.not_univ_subset] at h₂ h₃
Cleared hypotheses: h₂, h₃
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ¬Set.univ ⊆ S
h₃ : ¬Set.univ ⊆ T
h₄ : ∃ (a : ↥X), a ∉ S
⊢ False
have h₅ : ∃ (a : ↥X), a ∉ T
Tactic: rw [Set.not_univ_subset] at h₂ h₃
Cleared hypotheses: h₂, h₃
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
⊢ False
have this : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := sorry : Opens ↥X } : Scheme)
Tactic: haveI : Nonempty (⟨Sᶜ, hS.1⟩ : X.Opens) := ⟨⟨_, h₂.choose_spec⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
this : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
⊢ False
have this₁ : Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := sorry : Opens ↥X } : Scheme)
Tactic: haveI : Nonempty (⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, h₃.choose_spec⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
this_1 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this : Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
⊢ False
have this₁ : Nonempty.{u_1 + 1}
  ↥(↑({ carrier := Sᶜ, is_open' := sorry : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := sorry : Opens ↥X }) : Scheme)
Tactic: haveI : Nonempty (⟨Sᶜ, hS.1⟩ ⊔ ⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, Or.inl h₂.choose_spec⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
this_1 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this_2 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this :
  Nonempty.{u_1 + 1}
    ↥(↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Scheme)
refine_2 : False
⊢ False
have refine_1 : Eq (α := Opens ↥X) ({ carrier := Sᶜ, is_open' := sorry } ⊓ { carrier := Tᶜ, is_open' := sorry }) ⊥
Tactic: let e : Γ(X, _) ≅ CommRingCat.of _ :=
    (X.sheaf.isProductOfDisjoint ⟨_, hS.1⟩ ⟨_, hT.1⟩ ?_).conePointUniqueUpToIso
      (CommRingCat.prodFanIsLimit _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
this_1 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this_2 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this :
  Nonempty.{u_1 + 1}
    ↥(↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Scheme)
e : Γ(X, { carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) ≅
  CommRingCat.of
    (↑((X.sheaf.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
                (op { carrier := Sᶜ, is_open' := ⋯ })).prodFan
            (X.sheaf.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
              (op { carrier := Tᶜ, is_open' := ⋯ }))).1 :
      Type u_1) :=
  IsLimit.conePointUniqueUpToIso
    (X.sheaf.isProductOfDisjoint { carrier := Sᶜ, is_open' := ⋯ } { carrier := Tᶜ, is_open' := ⋯ } ⋯)
    ((X.sheaf.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
          (op { carrier := Sᶜ, is_open' := ⋯ })).prodFanIsLimit
      (X.sheaf.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
        (op { carrier := Tᶜ, is_open' := ⋯ })))
⊢ False
have this₁ : IsDomain.{u_1}
  ((↑Γ(X, { carrier := Sᶜ, is_open' := sorry }) : Type u_1) × (↑Γ(X, { carrier := Tᶜ, is_open' := sorry }) : Type u_1))
Tactic: have : IsDomain (Γ(X, ⟨Sᶜ, hS.1⟩) × Γ(X, ⟨Tᶜ, hT.1⟩)) :=
      e.symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
this_1 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this_2 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this :
  Nonempty.{u_1 + 1}
    ↥(↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Scheme)
⊢ Eq (α := Opens ↥X) ({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ }) ⊥
have refine_1 : ∀ (x : ↥X),
  x ∈ (↑({ carrier := Sᶜ, is_open' := sorry : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := sorry : Opens ↥X }) : Set ↥X) ↔
    x ∈ (↑⊥ : Set ↥X)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
this_1 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this_2 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this :
  Nonempty.{u_1 + 1}
    ↥(↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Scheme)
x : ↥X
⊢ x ∈ (↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Set ↥X) ↔
    x ∈ (↑⊥ : Set ↥X)
have refine_1 : x ∈ (↑({ carrier := Sᶜ, is_open' := sorry : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := sorry : Opens ↥X }) : Set ↥X) →
  x ∈ (↑⊥ : Set ↥X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
this_1 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this_2 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this :
  Nonempty.{u_1 + 1}
    ↥(↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Scheme)
x : ↥X
refine_1 :
  x ∈ (↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Set ↥X) →
    x ∈ (↑⊥ : Set ↥X)
⊢ x ∈ (↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Set ↥X) ↔
    x ∈ (↑⊥ : Set ↥X)
have refine_1₁ : x ∈ (↑⊥ : Set ↥X) →
  x ∈ (↑({ carrier := Sᶜ, is_open' := sorry : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := sorry : Opens ↥X }) : Set ↥X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS_1 : IsClosed S
hT_1 : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
this_1 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this_2 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this :
  Nonempty.{u_1 + 1}
    ↥(↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Scheme)
x : ↥X
hS : x ∈ (↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Set ↥X)
hT : x ∈ (↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Set ↥X)
⊢ x ∈ (↑⊥ : Set ↥X)
have refine_1 : ∀ (h : x ∈ S), x ∈ (↑⊥ : Set ↥X)
Tactic: rcases h₁ (show x ∈ ⊤ by trivial) with h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
S T : Set ↥X
hS_1 : IsClosed S
hT_1 : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ (a : ↥X), a ∉ S
h₃ : ∃ (a : ↥X), a ∉ T
this_1 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this_2 : Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)
this :
  Nonempty.{u_1 + 1}
    ↥(↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Scheme)
x : ↥X
hS : x ∈ (↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Set ↥X)
hT : x ∈ (↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Set ↥X)
refine_1 : ∀ (h : x ∈ S), x ∈ (↑⊥ : Set ↥X)
⊢ x ∈ (↑⊥ : Set ↥X)
have refine_1₁ : ∀ (h : x ∈ T), x ∈ (↑⊥ : Set ↥X)
Tactic: rcases h₁ (show x ∈ ⊤ by trivial) with h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
⊢ IsIntegral X
have nonempty : autoParam (Nonempty.{u_1 + 1} ↥X) IsIntegral.nonempty._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
nonempty : autoParam (Nonempty.{u_1 + 1} ↥X) IsIntegral.nonempty._autoParam
⊢ IsIntegral X
have component_integral : autoParam (∀ (U : X.Opens) [Nonempty.{u_1 + 1} ↥(↑U : Scheme)], IsDomain.{u_1} (↑Γ(X, U) : Type u_1))
  IsIntegral.component_integral._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ IsDomain.{u_1} (↑Γ(X, U) : Type u_1)
have this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
Tactic: haveI := (@LocallyRingedSpace.component_nontrivial X.toLocallyRingedSpace U hU).1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
⊢ NoZeroDivisors.{u_1} (↑(X.presheaf.obj (op U)) : Type u_1)
have refine : ∀ {a b : (↑(X.presheaf.obj (op U)) : Type u_1)} (e : a * b = 0), a = 0 ∨ b = 0
Tactic: refine ⟨fun {a b} e => ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
e : a * b = 0
⊢ a = 0 ∨ b = 0
have simp_rw : ¬(↑(X.basicOpen a) : Set ↥X).Nonempty ∨ ¬(↑(X.basicOpen b) : Set ↥X).Nonempty
Tactic: simp_rw [← basicOpen_eq_bot_iff, ← Opens.not_nonempty_iff_eq_bot]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
e : a * b = 0
⊢ ¬(↑(X.basicOpen a) : Set ↥X).Nonempty ∨ ¬(↑(X.basicOpen b) : Set ↥X).Nonempty
have by_contra! : ∀ (h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty), False
Tactic: by_contra! h