-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem basicOpen_eq_union_of_projection (f : A) :
    basicOpen 𝒜 f = ⨆ i : ℕ, basicOpen 𝒜 (GradedAlgebra.proj 𝒜 i f) :=
  TopologicalSpace.Opens.ext <|
    Set.ext fun z => by
      rw [mem_coe_basicOpen, mem_coe, iSup, TopologicalSpace.Opens.mem_sSup]
      constructor <;> intro hz
      · rcases show ∃ i, GradedAlgebra.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⟩
        exact ⟨basicOpen 𝒜 (GradedAlgebra.proj 𝒜 i f), ⟨i, rfl⟩, by rwa [mem_basicOpen]⟩
      · obtain ⟨_, ⟨i, rfl⟩, hz⟩ := hz
        exact fun rid => hz (z.1.2 i rid)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 f]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) f), ↑(((decompose 𝒜) f) i) ∈ z.asHomogeneousIdeal

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ∃ u ∈ Set.range fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f), z ∈ u
⊢ f ∉ z.asHomogeneousIdeal

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

Result:
case mpr.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
i : ℕ
hz : z ∈ (fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f)) i
⊢ f ∉ z.asHomogeneousIdeal

Proof state:
case mp.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi : (GradedAlgebra.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
⊢ ∃ u ∈ Set.range fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f), z ∈ u

Tactic:
exact ⟨basicOpen 𝒜 (GradedAlgebra.proj 𝒜 i f), ⟨i, rfl⟩, by rwa [mem_basicOpen]⟩

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ z ∈ ↑(basicOpen 𝒜 f) ↔ z ∈ ↑(⨆ i, basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f))

Tactic:
rw [mem_coe_basicOpen, mem_coe, iSup, TopologicalSpace.Opens.mem_sSup]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal ↔ ∃ u ∈ Set.range fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f), z ∈ u

Proof state:
case mpr.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
i : ℕ
hz : z ∈ (fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f)) i
⊢ f ∉ z.asHomogeneousIdeal

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

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal

Tactic:
classical
rw [← DirectSum.sum_support_decompose 𝒜 f]
apply Ideal.sum_mem _ fun i _ => H i

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
⊢ ∃ i, (GradedAlgebra.proj 𝒜 i) f ∉ z.asHomogeneousIdeal

Tactic:
contrapose! hz with H

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi : (GradedAlgebra.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
⊢ z ∈ basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f)

Tactic:
rwa [mem_basicOpen]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) f), ↑(((decompose 𝒜) f) i) ∈ z.asHomogeneousIdeal

Tactic:
apply Ideal.sum_mem _ fun i _ => H i

Result:
no goals

Proof state:
case mp
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
⊢ ∃ u ∈ Set.range fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f), z ∈ u

Tactic:
rcases show ∃ i, GradedAlgebra.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⟩

Result:
case mp.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi : (GradedAlgebra.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
⊢ ∃ u ∈ Set.range fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f), z ∈ u

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal ↔ ∃ u ∈ Set.range fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f), z ∈ u

Tactic:
constructor <;> intro hz

Result:
case mp
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
⊢ ∃ u ∈ Set.range fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f), z ∈ u

case mpr
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ∃ u ∈ Set.range fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f), z ∈ u
⊢ f ∉ z.asHomogeneousIdeal