ι : Type u_2
σ : Type u_3
R : Type ?u.216424
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ toIdeal (homogeneousHull 𝒜 I) = span (⋃ (i : ι), ↑(GradedRing.proj 𝒜 i) '' ↑I)
ι : Type u_2
σ : Type u_3
R : Type ?u.216424
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ toIdeal (homogeneousHull 𝒜 I) = ⨆ (i : ι), span (↑(GradedRing.proj 𝒜 i) '' ↑I)
rw [← Ideal.span_iUnion]
ι : Type u_2
σ : Type u_3
R : Type ?u.216424
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} = ⋃ (i : ι), ↑(GradedRing.proj 𝒜 i) '' ↑I
ι : Type u_2
σ : Type u_3
R : Type ?u.216424
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ toIdeal (homogeneousHull 𝒜 I) = span (⋃ (i : ι), ↑(GradedRing.proj 𝒜 i) '' ↑I)
apply congr_arg Ideal.span _
case h
ι : Type u_2
σ : Type u_3
R : Type ?u.216424
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
x✝ : A
⊢ x✝ ∈ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} ↔ x✝ ∈ ⋃ (i : ι), ↑(GradedRing.proj 𝒜 i) '' ↑I
ι : Type u_2
σ : Type u_3
R : Type ?u.216424
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} = ⋃ (i : ι), ↑(GradedRing.proj 𝒜 i) '' ↑I
ext1
no goals
case h
ι : Type u_2
σ : Type u_3
R : Type ?u.216424
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
x✝ : A
⊢ x✝ ∈ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} ↔ x✝ ∈ ⋃ (i : ι), ↑(GradedRing.proj 𝒜 i) '' ↑I
simp only [Set.mem_iUnion, Set.mem_image, mem_setOf_eq, GradedRing.proj_apply, SetLike.exists,
  exists_prop, Subtype.coe_mk, SetLike.mem_coe]