ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
i : ι
r : A
hr : r ∈ span s
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ span s
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
⊢ IsHomogeneous 𝒜 (span s)
rintro i r hr
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
i : ι
r : A
hr : r ∈ LinearMap.range (Finsupp.total (↑s) A A Subtype.val)
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ span s
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
i : ι
r : A
hr : r ∈ span s
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ span s
rw [Ideal.span, Finsupp.span_eq_range_total] at hr
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
i : ι
r : A
hr : ∃ y, ↑(Finsupp.total (↑s) A A Subtype.val) y = r
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ span s
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
i : ι
r : A
hr : r ∈ LinearMap.range (Finsupp.total (↑s) A A Subtype.val)
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ span s
rw [LinearMap.mem_range] at hr
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
⊢ ↑(↑(↑(decompose 𝒜) (↑(Finsupp.total (↑s✝) A A Subtype.val) s)) i) ∈ span s✝
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
i : ι
r : A
hr : ∃ y, ↑(Finsupp.total (↑s) A A Subtype.val) y = r
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ span s
obtain ⟨s, rfl⟩ := hr
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
⊢ ∑ i_1 in s.support, ↑(↑(↑(decompose 𝒜) (↑s i_1 • ↑i_1)) i) ∈ span s✝
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
⊢ ↑(↑(↑(decompose 𝒜) (↑(Finsupp.total (↑s✝) A A Subtype.val) s)) i) ∈ span s✝
rw [Finsupp.total_apply, Finsupp.sum, decompose_sum, Dfinsupp.finset_sum_apply,
  AddSubmonoidClass.coe_finset_sum]
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
⊢ ∀ (c : ↑s✝), c ∈ s.support → ↑(↑(↑(decompose 𝒜) (↑s c • ↑c)) i) ∈ span s✝
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
⊢ ∑ i_1 in s.support, ↑(↑(↑(decompose 𝒜) (↑s i_1 • ↑i_1)) i) ∈ span s✝
refine' Ideal.sum_mem _ _
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ ↑(↑(↑(decompose 𝒜) (↑s z • ↑z)) i) ∈ span s✝
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
⊢ ∀ (c : ↑s✝), c ∈ s.support → ↑(↑(↑(decompose 𝒜) (↑s c • ↑c)) i) ∈ span s✝
rintro z hz1
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ ↑(↑(↑(decompose 𝒜) (↑s z * ↑z)) i) ∈ span s✝
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ ↑(↑(↑(decompose 𝒜) (↑s z • ↑z)) i) ∈ span s✝
rw [smul_eq_mul]
case intro.refine'_1
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ Homogeneous 𝒜 ↑z

case intro.refine'_2
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ ↑z ∈ span s✝
case intro
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ ↑(↑(↑(decompose 𝒜) (↑s z * ↑z)) i) ∈ span s✝
refine' Ideal.mul_homogeneous_element_mem_of_mem 𝒜 (s z) z _ _ i
case intro.refine'_1.mk
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : A
hz2 : z ∈ s✝
hz1 : { val := z, property := hz2 } ∈ s.support
⊢ Homogeneous 𝒜 ↑{ val := z, property := hz2 }
case intro.refine'_1
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ Homogeneous 𝒜 ↑z
rcases z with ⟨z, hz2⟩
no goals
case intro.refine'_1.mk
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : A
hz2 : z ∈ s✝
hz1 : { val := z, property := hz2 } ∈ s.support
⊢ Homogeneous 𝒜 ↑{ val := z, property := hz2 }
apply h _ hz2
no goals
case intro.refine'_2
ι : Type u_2
σ : Type u_3
R : Type ?u.93837
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ ↑z ∈ span s✝
exact Ideal.subset_span z.2