-- 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)) ⊆
    (Scheme.Hom.opensRange (Sigma.ι (fun i => Spec (R i)) i ≫ sigmaSpec R)).carrier

Tactic:
simp

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)) ⊆
    Set.range ⇑(ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x => ↑(R x)) i))).base)

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 : ι
⊢ (Scheme.Hom.opensRange (Sigma.ι (fun i => Spec (R i)) i ≫ sigmaSpec R)).carrier ⊆ (zeroLocus t)ᶜ

Tactic:
rw [Scheme.Hom.opensRange_comp]

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 : ι
⊢ (sigmaSpec R ''ᵁ Scheme.Hom.opensRange (Sigma.ι (fun i => Spec (R i)) i)).carrier ⊆ (zeroLocus t)ᶜ

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) = ⊤
this : Ideal.span s = ⊤
⊢ U = ⊤

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

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
⊢ V ⊆ ⋃ i ∈ ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t), (basicOpen i).carrier

Tactic:
simpa using ht

Result:
no goals