-- Mathlib/AlgebraicGeometry/PointsPi.lean
lemma eq_top_of_sigmaSpec_subset_of_isCompact
    (U : (Spec (.of (Π i, R i))).Opens) (V : Set (Spec (.of (Π i, R i))))
    (hV : ↑(sigmaSpec R).opensRange ⊆ V)
    (hV' : IsCompact (X := Spec (.of (Π i, R i))) V)
    (hVU : V ⊆ U) : U = ⊤

Proof state:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Set.range ⇑(comap (Pi.evalRingHom (fun x => ↑(R x)) i)) ⊆
    Set.range ⇑(ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x => ↑(R x)) i))).base)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Finset ↑s
ht : V ⊆ ⋃ i ∈ t, (basicOpen ↑i).carrier
⊢ ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ⊆ s

Tactic:
simp

Result:
no goals

Proof state:
case intro
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Finset ↑s
ht : V ⊆ ⋃ i ∈ t, (basicOpen ↑i).carrier
⊢ ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, (basicOpen i).carrier

Tactic:
exact ⟨t.map (Function.Embedding.subtype _), by simp, Finset.finite_toSet _, by simpa using ht⟩

Result:
no goals

Proof state:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ (sigmaSpec R ''ᵁ Scheme.Hom.opensRange (Sigma.ι (fun i => Spec (R i)) i)).carrier ⊆ (zeroLocus t)ᶜ

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

Result:
no goals

Proof state:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
⊢ U = ⊤

Tactic:
obtain ⟨s, hs⟩ := (PrimeSpectrum.isOpen_iff _).mp U.2

Result:
case intro
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
⊢ U = ⊤

Proof state:
case intro.intro.intro.intro
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
this : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x => ↑(R x)) i) '' t) = ⊤
⊢ U = ⊤

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))

Result:
case intro.intro.intro.intro
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
this✝ : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x => ↑(R x)) i) '' t) = ⊤
this : Ideal.span s = ⊤
⊢ U = ⊤

Proof state:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Set.range ⇑(comap (Pi.evalRingHom (fun x => ↑(R x)) i)) ⊆ (zeroLocus t)ᶜ

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

Result:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Set.range ⇑(comap (Pi.evalRingHom (fun x => ↑(R x)) i)) ⊆
    (Scheme.Hom.opensRange (Sigma.ι (fun i => Spec (R i)) i ≫ sigmaSpec R)).carrier

ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ (Scheme.Hom.opensRange (Sigma.ι (fun i => Spec (R i)) i ≫ sigmaSpec R)).carrier ⊆ (zeroLocus t)ᶜ

Proof state:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Ideal.span (⇑(Pi.evalRingHom (fun x => ↑(R x)) i) '' 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]

Result:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↑↑(Spec (CommRingCat.of ((i : ι) → ↑(R i)))).toPresheafedSpace
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Set.range ⇑(comap (Pi.evalRingHom (fun x => ↑(R x)) i)) ⊆ (zeroLocus t)ᶜ