-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem Ideal.le_toIdeal_homogeneousHull : I ≤ (Ideal.homogeneousHull 𝒜 I).toIdeal

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ I ≤ (homogeneousHull 𝒜 I).toIdeal

Tactic:
intro r hr

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ (homogeneousHull 𝒜 I).toIdeal

Proof state:
case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support ((decompose 𝒜) r)
⊢ ↑(((decompose 𝒜) r) j) ∈ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}

Tactic:
use j

Result:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support ((decompose 𝒜) r)
⊢ ∃ x, ↑(((decompose 𝒜) ↑x) j) = ↑(((decompose 𝒜) r) j)

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ ∀ c ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) c) ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
intro j _

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support ((decompose 𝒜) r)
⊢ ↑(((decompose 𝒜) r) j) ∈ (homogeneousHull 𝒜 I).toIdeal

Proof state:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support ((decompose 𝒜) r)
⊢ ∃ x, ↑(((decompose 𝒜) ↑x) j) = ↑(((decompose 𝒜) r) j)

Tactic:
use ⟨r, hr⟩

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support ((decompose 𝒜) r)
⊢ ↑(((decompose 𝒜) r) j) ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
apply Ideal.subset_span

Result:
case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support ((decompose 𝒜) r)
⊢ ↑(((decompose 𝒜) r) j) ∈ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 r]

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) i) ∈ (homogeneousHull 𝒜 I).toIdeal

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
classical
rw [← DirectSum.sum_support_decompose 𝒜 r]
refine Ideal.sum_mem _ ?_
intro j _
apply Ideal.subset_span
use j
use ⟨r, hr⟩

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) i) ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
refine Ideal.sum_mem _ ?_

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ ∀ c ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) c) ∈ (homogeneousHull 𝒜 I).toIdeal