awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
mp :
  ∀ (i : ℕ) (hi : ((GradedRing.proj 𝒜 i : (a : A) → A) f : A) ∉ z.asHomogeneousIdeal),
    ∃ (u : Opens (ProjectiveSpectrum 𝒜)),
      Membership.mem (γ := Set (Opens (ProjectiveSpectrum 𝒜)))
          (Set.range fun (i : ℕ) ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) u ∧
        z ∈ u
⊢ ∃ (u : Opens (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Opens (ProjectiveSpectrum 𝒜)))
        (Set.range fun (i : ℕ) ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) u ∧
      z ∈ u

Tactic:
rcases show ∃ i, GradedRing.proj 𝒜 i f ∉ z.asHomogeneousIdeal by
          contrapose! hz with H
          classical
          rw [← DirectSum.sum_support_decompose 𝒜 f]
          apply Ideal.sum_mem _ fun i _ => H i with ⟨i, hi⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi rwa rwa₁ rwa₂ rwa₃ : ((GradedRing.proj 𝒜 i : (a : A) → A) f : A) ∉ z.asHomogeneousIdeal
⊢ Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) z

Tactic:
rwa [mem_basicOpen]

Premises used: ProjectiveSpectrum.mem_basicOpen
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi : ((GradedRing.proj 𝒜 i : (a : A) → A) f : A) ∉ z.asHomogeneousIdeal
⊢ ∃ (u : Opens (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Opens (ProjectiveSpectrum 𝒜)))
        (Set.range fun (i : ℕ) ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) u ∧
      z ∈ u

Tactic:
exact ⟨basicOpen 𝒜 (GradedRing.proj 𝒜 i f), ⟨i, rfl⟩, by rwa [mem_basicOpen]⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz :
  ∃ (u : Opens (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Opens (ProjectiveSpectrum 𝒜)))
        (Set.range fun (i : ℕ) ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) u ∧
      z ∈ u
mpr :
  ∀ (i : ℕ)
    (hz :
      Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜))
        ((fun (i : ℕ) ↦ (basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f) : Opens (ProjectiveSpectrum 𝒜))) i) z),
    f ∉ z.asHomogeneousIdeal
⊢ f ∉ z.asHomogeneousIdeal

Tactic:
obtain ⟨_, ⟨i, rfl⟩, hz⟩ := hz

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
i : ℕ
hz :
  Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜))
    ((fun (i : ℕ) ↦ (basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f) : Opens (ProjectiveSpectrum 𝒜))) i) z
⊢ f ∉ z.asHomogeneousIdeal

Tactic:
fun rid => hz (z.1.2 i rid)

Premises used: HomogeneousSubmodule.is_homogeneous', Not, ProjectiveSpectrum.asHomogeneousIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
i : ℕ
hz :
  Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜))
    ((fun (i : ℕ) ↦ (basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f) : Opens (ProjectiveSpectrum 𝒜))) i) z
⊢ f ∉ z.asHomogeneousIdeal

Tactic:
exact fun rid => hz (z.1.2 i rid)

Premises used: HomogeneousSubmodule.is_homogeneous', ProjectiveSpectrum.asHomogeneousIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
h_open :
  ∀ (u : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) u →
      IsOpen u
h_nhds :
  ∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)),
    a ∈ u →
      IsOpen u →
        ∃ (v : Set (ProjectiveSpectrum 𝒜)),
          Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
              (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
            a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u_1} (α := ProjectiveSpectrum 𝒜)
    (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜)))

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
r : A
⊢ IsOpen.{u_1} (X := ProjectiveSpectrum 𝒜) ((fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) r)

Tactic:
isOpen_basicOpen 𝒜

Premises used: ProjectiveSpectrum.isOpen_basicOpen
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
r : A
⊢ IsOpen.{u_1} (X := ProjectiveSpectrum 𝒜) ((fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) r)

Tactic:
exact isOpen_basicOpen 𝒜

Premises used: ProjectiveSpectrum.isOpen_basicOpen
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
hp : p ∈ U
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
h_nhds :
  ∀ (s : Set A) (hp : ∃ a ∈ s, a ∉ (↑p.asHomogeneousIdeal : Set A)) (hs : zeroLocus 𝒜 s = Uᶜ),
    ∃ (v : Set (ProjectiveSpectrum 𝒜)),
      Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
          (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
        p ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
      p ∈ v ∧ v ⊆ U

Tactic:
rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp

Premises used: compl_compl, ProjectiveSpectrum.mem_zeroLocus, Set.not_subset, Set.mem_compl_iff
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hp : ∃ a ∈ s, a ∉ (↑p.asHomogeneousIdeal : Set A)
hs : zeroLocus 𝒜 s = Uᶜ
h_nhds :
  ∀ (f : A) (hfs : f ∈ s) (hfp : f ∉ (↑p.asHomogeneousIdeal : Set A)),
    ∃ (v : Set (ProjectiveSpectrum 𝒜)),
      Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
          (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
        p ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
      p ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨f, hfs, hfp⟩ := hp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ (↑p.asHomogeneousIdeal : Set A)
⊢ ∃ (v : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
      p ∈ v ∧ v ⊆ U

Tactic:
⟨basicOpen 𝒜 f, ⟨f, rfl⟩, hfp, ?_⟩

Premises used: ProjectiveSpectrum.basicOpen, SetLike.coe, And.intro, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ (↑p.asHomogeneousIdeal : Set A)
h_nhds : (↑(basicOpen 𝒜 f) : Set (ProjectiveSpectrum 𝒜)) ⊆ U
⊢ ∃ (v : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
      p ∈ v ∧ v ⊆ U

Tactic:
refine ⟨basicOpen 𝒜 f, ⟨f, rfl⟩, hfp, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ (↑p.asHomogeneousIdeal : Set A)
h_nhds : Subset (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) (zeroLocus 𝒜 {f})
⊢ (↑(basicOpen 𝒜 f) : Set (ProjectiveSpectrum 𝒜)) ⊆ U

Tactic:
rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]

Premises used: compl_compl, Set.compl_subset_compl, ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ (↑p.asHomogeneousIdeal : Set A)
⊢ Subset (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) (zeroLocus 𝒜 {f})

Tactic:
zeroLocus_anti_mono 𝒜 (Set.singleton_subset_iff.mpr hfs)

Premises used: Iff.mpr, Set.singleton_subset_iff, ProjectiveSpectrum.zeroLocus_anti_mono
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ (↑p.asHomogeneousIdeal : Set A)
⊢ Subset (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) (zeroLocus 𝒜 {f})

Tactic:
exact zeroLocus_anti_mono 𝒜 (Set.singleton_subset_iff.mpr hfs)

Premises used: Iff.mpr, Set.singleton_subset_iff, ProjectiveSpectrum.zeroLocus_anti_mono
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x x_1 : ProjectiveSpectrum 𝒜
asHomogeneousIdeal : HomogeneousIdeal 𝒜
isPrime : asHomogeneousIdeal.toIdeal.IsPrime
not_irrelevant_le : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal
asHomogeneousIdeal_1 : HomogeneousIdeal 𝒜
isPrime_1 : asHomogeneousIdeal_1.toIdeal.IsPrime
not_irrelevant_le_1 : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal_1
⊢ { asHomogeneousIdeal := asHomogeneousIdeal, isPrime := isPrime, not_irrelevant_le := not_irrelevant_le :
          ProjectiveSpectrum 𝒜 }.asHomogeneousIdeal =
      { asHomogeneousIdeal := asHomogeneousIdeal_1, isPrime := isPrime_1,
          not_irrelevant_le := not_irrelevant_le_1 }.asHomogeneousIdeal →
    { asHomogeneousIdeal := asHomogeneousIdeal, isPrime := isPrime, not_irrelevant_le := not_irrelevant_le :
        ProjectiveSpectrum 𝒜 } =
      { asHomogeneousIdeal := asHomogeneousIdeal_1, isPrime := isPrime_1, not_irrelevant_le := not_irrelevant_le_1 }

Tactic:
simp only [mk.injEq, imp_self]

Premises used: ProjectiveSpectrum.mk.injEq, imp_self
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ x ≤ y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal < y.asHomogeneousIdeal ↔ x < y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x y : ProjectiveSpectrum 𝒜
rw : x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ (↑x.asHomogeneousIdeal : Set A) ⊆ (↑y.asHomogeneousIdeal : Set A)
⊢ x ≤ y ↔ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (closure {x}) y

Tactic:
rw [← as_ideal_le_as_ideal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus,
    vanishingIdeal_singleton]

Premises used: ProjectiveSpectrum.vanishingIdeal_singleton, ProjectiveSpectrum.as_ideal_le_as_ideal, ProjectiveSpectrum.mem_zeroLocus, ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ (↑x.asHomogeneousIdeal : Set A) ⊆ (↑y.asHomogeneousIdeal : Set A)

Tactic:
simp only [as_ideal_le_as_ideal, coe_subset_coe]

Premises used: ProjectiveSpectrum.as_ideal_le_as_ideal, SetLike.coe_subset_coe
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
⊢ T0Space.{u_1} ↥X

Tactic:
T0Space.of_open_cover fun x => ⟨_, X.affineCover.covers x,
    (X.affineCover.f _).opensRange.2, IsEmbedding.t0Space (Y := PrimeSpectrum _)
    (isAffineOpen_opensRange (X.affineCover.f _)).isoSpec.schemeIsoToHomeo.isEmbedding⟩

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, CategoryTheory.PreZeroHypercover.f, Topology.IsEmbedding.t0Space, Homeomorph.isEmbedding, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.intro, Exists.intro, CategoryTheory.Iso.schemeIsoToHomeo, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.is_open', Set.range, AlgebraicGeometry.Scheme.Cover.idx, T0Space.of_open_cover, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
hS :
  ∀
    (s :
      (↑(Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) :
        Type u_1)),
    IsOpen (↑s : Set ↥X)
inst :
  ∀
    (s :
      (↑(Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) :
        Type u_1)),
    QuasiSober.{u_1} (↑(↑s : Set ↥X) : Type u_1)
hS' :
  Eq.{u_1 + 1} (α := Set ↥X)
    (⋃₀ Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) ⊤
⊢ QuasiSober.{u_1} ↥X

Tactic:
apply +allowSynthFailures
    quasiSober_of_open_cover (Set.range fun x => Set.range <| (X.affineCover.f x))

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.ConcreteCategory.hom, quasiSober_of_open_cover, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
i : X.affineCover.I₀
⊢ IsOpen
    (↑(Subtype.mk (p := fun (x : Set ↥X) ↦
          Membership.mem (γ := Set (Set ↥X))
            (Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) x)
          ((fun (x : X.affineCover.I₀) ↦ (Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x) : Set ↥X)) i) ⋯) :
      Set ↥X)

Tactic:
(X.affineCover.f i).isOpenEmbedding.isOpen_range

Premises used: CategoryTheory.PreZeroHypercover.f, setOf, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsOpenEmbedding.isOpen_range, Set.range, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
i : X.affineCover.I₀
⊢ IsOpen
    (↑(Subtype.mk (p := fun (x : Set ↥X) ↦
          Membership.mem (γ := Set (Set ↥X))
            (Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) x)
          ((fun (x : X.affineCover.I₀) ↦ (Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x) : Set ↥X)) i) ⋯) :
      Set ↥X)

Tactic:
exact (X.affineCover.f i).isOpenEmbedding.isOpen_range

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsOpenEmbedding.isOpen_range, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
i : X.affineCover.I₀
⊢ QuasiSober.{u_1}
    (↑(↑(Subtype.mk (p := fun (x : Set ↥X) ↦
              Membership.mem (γ := Set (Set ↥X))
                (Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) x)
              ((fun (x : X.affineCover.I₀) ↦ (Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x) : Set ↥X)) i)
              ⋯) :
          Set ↥X) :
      Type u_1)

Tactic:
@IsOpenEmbedding.quasiSober _ _ _ _ _
      (X.affineCover.f i).isOpenEmbedding.isEmbedding.toHomeomorph.symm.isOpenEmbedding
        PrimeSpectrum.quasiSober

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.quasiSober, Topology.IsOpenEmbedding.isEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Homeomorph.symm, Homeomorph.isOpenEmbedding, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Topology.IsEmbedding.toHomeomorph
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
i : X.affineCover.I₀
⊢ QuasiSober.{u_1}
    (↑(↑(Subtype.mk (p := fun (x : Set ↥X) ↦
              Membership.mem (γ := Set (Set ↥X))
                (Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) x)
              ((fun (x : X.affineCover.I₀) ↦ (Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x) : Set ↥X)) i)
              ⋯) :
          Set ↥X) :
      Type u_1)

Tactic:
exact @IsOpenEmbedding.quasiSober _ _ _ _ _
      (X.affineCover.f i).isOpenEmbedding.isEmbedding.toHomeomorph.symm.isOpenEmbedding
        PrimeSpectrum.quasiSober

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.quasiSober, Topology.IsOpenEmbedding.isEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Homeomorph.symm, Homeomorph.isOpenEmbedding, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Topology.IsEmbedding.toHomeomorph
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
hS' :
  ∀ (x : ↥X),
    Membership.mem (γ := Set ↥X) (⋃ (x : X.affineCover.I₀), Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x))
      x
⊢ Eq.{u_1 + 1} (α := Set ↥X)
    (⋃₀ Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) ⊤

Tactic:
rw [Set.top_eq_univ, Set.sUnion_range, Set.eq_univ_iff_forall]

Premises used: Set.sUnion_range, Set.eq_univ_iff_forall, Set.top_eq_univ
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
x : ↥X
⊢ Membership.mem (γ := Set ↥X) (⋃ (x : X.affineCover.I₀), Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) x

Tactic:
⟨_, ⟨_, rfl⟩, X.affineCover.covers x⟩

Premises used: Set.Mem, iSup, setOf, AlgebraicGeometry.Scheme.Cover.covers, And.intro, Exists.intro, AlgebraicGeometry.Scheme.affineCover, Set.iUnion, rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
x : ↥X
⊢ Membership.mem (γ := Set ↥X) (⋃ (x : X.affineCover.I₀), Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) x

Tactic:
exact ⟨_, ⟨_, rfl⟩, X.affineCover.covers x⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 : Scheme
X : Scheme
⊢ PrespectralSpace.{u} ↥X

Tactic:
have (Y : Scheme.{u}) (_ : IsAffine Y) : PrespectralSpace Y :=
    .of_isClosedEmbedding (Y := PrimeSpectrum _) _
      Y.isoSpec.hom.homeomorph.isClosedEmbedding
  have (i : _) : PrespectralSpace (X.affineCover.f i).opensRange.1 :=
    this (X.affineCover.f i).opensRange (isAffineOpen_opensRange (X.affineCover.f i))
  .of_isOpenCover X.affineCover.isOpenCover_opensRange

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.Scheme.Hom.homeomorph, PrespectralSpace.of_isClosedEmbedding, PrespectralSpace.of_isOpenCover, Homeomorph.isClosedEmbedding, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.affineCover, AlgebraicGeometry.Scheme.Opens.toScheme, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
⊢ ObjectProperty.IsClosedUnderIsomorphisms.{u_1, u_1 + 1} (C := Scheme) fun (x : Scheme.{u_1}) ↦
    IrreducibleSpace.{u_1} ↥x

Tactic:
⟨fun e ↦ e.hom.homeomorph.irreducibleSpace_iff.mp⟩

Premises used: Homeomorph.irreducibleSpace_iff, AlgebraicGeometry.Scheme.Hom.homeomorph, Iff.mp, CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.mk, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
⊢ ObjectProperty.IsClosedUnderIsomorphisms.{u_1, u_1 + 1} (C := Scheme) fun (x : Scheme.{u_1}) ↦ ConnectedSpace.{u_1} ↥x

Tactic:
⟨fun e ↦ e.hom.homeomorph.connectedSpace_iff.mp⟩

Premises used: Homeomorph.connectedSpace_iff, AlgebraicGeometry.Scheme.Hom.homeomorph, Iff.mp, CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.mk, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : ∀ (x : ↥X), _root_.IsReduced.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
⊢ IsReduced X

Tactic:
⟨fun U => ⟨fun s hs => ?_⟩⟩

Premises used: AlgebraicGeometry.IsReduced.mk, IsReduced.mk
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : ∀ (x : ↥X), _root_.IsReduced.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
refine : ∀ (U : X.Opens) (s : (↑Γ(X, U) : Type u_1)) (hs : IsNilpotent s), s = 0
⊢ IsReduced X

Tactic:
refine ⟨fun U => ⟨fun s hs => ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : ∀ (x : ↥X), _root_.IsReduced.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : IsNilpotent s
apply :
  ∀ (x : ↥X) (hx : x ∈ U),
    Eq (α := (↑(X.sheaf.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ U x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op U)) : Type u_1)) → (↑(X.sheaf.presheaf.stalk x) : Type u_1))
          s :
        (↑(X.sheaf.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ U x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op U)) : Type u_1)) → (↑(X.sheaf.presheaf.stalk x) : Type u_1))
          0 :
        (↑(X.sheaf.presheaf.stalk x) : Type u_1))
⊢ s = 0

Tactic:
apply Presheaf.section_ext X.sheaf U s 0

Premises used: AlgebraicGeometry.Scheme.sheaf, OfNat.ofNat, TopCat.Presheaf.section_ext