-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f_1 : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
have :
  Eq (α := Ideal A)
    (Ideal.span
      (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
        x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
    (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
have₁ :
  ∀
    (H :
      Eq (α := Ideal A)
        (Ideal.span
          (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
            x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
              0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
        (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))),
    TopologicalSpace.IsOpenCover (X := ↥X) fun (ir : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
      X.basicOpen (U := ⊤)
        ((f : (a : A) → (↑Γ(X, ⊤) : Type u))
          (ir.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
            0 < ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
              r ∈ 𝒜 (ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
have₂ :
  Eq (α := Ideal A)
    (Ideal.span
      (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
        x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
    (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
have₃ have₄ :
  ∀
    (H :
      Eq (α := Ideal A)
        (Ideal.span
          (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
            x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
              0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
        (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))),
    TopologicalSpace.IsOpenCover (X := ↥X) fun (ir : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
      X.basicOpen (U := ⊤)
        ((f : (a : A) → (↑Γ(X, ⊤) : Type u))
          (ir.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
            0 < ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
              r ∈ 𝒜 (ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
h :
  ∀
    (H :
      Eq (α := Ideal A)
        (Ideal.span
          (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
            x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
              0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
        (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))),
    (↑(⨆ (ir : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i),
            X.basicOpen (U := ⊤)
              ((f : (a : A) → (↑Γ(X, ⊤) : Type u))
                (ir.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                  0 < ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                    r ∈ 𝒜 (ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))) :
        Set ↥X) =
      (↑⊤ : Set ↥X)
h₁ :
  ∀
    (H :
      Eq (α := Ideal A)
        (Ideal.span
          (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
            x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
              0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
        (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))),
    (↑(⨆ (ir : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i),
              X.basicOpen (U := ⊤)
                ((f : (a : A) → (↑Γ(X, ⊤) : Type u))
                  (ir.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                    0 < ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                      r ∈ 𝒜 (ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))) :
          Set ↥X)ᶜ =
      (↑⊤ : Set ↥X)ᶜ
h₂ :
  ∀
    (H :
      Eq (α := Ideal A)
        (Ideal.span
          (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
            x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
              0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
        (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))),
    X.zeroLocus (U := ⊤)
        (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
          (f : (a : A) → (↑Γ(X, ⊤) : Type u))
            (x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
              0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))))) =
      ∅
h₃ :
  ∀
    (H :
      Eq (α := Ideal A)
        (Ideal.span
          (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
            x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
              0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
        (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))),
    X.zeroLocus (↑⊤ : Set (↑Γ(X, ⊤) : Type u)) = ∅
⊢ TopologicalSpace.IsOpenCover (X := ↥X) fun (ir : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
    X.basicOpen (U := ⊤)
      ((f : (a : A) → (↑Γ(X, ⊤) : Type u))
        (ir.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (ir.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))

Tactic:
classical
    have H : Ideal.span (Set.range fun x : Σ' i r, 0 < i ∧ r ∈ 𝒜 i ↦ x.2.1) =
        (HomogeneousIdeal.irrelevant 𝒜).toIdeal := by
      apply le_antisymm
      · rw [Ideal.span_le, Set.range_subset_iff]
        rintro ⟨i, r, hi0, hri⟩
        simp [-ZeroMemClass.coe_eq_zero,
          DirectSum.decompose_of_mem_ne 𝒜 hri hi0.ne']
      · intro x hx
        rw [← DirectSum.sum_support_decompose 𝒜 x]
        refine Ideal.sum_mem _ fun c hc ↦ ?_
        have : c ≠ 0 := by contrapose hc; simpa [hc] using hx
        exact Ideal.subset_span ⟨⟨c, _, this.bot_lt, by simp⟩, rfl⟩
    ext1
    apply compl_injective
    simp only [TopologicalSpace.Opens.coe_iSup, Set.compl_iUnion, ← Scheme.zeroLocus_singleton,
      ← Scheme.zeroLocus_iUnion, Set.iUnion_singleton_eq_range, TopologicalSpace.Opens.coe_top,
      Set.compl_univ]
    rw [← Scheme.zeroLocus_span, Set.range_comp', ← Ideal.map_span, H, hf]
    simp

Premises used: TopologicalSpace.Opens.coe_iSup, AlgebraicGeometry.Scheme.zeroLocus_iUnion, AlgebraicGeometry.Scheme.zeroLocus_singleton, Set.iUnion_singleton_eq_range, Ideal.map_span, compl_injective, Set.compl_univ, Set.compl_iUnion, AlgebraicGeometry.Scheme.zeroLocus_span, Set.range_comp', TopologicalSpace.Opens.coe_top