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 : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
e_a :
  Eq (α := Away 𝒜 t →+* Localization.Away x')
    (@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
      (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
        (IsLocalization.map (Localization.Away x) f ⋯) (algebraMap (Away 𝒜 t) (Localization.Away t))))
    (@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (Localization.Away x') f ⋯)
      (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs ⋯)))
⊢ Eq (α := Spec (CommRingCat.of (Localization.Away x')) ⟶ Proj 𝒜)
    (Spec.map
        (CommRingCat.ofHom
          (@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
            (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
              (IsLocalization.map (Localization.Away x) f ⋯) (algebraMap (Away 𝒜 t) (Localization.Away t))))) ≫
      awayι 𝒜 t hd h0d)
    (Spec.map
        (CommRingCat.ofHom
          (@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.map (Localization.Away x') f ⋯)
            (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs ⋯)))) ≫
      awayι 𝒜 t hd h0d)

Tactic:
congr 3
-- 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)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
e_a :
  ∀ (x_1 : Away 𝒜 t),
    Eq (α := Localization.Away x')
      ((@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
              (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
              (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
                (IsLocalization.map (Localization.Away x) f ⋯) (algebraMap (Away 𝒜 t) (Localization.Away t))) :
            (a : Away 𝒜 t) → Localization.Away x')
          x_1 :
        Localization.Away x')
      ((@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
              (IsLocalization.map (Localization.Away x') f ⋯)
              (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs ⋯)) :
            (a : Away 𝒜 t) → Localization.Away x')
          x_1 :
        Localization.Away x')
⊢ Eq (α := Away 𝒜 t →+* Localization.Away x')
    (@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
      (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
        (IsLocalization.map (Localization.Away x) f ⋯) (algebraMap (Away 𝒜 t) (Localization.Away t))))
    (@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (Localization.Away x') f ⋯)
      (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs ⋯)))

Tactic:
ext
-- 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)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
e_a :
  Eq (α := Localization.Away x')
    ((IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s) :
          (a : Localization.Away x) → Localization.Away x')
        ((IsLocalization.map (Localization.Away x) f ⋯ : (a : Localization.Away t) → Localization.Away x) (val x_1)) :
      Localization.Away x')
    ((IsLocalization.map (Localization.Away x') f ⋯ : (a : Localization.Away (t * s)) → Localization.Away x')
        ((Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯ :
            (a : Localization.Away t) → Localization (Submonoid.powers (t * s)))
          (val x_1)) :
      Localization.Away x')
⊢ Eq (α := Localization.Away x')
    ((@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
            (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
              (IsLocalization.map (Localization.Away x) f ⋯) (algebraMap (Away 𝒜 t) (Localization.Away t))) :
          (a : Away 𝒜 t) → Localization.Away x')
        x_1 :
      Localization.Away x')
    ((@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.map (Localization.Away x') f ⋯)
            (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs ⋯)) :
          (a : Away 𝒜 t) → Localization.Away x')
        x_1 :
      Localization.Away x')

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply,
    HomogeneousLocalization.algebraMap_apply, HomogeneousLocalization.val_awayMap]

Premises used: HomogeneousLocalization.val_awayMap, RingHom.coe_comp, Function.comp_apply, HomogeneousLocalization.algebraMap_apply
-- 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)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
e_a :
  Eq (α := Localization.Away x')
    ((@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
            (IsLocalization.map (Localization.Away x) f ⋯) :
          (a : Localization.Away t) → Localization.Away x')
        (val x_1) :
      Localization.Away x')
    ((RingHom.comp (IsLocalization.map (Localization.Away x') f ⋯)
            (Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯) :
          (a : Localization.Away t) → Localization.Away x')
        (val x_1) :
      Localization.Away x')
⊢ Eq (α := Localization.Away x')
    ((IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s) :
          (a : Localization.Away x) → Localization.Away x')
        ((IsLocalization.map (Localization.Away x) f ⋯ : (a : Localization.Away t) → Localization.Away x) (val x_1)) :
      Localization.Away x')
    ((IsLocalization.map (Localization.Away x') f ⋯ : (a : Localization.Away (t * s)) → Localization.Away x')
        ((Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯ :
            (a : Localization.Away t) → Localization (Submonoid.powers (t * s)))
          (val x_1)) :
      Localization.Away x')

Tactic:
simp only [← RingHom.comp_apply]

Premises used: RingHom.comp_apply
-- 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)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := Localization.Away x')
    ((@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
            (IsLocalization.map (Localization.Away x) f ⋯) :
          (a : Localization.Away t) → Localization.Away x')
        (val x_1) :
      Localization.Away x')
    ((RingHom.comp (IsLocalization.map (Localization.Away x') f ⋯)
            (Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯) :
          (a : Localization.Away t) → Localization.Away x')
        (val x_1) :
      Localization.Away x')

Tactic:
congr 1
-- 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)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply IsLocalization.ringHom_ext (M := .powers t)

Premises used: Submonoid.powers, IsLocalization.ringHom_ext
-- 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)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext i
-- 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)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
i : A
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [IsLocalization.Away.awayToAwayRight_eq]

Premises used: IsLocalization.Away.awayToAwayRight_eq
-- 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 𝒜))) ⊤
a :
  LE.le (α := 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 𝒜))
a₁ :
  LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
    (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)))))
⊢ 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:
apply le_antisymm

Premises used: le_antisymm
-- 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 𝒜))) ⊤
a :
  ∀ (y : (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))) ∈
      (↑(HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) : Set A)
⊢ LE.le (α := 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:
rw [Ideal.span_le, Set.range_subset_iff]

Premises used: Ideal.span_le, Set.range_subset_iff
-- 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 𝒜))) ⊤
i : ℕ
r : A
hi0 : 0 < i
hri : r ∈ 𝒜 i
⊢ PSigma.fst (β := fun (r_1 : A) ↦
      0 <
          PSigma.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)
            (PSigma.mk (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) i
              (PSigma.mk (β := fun (r : A) ↦ 0 < i ∧ r ∈ 𝒜 i) r ⋯)) ∧
        r_1 ∈
          𝒜
            (PSigma.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)
              (PSigma.mk (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) i
                (PSigma.mk (β := fun (r : A) ↦ 0 < i ∧ r ∈ 𝒜 i) r ⋯))))
      (PSigma.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)
        (PSigma.mk (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) i
          (PSigma.mk (β := fun (r : A) ↦ 0 < i ∧ r ∈ 𝒜 i) r ⋯))) ∈
    (↑(HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) : Set A)

Tactic:
simp [-ZeroMemClass.coe_eq_zero,
          DirectSum.decompose_of_mem_ne 𝒜 hri hi0.ne']

Premises used: ZeroMemClass.coe_eq_zero, LT.lt.ne', DirectSum.decompose_of_mem_ne
-- 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
a :
  Membership.mem (γ := Submodule A 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)))))
    (∑
      i ∈
        DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x),
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            i) :
        A))
⊢ Membership.mem (γ := Submodule A 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)))))
    x

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 x]

Premises used: DirectSum.sum_support_decompose
-- 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
⊢ Membership.mem (γ := Submodule A 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)))))
    (∑
      i ∈
        DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x),
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            i) :
        A))

Tactic:
Ideal.sum_mem _ fun c hc ↦ ?_

Premises used: Set.Mem, Ideal.sum_mem
-- 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
a :
  ∀ (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)
⊢ Membership.mem (γ := Submodule A 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)))))
    (∑
      i ∈
        DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x),
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            i) :
        A))

Tactic:
refine Ideal.sum_mem _ fun c hc ↦ ?_

Premises used: Ideal.sum_mem
-- 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
contrapose :
  ∀ (hc : c = 0),
    c ∉
      DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x)
⊢ c ≠ 0

Tactic:
contrapose hc
-- 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 : c = 0
⊢ c ∉
    DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x)

Tactic:
simpa [hc] using hx