-- 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 :
  Membership.mem (α := A) I
    ((GradedRing.proj 𝒜 j : (a : A) → A)
        ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) *
          x) :
      A)
rw₁ :
  Membership.mem (α := A) I
    ((GradedRing.proj 𝒜 j : (a : A) → A)
        (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * x) :
      A)
rw₂ rw₃ 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
a a₁ :
  ∀ (k : ι),
    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)
a₂ :
  ∀ (k : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) k →
      ∀ (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)
a₃ :
  ∀ (k : ι),
    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)),
        Membership.mem (α := A) I
          ((GradedRing.proj 𝒜 j : (a : A) → A)
              ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) *
                x) :
            A)
a₄ :
  ∀ (k : ι),
    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)),
        (↑(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
pos :
  ∀ (k : ι),
    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)),
        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 neg₁ :
  ∀ (k : ι),
    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)),
        ¬k + i = j → (↑0 : A) ∈ I
⊢ Membership.mem (α := A) I ((GradedRing.proj 𝒜 j : (a : A) → A) (r * x) : A)

Tactic:
classical
  rw [← DirectSum.sum_support_decompose 𝒜 r, Finset.sum_mul, map_sum]
  apply Ideal.sum_mem
  intro k _
  obtain ⟨i, hi⟩ := hx₁
  have mem₁ : (DirectSum.decompose 𝒜 r k : A) * x ∈ 𝒜 (k + i) :=
    GradedMul.mul_mem (SetLike.coe_mem _) hi
  rw [GradedRing.proj_apply, DirectSum.decompose_of_mem 𝒜 mem₁, coe_of_apply]
  split_ifs
  · exact I.mul_mem_left _ hx₂
  · exact I.zero_mem

Premises used: Ideal.sum_mem, map_sum, Ideal.zero_mem, DirectSum.coe_of_apply, Ideal.mul_mem_left, Finset.sum_mul, GradedRing.proj_apply