-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
lemma iSup_basicOpen_eq_top {ι : Type*} (f : ι → A)
    (hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)) :
    ⨆ i, Proj.basicOpen 𝒜 (f i) = ⊤

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↑↑(Proj 𝒜).toPresheafedSpace
hx : x ∈ ↑⊤
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule

Tactic:
rwa [Ideal.span_le, Set.range_subset_iff]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↑↑(Proj 𝒜).toPresheafedSpace
hx : x ∈ ↑⊤
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ False

Tactic:
refine x.not_irrelevant_le (hf.trans ?_)

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↑↑(Proj 𝒜).toPresheafedSpace
hx : x ∈ ↑⊤
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
⊢ ⨆ i, basicOpen 𝒜 (f i) = ⊤

Tactic:
refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↑↑(Proj 𝒜).toPresheafedSpace
hx : x ∈ ↑⊤
⊢ ∃ i, x ∈ basicOpen 𝒜 (f i)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↑↑(Proj 𝒜).toPresheafedSpace
hx : x ∈ ↑⊤
H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)
⊢ False

Tactic:
simp only [mem_basicOpen, Decidable.not_not] at H

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↑↑(Proj 𝒜).toPresheafedSpace
hx : x ∈ ↑⊤
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ False

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↑↑(Proj 𝒜).toPresheafedSpace
hx : x ∈ ↑⊤
⊢ ∃ i, x ∈ basicOpen 𝒜 (f i)

Tactic:
by_contra! H

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↑↑(Proj 𝒜).toPresheafedSpace
hx : x ∈ ↑⊤
H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)
⊢ False

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ι : Type u_3
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
⊢ ⨆ i, basicOpen 𝒜 (f i) = ⊤

Tactic:
classical
refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_
by_contra! H
simp only [mem_basicOpen, Decidable.not_not] at H
refine x.not_irrelevant_le (hf.trans ?_)
rwa [Ideal.span_le, Set.range_subset_iff]

Result:
no goals