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 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
refine :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x),
    ∃ (i : ι), Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x
refine₁ :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x)
    (H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)), False
refine₂ :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x)
    (H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal), False
refine₃ :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x)
    (H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal), Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤

Tactic:
classical
  refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_
  by_contra! H
  simp only [mem_basicOpen, Decidable.not_not] at H
  refine x.not_irrelevant_le (hf.trans ?_)
  rwa [Ideal.span_le, Set.range_subset_iff]

Premises used: Ideal.span_le, AlgebraicGeometry.Proj.mem_basicOpen, top_le_iff, Iff.mp, Decidable.not_not, 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
hf₁ : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤

Tactic:
apply Proj.iSup_basicOpen_eq_top

Premises used: AlgebraicGeometry.Proj.iSup_basicOpen_eq_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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
h : x = HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
hf₁ :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) x

Tactic:
convert_to x - GradedRing.projZeroRingHom 𝒜 x ∈ _

Premises used: GradedRing.projZeroRingHom, DFunLike.coe
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
h :
  x =
    x -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A)
h₁ : x = HSub.hSub (β := A) x ((GradedRing.proj 𝒜 0 : (a : A) → A) x : A)
h₂ : x = x - 0
h₃ h₄ : x = x
⊢ x = HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)

Tactic:
rw [GradedRing.projZeroRingHom_apply, ← GradedRing.proj_apply,
      (HomogeneousIdeal.mem_irrelevant_iff _ _).mp hx, sub_zero]

Premises used: sub_zero, HomogeneousIdeal.mem_irrelevant_iff, Iff.mp, GradedRing.projZeroRingHom_apply, GradedRing.proj_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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
⊢ Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x

Tactic:
have := (eq_iff_iff.mp congr(x ∈ $hf)).mpr trivial
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x : A
hx : x ∈ Set.range f
hf₁ :
  ∀ (i : ι),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (β := A) (f i) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (f i) : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))

Tactic:
obtain ⟨i, rfl⟩ := hx

Premises used: 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
hf₁ :
  ∀ (n : ℕ) (hn : f i ∈ 𝒜 n),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (β := A) (f i) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (f i) : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (f i) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (f i) : A))

Tactic:
obtain ⟨n, hn⟩ := hfn 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hf₁ :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (f i) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (f i) : A))

Tactic:
rw [GradedRing.projZeroRingHom_apply]

Premises used: GradedRing.projZeroRingHom_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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
pos :
  ∀ (hn' : n = 0),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (f i -
        (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                  DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              0) :
          A))
neg :
  ∀ (hn' : ¬n = 0),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (f i -
        (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                  DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              0) :
          A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))

Tactic:
by_cases hn' : n = 0
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : n = 0
pos : Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) 0
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))

Tactic:
rw [DirectSum.decompose_of_mem_same 𝒜 (hn' ▸ hn), sub_self]

Premises used: DirectSum.decompose_of_mem_same, sub_self
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : n = 0
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : n = 0
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : ¬n = 0
neg : Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) (f i)
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))

Tactic:
rw [DirectSum.decompose_of_mem_ne 𝒜 hn hn', sub_zero]

Premises used: sub_zero, 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : ¬n = 0
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) (f i)

Tactic:
Ideal.subset_span ⟨_, rfl⟩

Premises used: Ideal.subset_span, Set.Mem, Exists.intro, 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : ¬n = 0
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) (f i)

Tactic:
exact Ideal.subset_span ⟨_, 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
r : ↥(𝒜 0)
⊢ Membership.mem (γ := Ideal A) (Ideal.span (Set.range f)) 0

Tactic:
zero_mem (Ideal.span _)

Premises used: Ideal.span, ZeroMemClass.zero_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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
r : ↥(𝒜 0)
h :
  HSub.hSub (α := A) (β := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
      ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A) =
    0
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (α := A) (β := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
      ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A))

Tactic:
convert! zero_mem (Ideal.span _)

Premises used: Ideal.span, ZeroMemClass.zero_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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
r : ↥(𝒜 0)
h :
  Eq (α := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
    ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A)
⊢ HSub.hSub (α := A) (β := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
      ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A) =
    0

Tactic:
rw [sub_eq_zero]

Premises used: sub_eq_zero
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
r : ↥(𝒜 0)
⊢ Eq (α := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
    ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A)

Tactic:
(DirectSum.decompose_of_mem_same 𝒜 r.2).symm

Premises used: DirectSum.decompose_of_mem_same, Eq.symm, Subtype.property
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
r : ↥(𝒜 0)
⊢ Eq (α := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
    ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A)

Tactic:
exact (DirectSum.decompose_of_mem_same 𝒜 r.2).symm

Premises used: DirectSum.decompose_of_mem_same, Eq.symm, Subtype.property
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
h :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
h_1 :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
hf₁ :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A) +
      HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (x + y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x + y) : A))

Tactic:
rw [map_add, add_sub_add_comm]

Premises used: map_add, add_sub_add_comm
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
h :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
h_1 :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A) +
      HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))

Tactic:
add_mem ‹_› ‹_›

Premises used: AddMemClass.add_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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
h :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
h_1 :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A) +
      HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))

Tactic:
exact add_mem ‹_› ‹_›

Premises used: AddMemClass.add_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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
hx' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
hy' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
⊢ Membership.mem (γ := Ideal A) (Ideal.span (Set.range f))
    (x * HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) +
      HMul.hMul (β := A) (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))

Tactic:
add_mem (Ideal.mul_mem_left _ x hy')
        (Ideal.mul_mem_right (GradedRing.projZeroRingHom 𝒜 y) _ hx')

Premises used: Ideal.mul_mem_right, AddMemClass.add_mem, Ideal.mul_mem_left, GradedRing.projZeroRingHom, DFunLike.coe
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
hx' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
hy' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
h :
  HSub.hSub (β := A) (x * y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x * y) : A) =
    x * HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) +
      HMul.hMul (β := A) (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A)
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (x * y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x * y) : A))

Tactic:
convert!
      add_mem (Ideal.mul_mem_left _ x hy')
        (Ideal.mul_mem_right (GradedRing.projZeroRingHom 𝒜 y) _ hx') using 1

Premises used: Ideal.mul_mem_right, AddMemClass.add_mem, Ideal.mul_mem_left, GradedRing.projZeroRingHom, DFunLike.coe
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
hx' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
hy' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
h :
  x * y -
      HMul.hMul (α := A) (β := A) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) =
    x * HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) +
      HMul.hMul (β := A) (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A)
⊢ HSub.hSub (β := A) (x * y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x * y) : A) =
    x * HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) +
      HMul.hMul (β := A) (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A)

Tactic:
rw [map_mul]

Premises used: map_mul