awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
n : (i : S) → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
refine : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) ⊤
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, ∃ (n : ι), n ≠ 0 ∧ i ∈ 𝒜 n

Tactic:
refine ⟨s.filter (n · ≠ 0), ?_, by simpa using fun i hi hin ↦ ⟨n i, hin, hn i hi⟩⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
n : (i : S) → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
rw : (↑s : Set S) ⊆ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)
⊢ Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) ⊤

Tactic:
rw [← top_le_iff, ← h₁, Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff, top_le_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
n : (i : S) → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
i : S
hi : i ∈ (↑s : Set S)
pos : ∀ (hi0 : n i = 0), i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)
neg : ∀ (hi0 : ¬n i = 0), i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)
⊢ i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)

Tactic:
by_cases hi0 : n i = 0
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
n : (i : S) → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
i : S
hi : i ∈ (↑s : Set S)
hi0 : n i = 0
⊢ i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)

Tactic:
Subalgebra.algebraMap_mem
      (Algebra.adjoin (𝒜 0) (s.filter (n · ≠ 0) : Set S)) ⟨i, hi0 ▸ hn i hi⟩

Premises used: Set.Mem, Algebra.adjoin, Membership.mem, Eq.rec, Subtype, Ne, Subtype.mk, SetLike.coe, Subalgebra.algebraMap_mem, OfNat.ofNat, Finset.filter
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
n : (i : S) → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
i : S
hi : i ∈ (↑s : Set S)
hi0 : n i = 0
⊢ i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)

Tactic:
exact Subalgebra.algebraMap_mem
      (Algebra.adjoin (𝒜 0) (s.filter (n · ≠ 0) : Set S)) ⟨i, hi0 ▸ hn i hi⟩

Premises used: Algebra.adjoin, Membership.mem, Eq.rec, Subtype, Ne, Subtype.mk, SetLike.coe, Subalgebra.algebraMap_mem, OfNat.ofNat, Finset.filter
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
n : (i : S) → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
i : S
hi : i ∈ (↑s : Set S)
hi0 : ¬n i = 0
⊢ i ∈ (↑({x ∈ s | n x ≠ 0}) : Set S)

Tactic:
simpa [hi0] using hi
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
n : (i : S) → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
i : S
hi : i ∈ (↑s : Set S)
hi0 : ¬n i = 0
⊢ i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)

Tactic:
exact Algebra.subset_adjoin (by simpa [hi0] using hi)

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
x : A
⊢ x ∈ I ↔
    ∀ (i : ι), (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ I

Tactic:
AddSubmonoidClass.IsHomogeneous.mem_iff 𝒜 _ hI

Premises used: Set.Mem, DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ (↑I.toIdeal : Set A) = (↑I : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ Ideal.IsHomogeneous 𝒜 I.toIdeal

Tactic:
I.is_homogeneous'

Premises used: HomogeneousSubmodule.is_homogeneous'
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
⊢ Function.Injective (α := HomogeneousIdeal 𝒜) toIdeal

Tactic:
HomogeneousSubmodule.toSubmodule_injective 𝒜 𝒜

Premises used: HomogeneousSubmodule.toSubmodule_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I J : HomogeneousIdeal 𝒜
⊢ I.toIdeal ≤ J.toIdeal ↔ I ≤ J

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I J : HomogeneousIdeal 𝒜
h : I.toIdeal = J.toIdeal
⊢ I = J

Tactic:
HomogeneousIdeal.toIdeal_injective h

Premises used: HomogeneousIdeal.toIdeal_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I J : HomogeneousIdeal 𝒜
h : ∀ (i : ι), ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J
⊢ I = J

Tactic:
HomogeneousSubmodule.ext' 𝒜 𝒜 h

Premises used: HomogeneousSubmodule.ext'
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
x : A
⊢ x ∈ I.toIdeal ↔ x ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
⊢ Monotone (α := Ideal A) (homogeneousCore' 𝒜)

Tactic:
fun _ _ I_le_J => Ideal.span_mono <| Set.image_mono fun _ => @I_le_J _

Premises used: Set.Mem, Set.image_mono, Monotone, Ideal.span_mono
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
𝒜 : ι → σ
I : Ideal A
⊢ homogeneousCore' 𝒜 I ≤ I

Tactic:
Ideal.span_le.2 <| image_preimage_subset _ _

Premises used: Ideal.span_le, Iff.mpr, Set.Mem, Set.image_preimage_subset
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
⊢ IsHomogeneous 𝒜 I ↔ ∀ (i : ι), (↑I : Set A) ⊆ (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) ⁻¹' (↑I : Set A)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset, Set.preimage, DirectSum.SetLike.IsHomogeneous, Submodule.IsHomogeneous
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
⊢ IsHomogeneous 𝒜 I ↔ (↑I : Set A) ⊆ ⋂ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) ⁻¹' (↑I : Set A)

Tactic:
subset_iInter_iff.symm

Premises used: Set.subset_iInter_iff, Set.Mem, setOf, Set.Subset, Set.preimage, DirectSum.SetLike.IsHomogeneous, Submodule.IsHomogeneous, Iff.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₁ : IsHomogeneousElem 𝒜 x
hx₂ : x ∈ I
j : ι
rw :
  ∑ x_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r),
      (GradedRing.proj 𝒜 j : (a : A) → A)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x_1) : A) * x) ∈
    I
⊢ Membership.mem (α := A) I ((GradedRing.proj 𝒜 j : (a : A) → A) (r * x) : A)

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 r, Finset.sum_mul, map_sum]

Premises used: map_sum, DirectSum.sum_support_decompose, Finset.sum_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₁ : IsHomogeneousElem 𝒜 x
hx₂ : x ∈ I
j : ι
a :
  ∀ (c : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) c →
      Membership.mem (α := A) I
        ((GradedRing.proj 𝒜 j : (a : A) → A)
            ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) c) : A) * x) :
          A)
⊢ ∑ x_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r),
      (GradedRing.proj 𝒜 j : (a : A) → A)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x_1) : A) * x) ∈
    I

Tactic:
apply Ideal.sum_mem

Premises used: Ideal.sum_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₁ : IsHomogeneousElem 𝒜 x
hx₂ : x ∈ I
j k : ι
a :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k →
    Membership.mem (α := A) I
      ((GradedRing.proj 𝒜 j : (a : A) → A)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x) :
        A)
⊢ Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k →
    Membership.mem (α := A) I
      ((GradedRing.proj 𝒜 j : (a : A) → A)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x) :
        A)

Tactic:
_
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₁ : IsHomogeneousElem 𝒜 x
hx₂ : x ∈ I
j k : ι
h :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k
a :
  ∀ (i : ι) (hi : x ∈ 𝒜 i),
    Membership.mem (α := A) I
      ((GradedRing.proj 𝒜 j : (a : A) → A)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x) :
        A)
⊢ Membership.mem (α := A) I
    ((GradedRing.proj 𝒜 j : (a : A) → A)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x) :
      A)

Tactic:
obtain ⟨i, hi⟩ := hx₁
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
h :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k
i : ι
hi : x ∈ 𝒜 i
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x ∈ 𝒜 (k + i)

Tactic:
have mem₁ : (DirectSum.decompose 𝒜 r k : A) * x ∈ 𝒜 (k + i) :=
    GradedMul.mul_mem (SetLike.coe_mem _) hi
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
h :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k
i : ι
hi : x ∈ 𝒜 i
mem₁ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x ∈ 𝒜 (k + i)
a :
  (↑(if k + i = j then
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (k + i))
            ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x)
            mem₁
        else 0) :
      A) ∈
    I
⊢ Membership.mem (α := A) I
    ((GradedRing.proj 𝒜 j : (a : A) → A)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x) :
      A)

Tactic:
rw [GradedRing.proj_apply, DirectSum.decompose_of_mem 𝒜 mem₁, coe_of_apply]

Premises used: DirectSum.decompose_of_mem, DirectSum.coe_of_apply, GradedRing.proj_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
h :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k
i : ι
hi : x ∈ 𝒜 i
mem₁ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x ∈ 𝒜 (k + i)
pos :
  k + i = j →
    (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (k + i))
            ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x)
            mem₁) :
        A) ∈
      I
neg : ¬k + i = j → (↑0 : A) ∈ I
⊢ (↑(if k + i = j then
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (k + i))
            ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x)
            mem₁
        else 0) :
      A) ∈
    I

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
h :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k
i : ι
hi : x ∈ 𝒜 i
mem₁ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x ∈ 𝒜 (k + i)
h_1 : k + i = j
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (k + i))
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x)
          mem₁) :
      A) ∈
    I

Tactic:
I.mul_mem_left _ hx₂

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
h :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k
i : ι
hi : x ∈ 𝒜 i
mem₁ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x ∈ 𝒜 (k + i)
h_1 : k + i = j
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (k + i))
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x)
          mem₁) :
      A) ∈
    I

Tactic:
exact I.mul_mem_left _ hx₂

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
h :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k
i : ι
hi : x ∈ 𝒜 i
mem₁ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x ∈ 𝒜 (k + i)
h_1 : ¬k + i = j
⊢ (↑0 : A) ∈ I

Tactic:
I.zero_mem

Premises used: Set.Mem, Ideal.zero_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
h :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k
i : ι
hi : x ∈ 𝒜 i
mem₁ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x ∈ 𝒜 (k + i)
h_1 : ¬k + i = j
⊢ (↑0 : A) ∈ I

Tactic:
exact I.zero_mem

Premises used: Ideal.zero_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
r : A
hr : Membership.mem (γ := Submodule A A) (span s) r
⊢ Membership.mem (γ := Submodule A A)
    (LinearMap.range (M := { x : A // x ∈ s } →₀ A)
      (Finsupp.linearCombination A (Subtype.val (p := fun (x : A) ↦ x ∈ s))))
    r

Tactic:
rw [Ideal.span, Finsupp.span_eq_range_linearCombination] at hr

Premises used: Finsupp.span_eq_range_linearCombination, Ideal.span
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
r : A
hr :
  Membership.mem (γ := Submodule A A)
    (LinearMap.range (M := { x : A // x ∈ s } →₀ A)
      (Finsupp.linearCombination A (Subtype.val (p := fun (x : A) ↦ x ∈ s))))
    r
⊢ ∃ (y : { x : A // x ∈ s } →₀ A),
    (Finsupp.linearCombination A (Subtype.val (p := fun (x : A) ↦ x ∈ s)) : (a : { x : A // x ∈ s } →₀ A) → A) y = r

Tactic:
rw [LinearMap.mem_range] at hr

Premises used: LinearMap.mem_range
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
r : A
hr :
  ∃ (y : { x : A // x ∈ s } →₀ A),
    (Finsupp.linearCombination A (Subtype.val (p := fun (x : A) ↦ x ∈ s)) : (a : { x : A // x ∈ s } →₀ A) → A) y = r
obtain :
  ∀ (s_1 : { x : A // x ∈ s } →₀ A),
    Membership.mem (γ := Submodule A A) (span s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                  ((Finsupp.linearCombination A (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
                      (a : { x : A // x ∈ s } →₀ A) → A)
                    s_1) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A)
⊢ Membership.mem (γ := Submodule A A) (span s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
obtain ⟨s, rfl⟩ := hr

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
rw :
  Membership.mem (γ := Submodule A A) (span s_1)
    (∑ i_1 ∈ s.support,
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                  (HSMul.hSMul (α := A) ((s : (a : { x : A // x ∈ s_1 }) → A) i_1 : A) (↑i_1 : A)) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))
⊢ Membership.mem (γ := Submodule A A) (span s_1)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                ((Finsupp.linearCombination A (Subtype.val (p := fun (x : A) ↦ x ∈ s_1)) :
                    (a : { x : A // x ∈ s_1 } →₀ A) → A)
                  s) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum, decompose_sum, DFinsupp.finsetSum_apply,
    AddSubmonoidClass.coe_finsetSum]

Premises used: DFinsupp.finsetSum_apply, Finsupp.sum, AddSubmonoidClass.coe_finsetSum, Finsupp.linearCombination_apply, DirectSum.decompose_sum
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
⊢ Membership.mem (γ := Submodule A A) (span s_1)
    (∑ i_1 ∈ s.support,
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                  (HSMul.hSMul (α := A) ((s : (a : { x : A // x ∈ s_1 }) → A) i_1 : A) (↑i_1 : A)) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))

Tactic:
Ideal.sum_mem _ ?_

Premises used: Set.Mem, Ideal.sum_mem