awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
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)
⊢ i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)
have pos : ∀ (hi0 : n i = 0), i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)
Tactic: by_cases hi0 : n i = 0
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
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)
⊢ i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)
have neg : ∀ (hi0 : ¬n i = 0), i ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)
Tactic: by_cases hi0 : n i = 0
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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 : ι
⊢ Membership.mem (α := A) I ((GradedRing.proj 𝒜 j : (a : A) → A) (r * x) : A)
have 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
Tactic: rw [← DirectSum.sum_support_decompose 𝒜 r, Finset.sum_mul, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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 : ι
⊢ ∑ 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
have 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)
Tactic: apply Ideal.sum_mem
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ Membership.mem (α := A) I
    ((GradedRing.proj 𝒜 j : (a : A) → A)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x) :
      A)
have 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)
Tactic: obtain ⟨i, hi⟩ := hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (hypothesis)
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
⊢ Membership.mem (α := A) I
    ((GradedRing.proj 𝒜 j : (a : A) → A)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x) :
      A)
have mem₁ : (↑((((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
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ Membership.mem (α := A) I
    ((GradedRing.proj 𝒜 j : (a : A) → A)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k) : A) * x) :
      A)
have 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
Tactic: rw [GradedRing.proj_apply, DirectSum.decompose_of_mem 𝒜 mem₁, coe_of_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ (↑(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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ (↑(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
have neg : ¬k + i = j → (↑0 : A) ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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 : ι
⊢ Membership.mem (α := A) I ((GradedRing.proj 𝒜 j : (a : A) → A) (r * x) : A)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ Membership.mem (α := A) I ((GradedRing.proj 𝒜 j : (a : A) → A) (r * x) : A)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ Membership.mem (α := A) I ((GradedRing.proj 𝒜 j : (a : A) → A) (r * x) : A)
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ Membership.mem (α := A) I ((GradedRing.proj 𝒜 j : (a : A) → A) (r * x) : A)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ Membership.mem (α := A) I ((GradedRing.proj 𝒜 j : (a : A) → A) (r * x) : A)
have 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)
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
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ Membership.mem (α := A) I ((GradedRing.proj 𝒜 j : (a : A) → A) (r * x) : A)
have 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)
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
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (hypothesis)
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) (span s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have 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
Tactic: rw [Ideal.span, Finsupp.span_eq_range_linearCombination] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (hypothesis)
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
⊢ Membership.mem (γ := Submodule A A) (span s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have 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
Tactic: rw [LinearMap.mem_range] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ Membership.mem (γ := Submodule A A) (span s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have 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)
Tactic: obtain ⟨s, rfl⟩ := hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
    (↑((((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)
have 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))
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum, decompose_sum, DFinsupp.finsetSum_apply,
    AddSubmonoidClass.coe_finsetSum]