awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Properties
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
⊢ Subsingleton.{u_1 + 1} (PrimeSpectrum (↑((Spec R).presheaf.stalk x) : Type u_1))

Tactic:
IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes _ hx
    ((Spec.structureSheaf R).presheaf.stalk x)

Premises used: CommRingCat.carrier, AlgebraicGeometry.Spec.topObj, IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes, TopCat.Presheaf.stalk, AlgebraicGeometry.Spec.structureSheaf, AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.structurePresheafInCommRingCat, TopCat.Sheaf.presheaf
-- Module: Mathlib.AlgebraicGeometry.Properties
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
⊢ Subsingleton.{u_1 + 1} (PrimeSpectrum (↑((Spec R).presheaf.stalk x) : Type u_1))

Tactic:
exact IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes _ hx
    ((Spec.structureSheaf R).presheaf.stalk x)

Premises used: CommRingCat.carrier, IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes, TopCat.Presheaf.stalk, AlgebraicGeometry.Spec.structureSheaf, TopCat.Sheaf.presheaf
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
⊢ IsDomain.{u_1} (↑Γ(X, ⊤) : Type u_1)

Tactic:
@IsIntegral.component_integral _ _ _ ⟨Nonempty.some inferInstance, trivial⟩

Premises used: AlgebraicGeometry.IsIntegral.component_integral
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
component_reduced :
  autoParam (∀ (U : X.Opens), _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)) IsReduced.component_reduced._autoParam
⊢ IsReduced X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
component_reduced : ∀ (h : U.carrier = ∅), _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
component_reduced₁ : ∀ (h : U.carrier.Nonempty), _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)

Tactic:
rcases U.1.eq_empty_or_nonempty with h | h

Premises used: TopologicalSpace.Opens.carrier, Set.eq_empty_or_nonempty
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
h : U.carrier = ∅
⊢ U = ⊥

Tactic:
have : U = ⊥ := SetLike.ext' h
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
h : U.carrier = ∅
this : U = ⊥
⊢ Subsingleton.{u_1 + 1} (↑Γ(X, U) : Type u_1)

Tactic:
haveI : Subsingleton Γ(X, U) :=
      CommRingCat.subsingleton_of_isTerminal (X.sheaf.isTerminalOfEqEmpty this)
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
h : U.carrier = ∅
this_1 : U = ⊥
this : Subsingleton.{u_1 + 1} (↑Γ(X, U) : Type u_1)
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
h : U.carrier.Nonempty
⊢ Nonempty.{u_1 + 1} ↥(↑U : Scheme)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
h : U.carrier.Nonempty
⊢ Nonempty.{u_1 + 1} ↥(↑U : Scheme)

Tactic:
haveI : Nonempty U := by simpa
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
h : U.carrier.Nonempty
this : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 : Scheme
X : Scheme
U : X.Opens
inst : Nonempty.{u + 1} ↥(↑U : Scheme)
⊢ Nontrivial.{u} (↑Γ(X, U) : Type u)

Tactic:
LocallyRingedSpace.component_nontrivial (hU := ‹_›)

Premises used: AlgebraicGeometry.LocallyRingedSpace.component_nontrivial
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
by_contra : ∀ (H : ¬IrreducibleSpace.{u_1} ↥X), False
⊢ IrreducibleSpace.{u_1} ↥X

Tactic:
by_contra H
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
H : ¬IrreducibleSpace.{u_1} ↥X
⊢ ¬IsPreirreducible.{u_1} (X := ↥X) Set.univ

Tactic:
replace H : ¬IsPreirreducible .univ := fun h =>
    H { toPreirreducibleSpace := ⟨h⟩
        toNonempty := inferInstance }
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
H : ¬IsPreirreducible.{u_1} (X := ↥X) Set.univ
⊢ ∃ (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

Premises used: isPreirreducible_iff_isClosed_union_isClosed, not_or, Classical.not_forall
-- Module: Mathlib.AlgebraicGeometry.Properties
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
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
⊢ False

Tactic:
rcases H with ⟨S, T, hS, hT, h₁, h₂, h₃⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
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
⊢ ∃ (a : ↥X), a ∉ S

Tactic:
rw [Set.not_univ_subset] at h₂ h₃

Premises used: Set.not_univ_subset
-- Module: Mathlib.AlgebraicGeometry.Properties
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
⊢ ∃ (a : ↥X), a ∉ T

Tactic:
rw [Set.not_univ_subset] at h₂ h₃

Premises used: Set.not_univ_subset
-- Module: Mathlib.AlgebraicGeometry.Properties
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
⊢ Nonempty.{u_1 + 1} ↥(↑{ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)

Tactic:
haveI : Nonempty (⟨Sᶜ, hS.1⟩ : X.Opens) := ⟨⟨_, h₂.choose_spec⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
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)
⊢ Nonempty.{u_1 + 1} ↥(↑{ carrier := Tᶜ, is_open' := ⋯ : Opens ↥X } : Scheme)

Tactic:
haveI : Nonempty (⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, h₃.choose_spec⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
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)
⊢ Nonempty.{u_1 + 1}
    ↥(↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊔ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Scheme)

Tactic:
haveI : Nonempty (⟨Sᶜ, hS.1⟩ ⊔ ⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, Or.inl h₂.choose_spec⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
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
refine_1 : Eq (α := Opens ↥X) ({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ }) ⊥
⊢ False

Tactic:
let e : Γ(X, _) ≅ CommRingCat.of _ :=
    (X.sheaf.isProductOfDisjoint ⟨_, hS.1⟩ ⟨_, hT.1⟩ ?_).conePointUniqueUpToIso
      (CommRingCat.prodFanIsLimit _ _)
-- Module: Mathlib.AlgebraicGeometry.Properties
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' := ⋯ })))
⊢ IsDomain.{u_1}
    ((↑Γ(X, { carrier := Sᶜ, is_open' := ⋯ }) : Type u_1) × (↑Γ(X, { carrier := Tᶜ, is_open' := ⋯ }) : Type u_1))

Tactic:
have : IsDomain (Γ(X, ⟨Sᶜ, hS.1⟩) × Γ(X, ⟨Tᶜ, hT.1⟩)) :=
      e.symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _
-- Module: Mathlib.AlgebraicGeometry.Properties
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_3 :
  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' := ⋯ })))
this :
  IsDomain.{u_1}
    ((↑Γ(X, { carrier := Sᶜ, is_open' := ⋯ }) : Type u_1) × (↑Γ(X, { carrier := Tᶜ, is_open' := ⋯ }) : Type u_1))
⊢ False

Tactic:
false_of_nontrivial_of_product_domain Γ(X, ⟨Sᶜ, hS.1⟩) Γ(X, ⟨Tᶜ, hT.1⟩)

Premises used: false_of_nontrivial_of_product_domain, CommRingCat.carrier, IsClosed.isOpen_compl, Compl.compl, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopologicalSpace.Opens.mk, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
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_3 :
  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' := ⋯ })))
this :
  IsDomain.{u_1}
    ((↑Γ(X, { carrier := Sᶜ, is_open' := ⋯ }) : Type u_1) × (↑Γ(X, { carrier := Tᶜ, is_open' := ⋯ }) : Type u_1))
⊢ False

Tactic:
exact false_of_nontrivial_of_product_domain Γ(X, ⟨Sᶜ, hS.1⟩) Γ(X, ⟨Tᶜ, hT.1⟩)

Premises used: false_of_nontrivial_of_product_domain, CommRingCat.carrier, IsClosed.isOpen_compl, Compl.compl, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopologicalSpace.Opens.mk, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
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_1 :
  ∀ (x : ↥X),
    x ∈ (↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Set ↥X) ↔
      x ∈ (↑⊥ : Set ↥X)
⊢ Eq (α := Opens ↥X) ({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ }) ⊥

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Properties
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)
refine_1₁ :
  x ∈ (↑⊥ : Set ↥X) →
    x ∈ (↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Set ↥X)
⊢ x ∈ (↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Set ↥X) ↔
    x ∈ (↑⊥ : Set ↥X)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Properties
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)
⊢ Membership.mem (γ := Set ↥X) ⊤ x

Tactic:
trivial
-- Module: Mathlib.AlgebraicGeometry.Properties
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)
refine_1₁ : ∀ (h : x ∈ T), x ∈ (↑⊥ : Set ↥X)
⊢ x ∈ (↑⊥ : Set ↥X)

Tactic:
rcases h₁ (show x ∈ ⊤ by trivial) with h | h
-- Module: Mathlib.AlgebraicGeometry.Properties
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)
h : x ∈ S
⊢ x ∈ (↑⊥ : Set ↥X)

Tactic:
hS h

Premises used: Set.Mem
-- Module: Mathlib.AlgebraicGeometry.Properties
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)
h : x ∈ T
⊢ x ∈ (↑⊥ : Set ↥X)

Tactic:
hT h

Premises used: Set.Mem
-- Module: Mathlib.AlgebraicGeometry.Properties
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)
h : x ∈ S
⊢ x ∈ (↑⊥ : Set ↥X)

Tactic:
exacts [hS h, hT h]
-- Module: Mathlib.AlgebraicGeometry.Properties
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 ∈ (↑⊥ : Set ↥X) →
    x ∈ (↑({ carrier := Sᶜ, is_open' := ⋯ : Opens ↥X } ⊓ { carrier := Tᶜ, is_open' := ⋯ : Opens ↥X }) : Set ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
nonempty : autoParam (Nonempty.{u_1 + 1} ↥X) IsIntegral.nonempty._autoParam
component_integral :
  autoParam (∀ (U : X.Opens) [Nonempty.{u_1 + 1} ↥(↑U : Scheme)], IsDomain.{u_1} (↑Γ(X, U) : Type u_1))
    IsIntegral.component_integral._autoParam
⊢ IsIntegral X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
⊢ autoParam (Nonempty.{u_1 + 1} ↥X) IsIntegral.nonempty._autoParam

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ ∃ (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
-- Module: Mathlib.AlgebraicGeometry.Properties
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)

Tactic:
⟨fun {a b} e => ?_⟩

Premises used: NoZeroDivisors.mk
-- Module: Mathlib.AlgebraicGeometry.Properties
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
refine : ∀ {a b : (↑(X.presheaf.obj (op U)) : Type u_1)} (e : a * b = 0), a = 0 ∨ b = 0
⊢ NoZeroDivisors.{u_1} (↑(X.presheaf.obj (op U)) : Type u_1)

Tactic:
refine ⟨fun {a b} e => ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
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
simp_rw : ¬(↑(X.basicOpen a) : Set ↥X).Nonempty ∨ ¬(↑(X.basicOpen b) : Set ↥X).Nonempty
⊢ a = 0 ∨ b = 0

Tactic:
simp_rw [← basicOpen_eq_bot_iff, ← Opens.not_nonempty_iff_eq_bot]

Premises used: AlgebraicGeometry.basicOpen_eq_bot_iff, TopologicalSpace.Opens.not_nonempty_iff_eq_bot
-- Module: Mathlib.AlgebraicGeometry.Properties
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
by_contra! : ∀ (h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty), False
⊢ ¬(↑(X.basicOpen a) : Set ↥X).Nonempty ∨ ¬(↑(X.basicOpen b) : Set ↥X).Nonempty

Tactic:
by_contra! h