awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
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_1 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 𝒜))) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
c : ℕ
hc :
  Membership.mem (γ := Finset ℕ)
    (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x))
    c
⊢ c ≠ 0
have contrapose : ∀ (hc : c = 0),
  c ∉
    DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x)
Tactic: contrapose hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (hypothesis)
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_1 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 𝒜))) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
c : ℕ
hc :
  Membership.mem (γ := Finset ℕ)
    (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x))
    c
⊢ Membership.mem (γ := 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)))))
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          c) :
      A)
have this : c ≠ 0
Tactic: have : c ≠ 0 := by contrapose hc; simpa [hc] using hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (hypothesis)
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 𝒜))) ⊤
⊢ 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 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 𝒜))
Tactic: 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⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
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 𝒜))) ⊤
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 h : (↑(⨆ (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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
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 𝒜))) ⊤
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)
have h : (↑(⨆ (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)ᶜ
Tactic: apply compl_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
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 𝒜))) ⊤
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)ᶜ
have h : 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))))) =
  ∅
Tactic: 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
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 𝒜))) ⊤
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))))) =
    ∅
have h : X.zeroLocus (↑⊤ : Set (↑Γ(X, ⊤) : Type u)) = ∅
Tactic: rw [← Scheme.zeroLocus_span, Set.range_comp', ← Ideal.map_span, H, hf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
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 𝒜))) ⊤
⊢ 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 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 𝒜))
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
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 𝒜))
⊢ 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 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)))))
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
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 𝒜))) ⊤
⊢ X ⟶ Proj 𝒜
have refine : ∀ (x y : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀),
  Eq (α := pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ⟶ Proj 𝒜)
    (pullback.fst ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≫
      (fun (ri : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀) ↦
          (toBasicOpenOfGlobalSections 𝒜 f sorry sorry sorry ≫
              Scheme.Opens.ι
                (basicOpen 𝒜
                  (ri.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                    0 < ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                      r ∈ 𝒜 (ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))))) :
            (openCoverOfMapIrrelevantEqTop 𝒜 f hf).X ri ⟶ Proj 𝒜))
        x)
    (pullback.snd ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≫
      (fun (ri : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀) ↦
          (toBasicOpenOfGlobalSections 𝒜 f sorry sorry sorry ≫
              Scheme.Opens.ι
                (basicOpen 𝒜
                  (ri.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                    0 < ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                      r ∈ 𝒜 (ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))))) :
            (openCoverOfMapIrrelevantEqTop 𝒜 f hf).X ri ⟶ Proj 𝒜))
        y)
Tactic: refine (openCoverOfMapIrrelevantEqTop 𝒜 f hf).glueMorphisms
    (fun ri ↦ toBasicOpenOfGlobalSections 𝒜 f rfl ri.2.2.1 ri.2.2.2 ≫ Scheme.Opens.ι _) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ Eq (α := (↑(fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r) : Scheme) ⟶ (↑(basicOpen 𝒜 r) : Scheme))
    (fromOfGlobalSections 𝒜 f hf ∣_ basicOpen 𝒜 r) (Iso.hom (X.isoOfEq ⋯) ≫ toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr)
have rw : Eq (α := (↑(X.basicOpen (U := ⊤) ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) r)) : Scheme) ⟶ Proj 𝒜)
  ((Iso.inv (X.isoOfEq sorry) ≫ fromOfGlobalSections 𝒜 f hf ∣_ basicOpen 𝒜 r) ≫ Scheme.Opens.ι (basicOpen 𝒜 r))
  (toBasicOpenOfGlobalSections 𝒜 f sorry hn hr ≫ Scheme.Opens.ι (basicOpen 𝒜 r))
Tactic: rw [← Iso.inv_comp_eq, ← cancel_mono (basicOpen 𝒜 r).ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ Eq (α := (↑(X.basicOpen (U := ⊤) ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) r)) : Scheme) ⟶ Proj 𝒜)
    ((Iso.inv (X.isoOfEq ⋯) ≫ fromOfGlobalSections 𝒜 f hf ∣_ basicOpen 𝒜 r) ≫ Scheme.Opens.ι (basicOpen 𝒜 r))
    (toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr ≫ Scheme.Opens.ι (basicOpen 𝒜 r))
have simp : (X.basicOpen (U := ⊤) ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) r)).ι ≫
    Scheme.Cover.glueMorphisms (openCoverOfMapIrrelevantEqTop 𝒜 f hf)
      (fun (ri : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀) ↦
        toBasicOpenOfGlobalSections 𝒜 f sorry sorry sorry ≫
          Scheme.Opens.ι
            (basicOpen 𝒜
              (ri.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                0 < ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                  r ∈ 𝒜 (ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))))))
      sorry =
  toBasicOpenOfGlobalSections 𝒜 f sorry hn hr ≫ Scheme.Opens.ι (basicOpen 𝒜 r)
Tactic: simp only [Scheme.isoOfEq_inv, Category.assoc, morphismRestrict_ι, Scheme.homOfLE_ι_assoc,
    fromOfGlobalSections]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ Eq (α := (↑(X.basicOpen (U := ⊤) ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) r)) : Scheme) ⟶ (↑(basicOpen 𝒜 r) : Scheme))
    (Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r)
      (X.basicOpen (U := ⊤) ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) r)) ⋯)
    (toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr)
have rw : Eq (α := (↑(X.basicOpen (U := ⊤) ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) r)) : Scheme) ⟶ (↑(basicOpen 𝒜 r) : Scheme))
  (Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r)
    (X.basicOpen (U := ⊤) ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) r)) sorry)
  (Iso.inv (X.isoOfEq sorry) ≫
    Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r) sorry)
Tactic: rw [← (Iso.inv_comp_eq _).mpr (fromOfGlobalSections_morphismRestrict 𝒜 f hf hn hr),
    ← Scheme.Hom.resLE_eq_morphismRestrict]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
⊢ Eq (α := X ⟶ Spec (CommRingCat.of ↥(𝒜 0))) (fromOfGlobalSections 𝒜 f hf ≫ toSpecZero 𝒜)
    (X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A))))
have refine : ∀ (x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀),
  Eq (α := (openCoverOfMapIrrelevantEqTop 𝒜 f hf).X x ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x ≫ fromOfGlobalSections 𝒜 f hf ≫ toSpecZero 𝒜)
    ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x ≫
      X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A))))
Tactic: refine (openCoverOfMapIrrelevantEqTop 𝒜 f hf).hom_ext _ _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
⊢ Continuous (X := ProjectiveSpectrum ℬ) (Y := ProjectiveSpectrum 𝒜)
    (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
have simp_rw : ∀ (a : Set A),
  ∃ (s : Set B),
    Eq (α := Set (ProjectiveSpectrum ℬ))
      (Set.preimage (β := ProjectiveSpectrum 𝒜) (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
          (zeroLocus 𝒜 a : Set (ProjectiveSpectrum 𝒜)) :
        Set (ProjectiveSpectrum ℬ))
      (zeroLocus ℬ s : Set (ProjectiveSpectrum ℬ))
Tactic: simp_rw [continuous_iff_isClosed, isClosed_iff_zeroLocus, exists_imp, forall_eq_apply_imp_iff]