awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
⊢ V ⊆
    ⋃ (i : (↑s : Type u)),
      (fun (i : (↑s : Type u)) ↦
          (TopologicalSpace.Opens.carrier
              (basicOpen (↑i : (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u))) :
            Set (PrimeSpectrum (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u))))
        i

Tactic:
simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ s)), ← hs]

Premises used: Set.compl_iInter, PrimeSpectrum.zeroLocus_iUnion₂
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
obtain :
  ∀ (t : Finset (↑s : Type u))
    (ht :
      V ⊆
        ⋃ i ∈ t,
          TopologicalSpace.Opens.carrier (basicOpen (↑i : (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))),
    ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)
⊢ ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)

Tactic:
obtain ⟨t, ht⟩ := hV'.elim_finite_subcover
      (fun i : s ↦ (basicOpen i.1).1) (fun _ ↦ (basicOpen _).2)
      (by simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ s)), ← hs])

Premises used: PrimeSpectrum.basicOpen, TopologicalSpace.Opens.carrier, IsCompact.elim_finite_subcover, TopologicalSpace.Opens.is_open', Subtype.val
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Finset (↑s : Type u)
ht :
  V ⊆
    ⋃ i ∈ t,
      TopologicalSpace.Opens.carrier (basicOpen (↑i : (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))
⊢ (↑(Finset.map
          (Function.Embedding.subtype fun (x : (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) ↦ x ∈ s) t) :
      Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) ⊆
    s

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Finset (↑s : Type u)
ht :
  V ⊆
    ⋃ i ∈ t,
      TopologicalSpace.Opens.carrier (basicOpen (↑i : (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))
⊢ V ⊆
    ⋃
      i ∈
        (↑(Finset.map
              (Function.Embedding.subtype fun (x : (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) ↦ x ∈ s)
              t) :
          Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)),
      TopologicalSpace.Opens.carrier (basicOpen i)

Tactic:
simpa using ht
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Finset (↑s : Type u)
ht :
  V ⊆
    ⋃ i ∈ t,
      TopologicalSpace.Opens.carrier (basicOpen (↑i : (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))
⊢ ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)

Tactic:
exact ⟨t.map (Function.Embedding.subtype _), by simp, Finset.finite_toSet _, by simpa using ht⟩
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
obtain :
  ∀ (t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) (hts : t ⊆ s) (ht : t.Finite)
    (ht' : V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)), U = ⊤
⊢ U = ⊤

Tactic:
obtain ⟨t, hts, ht, ht'⟩ : ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, (basicOpen i).1 := by
    obtain ⟨t, ht⟩ := hV'.elim_finite_subcover
      (fun i : s ↦ (basicOpen i.1).1) (fun _ ↦ (basicOpen _).2)
      (by simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ s)), ← hs])
    exact ⟨t.map (Function.Embedding.subtype _), by simp, Finset.finite_toSet _, by simpa using ht⟩
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)
⊢ V ⊆ (zeroLocus t)ᶜ

Tactic:
simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ t))] using ht'

Premises used: Set.compl_iInter, PrimeSpectrum.zeroLocus_iUnion₂
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)
⊢ V ⊆ (zeroLocus t)ᶜ

Tactic:
replace ht' : V ⊆ (zeroLocus t)ᶜ := by
    simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ t))] using ht'
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
rw :
  Subset (α := Set (PrimeSpectrum ((i : ι) → (↑(R i) : Type u))))
    (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
    (zeroLocus t)ᶜ
⊢ Eq (α := Ideal (↑(R i) : Type u))
    (Ideal.span
      ((⇑(Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i) :
          (a : (i : ι) → (↑(R i) : Type u)) → (↑(R i) : Type u)) ''
        t))
    ⊤

Tactic:
rw [← zeroLocus_empty_iff_eq_top, zeroLocus_span, ← preimage_comap_zeroLocus,
      ← Set.compl_univ_iff, ← Set.preimage_compl, Set.preimage_eq_univ_iff]

Premises used: PrimeSpectrum.zeroLocus_span, PrimeSpectrum.preimage_comap_zeroLocus, Set.preimage_eq_univ_iff, Set.preimage_compl, PrimeSpectrum.zeroLocus_empty_iff_eq_top, Set.compl_univ_iff
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
trans :
  Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)) ⊆
    (Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier
trans₁ :
  (Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier ⊆ (zeroLocus t)ᶜ
⊢ Subset (α := Set (PrimeSpectrum ((i : ι) → (↑(R i) : Type u))))
    (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
    (zeroLocus t)ᶜ

Tactic:
trans (Sigma.ι _ i ≫ sigmaSpec R).opensRange.1

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange, CategoryTheory.Limits.Sigma.ι, TopologicalSpace.Opens.carrier, AlgebraicGeometry.sigmaSpec, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
simp :
  Subset.{u} (α := Set (PrimeSpectrum ((i : ι) → (↑(R i) : Type u))))
    (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
    (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
⊢ Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)) ⊆
    (Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Subset.{u} (α := Set (PrimeSpectrum ((i : ι) → (↑(R i) : Type u))))
    (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
    (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
rw :
  (sigmaSpec R ''ᵁ Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i)).carrier ⊆ (zeroLocus t)ᶜ
⊢ (Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier ⊆ (zeroLocus t)ᶜ

Tactic:
rw [Scheme.Hom.opensRange_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange_comp
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ (sigmaSpec R ''ᵁ Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i)).carrier ⊆ (zeroLocus t)ᶜ

Tactic:
(Set.image_subset_range _ _).trans (hV.trans ht')

Premises used: setOf, HasSubset.Subset.trans, Set.image_subset_range, Set.image
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ (sigmaSpec R ''ᵁ Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i)).carrier ⊆ (zeroLocus t)ᶜ

Tactic:
exact (Set.image_subset_range _ _).trans (hV.trans ht')

Premises used: HasSubset.Subset.trans, Set.image_subset_range
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
⊢ ∀ (i : ι),
    Eq (α := Ideal (↑(R i) : Type u))
      (Ideal.span
        ((⇑(Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i) :
            (a : (i : ι) → (↑(R i) : Type u)) → (↑(R i) : Type u)) ''
          t))
      ⊤

Tactic:
have (i : _) : Ideal.span (Pi.evalRingHom (R ·) i '' t) = ⊤ := by
    rw [← zeroLocus_empty_iff_eq_top, zeroLocus_span, ← preimage_comap_zeroLocus,
      ← Set.compl_univ_iff, ← Set.preimage_compl, Set.preimage_eq_univ_iff]
    trans (Sigma.ι _ i ≫ sigmaSpec R).opensRange.1
    · simp; rfl
    · rw [Scheme.Hom.opensRange_comp]
      exact (Set.image_subset_range _ _).trans (hV.trans ht')
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
this :
  ∀ (i : ι),
    Eq (α := Ideal (↑(R i) : Type u))
      (Ideal.span
        ((⇑(Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i) :
            (a : (i : ι) → (↑(R i) : Type u)) → (↑(R i) : Type u)) ''
          t))
      ⊤
⊢ Eq (α := Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) (Ideal.span s) ⊤

Tactic:
have : Ideal.span s = ⊤ := top_le_iff.mp
    ((Ideal.span_eq_top_of_span_image_evalRingHom _ ht this).ge.trans (Ideal.span_mono hts))
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
this_1 :
  ∀ (i : ι),
    Eq (α := Ideal (↑(R i) : Type u))
      (Ideal.span
        ((⇑(Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i) :
            (a : (i : ι) → (↑(R i) : Type u)) → (↑(R i) : Type u)) ''
          t))
      ⊤
this : Eq (α := Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) (Ideal.span s) ⊤
⊢ U = ⊤

Tactic:
simpa [← zeroLocus_span s, zeroLocus_empty_iff_eq_top.mpr this] using hs

Premises used: Iff.mpr, PrimeSpectrum.zeroLocus_span, PrimeSpectrum.zeroLocus_empty_iff_eq_top
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → (↑(R i) : Type u))
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → (↑(R i) : Type u)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
⊢ I = ⊥

Tactic:
le_bot_iff.mp fun x hx ↦ ?_

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → (↑(R i) : Type u))
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → (↑(R i) : Type u)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
refine :
  ∀ (x : (i : ι) → (↑(R i) : Type u)) (hx : x ∈ I),
    Membership.mem (γ := Submodule ((i : ι) → (↑(R i) : Type u)) ((i : ι) → (↑(R i) : Type u))) ⊥ x
⊢ I = ⊥

Tactic:
refine le_bot_iff.mp fun x hx ↦ ?_

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → (↑(R i) : Type u))
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → (↑(R i) : Type u)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → (↑(R i) : Type u)
hx : x ∈ I
h : ∀ (i : ι), x i = 0 i
⊢ Membership.mem (γ := Submodule ((i : ι) → (↑(R i) : Type u)) ((i : ι) → (↑(R i) : Type u))) ⊥ x

Tactic:
ext i
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → (↑(R i) : Type u))
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → (↑(R i) : Type u)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → (↑(R i) : Type u)
hx : x ∈ I
i : ι
⊢ x i = 0 i

Tactic:
simpa [← Category.assoc, Ideal.Quotient.eq_zero_iff_mem.mpr hx] using
    congr((Spec.preimage (Sigma.ι (Spec <| R ·) i ≫ $hf)).hom x).symm

Premises used: Iff.mpr, CategoryTheory.Category.assoc, AlgebraicGeometry.Spec, CommRingCat.Hom.hom, congrArg, CategoryTheory.Limits.Sigma.ι, id, Ideal.Quotient.eq_zero_iff_mem, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Spec.preimage, Eq.symm, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
hV :
  (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆
    Set.range (ι := ↥V) ⇑g
hV' : IsCompact (X := ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) (Set.range (ι := ↥V) ⇑g)
⊢ Scheme.Hom.coborderRange g = ⊤

Tactic:
apply eq_top_of_sigmaSpec_subset_of_isCompact (hVU := subset_coborder)

Premises used: AlgebraicGeometry.eq_top_of_sigmaSpec_subset_of_isCompact
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
⊢ (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆
    Set.range (ι := ↥V) ⇑g

Tactic:
simpa only [← hU'] using Set.range_comp_subset_range f g

Premises used: Set.range_comp_subset_range, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
⊢ IsCompact (X := ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) (Set.range (ι := ↥V) ⇑g)

Tactic:
isCompact_range g.continuous

Premises used: isCompact_range, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
⊢ IsCompact (X := ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) (Set.range (ι := ↥V) ⇑g)

Tactic:
exact isCompact_range g.continuous

Premises used: isCompact_range, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
⊢ Scheme.Hom.coborderRange g = ⊤

Tactic:
have : g.coborderRange = ⊤ := by
    apply eq_top_of_sigmaSpec_subset_of_isCompact (hVU := subset_coborder)
    · simpa only [← hU'] using Set.range_comp_subset_range f g
    · exact isCompact_range g.continuous