awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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

Tactic:
have : c ≠ 0 := by contrapose hc; simpa [hc] using hx
-- 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_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
this : c ≠ 0
⊢ ((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
          (a : ℕ) → ↥(𝒜 a))
        c).1 ∈
    𝒜 c

Tactic:
simp
-- 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_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
this : c ≠ 0
⊢ 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)

Tactic:
exact Ideal.subset_span ⟨⟨c, _, this.bot_lt, by simp⟩, rfl⟩
-- 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 𝒜))) ⊤
⊢ 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⟩
-- 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 𝒜))) ⊤
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 𝒜))
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)
⊢ 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:
ext1
-- 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 𝒜))) ⊤
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 𝒜))
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)ᶜ
⊢ (↑(⨆ (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

Premises used: compl_injective
-- 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 𝒜))) ⊤
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 𝒜))
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))))) =
    ∅
⊢ (↑(⨆ (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:
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]

Premises used: TopologicalSpace.Opens.coe_iSup, AlgebraicGeometry.Scheme.zeroLocus_iUnion, AlgebraicGeometry.Scheme.zeroLocus_singleton, Set.iUnion_singleton_eq_range, Set.compl_univ, Set.compl_iUnion, TopologicalSpace.Opens.coe_top
-- 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 𝒜))) ⊤
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 𝒜))
h : X.zeroLocus (↑⊤ : Set (↑Γ(X, ⊤) : Type u)) = ∅
⊢ 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:
rw [← Scheme.zeroLocus_span, Set.range_comp', ← Ideal.map_span, H, hf]

Premises used: Ideal.map_span, AlgebraicGeometry.Scheme.zeroLocus_span, Set.range_comp'
-- 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 𝒜))) ⊤
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)) = ∅

Tactic:
simp
-- 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 𝒜))) ⊤
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 ⋯ ⋯ ⋯ ≫
                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 ⋯ ⋯ ⋯ ≫
                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)
⊢ X ⟶ Proj 𝒜

Tactic:
refine (openCoverOfMapIrrelevantEqTop 𝒜 f hf).glueMorphisms
    (fun ri ↦ toBasicOpenOfGlobalSections 𝒜 f rfl ri.2.2.1 ri.2.2.2 ≫ Scheme.Opens.ι _) ?_

Premises used: PSigma.snd, AlgebraicGeometry.Proj.basicOpen, And.right, And.left, AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections, AlgebraicGeometry.Scheme.Cover.glueMorphisms, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Opens.ι, PSigma.fst, rfl, AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTop
-- 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_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 y : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ (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))))))
        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))))))
        y =
    X.basicOpen (U := ⊤)
      ((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))) *
          y.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
            0 < y.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
              r ∈ 𝒜 (y.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))

Tactic:
simp
-- 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 : 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
rw :
  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))
⊢ Eq (α := (↑(fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r) : Scheme) ⟶ (↑(basicOpen 𝒜 r) : Scheme))
    (fromOfGlobalSections 𝒜 f hf ∣_ basicOpen 𝒜 r) (Iso.hom (X.isoOfEq ⋯) ≫ toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr)

Tactic:
rw [← Iso.inv_comp_eq, ← cancel_mono (basicOpen 𝒜 r).ι]

Premises used: CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.Proj.basicOpen, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- 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 : 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
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 ⋯ ⋯ ⋯ ≫
            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))))))
        ⋯ =
    toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr ≫ Scheme.Opens.ι (basicOpen 𝒜 r)
⊢ 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))

Tactic:
simp only [Scheme.isoOfEq_inv, Category.assoc, morphismRestrict_ι, Scheme.homOfLE_ι_assoc,
    fromOfGlobalSections]

Premises used: AlgebraicGeometry.Scheme.isoOfEq_inv, CategoryTheory.Category.assoc, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.homOfLE_ι_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections
-- 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 : 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
⊢ (X.basicOpen (U := ⊤) ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) r)).ι ≫
      Scheme.Cover.glueMorphisms (openCoverOfMapIrrelevantEqTop 𝒜 f hf)
        (fun (ri : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀) ↦
          toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫
            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))))))
        ⋯ =
    toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr ≫ Scheme.Opens.ι (basicOpen 𝒜 r)

Tactic:
(openCoverOfMapIrrelevantEqTop 𝒜 f hf).ι_glueMorphisms _ _ ⟨_, _, hn, hr⟩

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, And.intro, PSigma.mk, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTop
-- 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 : 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
⊢ (X.basicOpen (U := ⊤) ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) r)).ι ≫
      Scheme.Cover.glueMorphisms (openCoverOfMapIrrelevantEqTop 𝒜 f hf)
        (fun (ri : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀) ↦
          toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫
            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))))))
        ⋯ =
    toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr ≫ Scheme.Opens.ι (basicOpen 𝒜 r)

Tactic:
exact (openCoverOfMapIrrelevantEqTop 𝒜 f hf).ι_glueMorphisms _ _ ⟨_, _, hn, hr⟩

Premises used: AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, And.intro, PSigma.mk, AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTop
-- 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 : 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
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)) ⋯)
    (Iso.inv (X.isoOfEq ⋯) ≫
      Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r) ⋯)
⊢ 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)

Tactic:
rw [← (Iso.inv_comp_eq _).mpr (fromOfGlobalSections_morphismRestrict 𝒜 f hf hn hr),
    ← Scheme.Hom.resLE_eq_morphismRestrict]

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict
-- 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 : 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)) ⋯)
    (Iso.inv (X.isoOfEq ⋯) ≫
      Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r) ⋯)

Tactic:
simp [Scheme.isoOfEq_inv]

Premises used: AlgebraicGeometry.Scheme.isoOfEq_inv