case a
ι : Type u_2
σ : Type u_3
R : Type ?u.210738
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
I_le_J : I ≤ J
⊢ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} ⊆ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r}
ι : Type u_2
σ : Type u_3
R : Type ?u.210738
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
I_le_J : I ≤ J
⊢ homogeneousHull 𝒜 I ≤ homogeneousHull 𝒜 J
apply Ideal.span_mono
case a.intro.intro.mk
ι : Type u_2
σ : Type u_3
R : Type ?u.210738
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
I_le_J : I ≤ J
hr1 : ι
x : A
hx : x ∈ I
⊢ ↑(↑(↑(decompose 𝒜) ↑{ val := x, property := hx }) hr1) ∈ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r}
case a
ι : Type u_2
σ : Type u_3
R : Type ?u.210738
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
I_le_J : I ≤ J
⊢ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} ⊆ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r}
rintro r ⟨hr1, ⟨x, hx⟩, rfl⟩
no goals
case a.intro.intro.mk
ι : Type u_2
σ : Type u_3
R : Type ?u.210738
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
I_le_J : I ≤ J
hr1 : ι
x : A
hx : x ∈ I
⊢ ↑(↑(↑(decompose 𝒜) ↑{ val := x, property := hx }) hr1) ∈ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r}
refine' ⟨hr1, ⟨⟨x, I_le_J hx⟩, rfl⟩⟩