case intro.intro
ι : Type ?u.242952
σ : Type ?u.242955
R : Type ?u.242958
A : Type ?u.242961
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
i : ι
x : A
⊢ Homogeneous 𝒜 (↑(GradedRing.proj 𝒜 i) x)
ι : Type ?u.242952
σ : Type ?u.242955
R : Type ?u.242958
A : Type ?u.242961
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
i : ι
⊢ ∀ (x : A), x ∈ ↑(GradedRing.proj 𝒜 i) '' ↑I → Homogeneous 𝒜 x
rintro _ ⟨x, -, rfl⟩
no goals
case intro.intro
ι : Type ?u.242952
σ : Type ?u.242955
R : Type ?u.242958
A : Type ?u.242961
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
i : ι
x : A
⊢ Homogeneous 𝒜 (↑(GradedRing.proj 𝒜 i) x)
apply SetLike.homogeneous_coe
case h
ι : Type u_2
σ : Type u_3
R : Type ?u.242958
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) =
    toIdeal
      (⨆ (i : ι),
        { toSubmodule := span (↑(GradedRing.proj 𝒜 i) '' ↑I),
          is_homogeneous' := (_ : IsHomogeneous 𝒜 (span (↑(GradedRing.proj 𝒜 i) '' ↑I))) })
ι : Type u_2
σ : Type u_3
R : Type ?u.242958
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ homogeneousHull 𝒜 I =
    ⨆ (i : ι),
      { toSubmodule := span (↑(GradedRing.proj 𝒜 i) '' ↑I),
        is_homogeneous' := (_ : IsHomogeneous 𝒜 (span (↑(GradedRing.proj 𝒜 i) '' ↑I))) }
ext1
case h
ι : Type u_2
σ : Type u_3
R : Type ?u.242958
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (⨆ (i : ι), span (↑(GradedRing.proj 𝒜 i) '' ↑I)) =
    ⨆ (i : ι),
      toIdeal
        { toSubmodule := span (↑(GradedRing.proj 𝒜 i) '' ↑I),
          is_homogeneous' := (_ : IsHomogeneous 𝒜 (span (↑(GradedRing.proj 𝒜 i) '' ↑I))) }
case h
ι : Type u_2
σ : Type u_3
R : Type ?u.242958
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) =
    toIdeal
      (⨆ (i : ι),
        { toSubmodule := span (↑(GradedRing.proj 𝒜 i) '' ↑I),
          is_homogeneous' := (_ : IsHomogeneous 𝒜 (span (↑(GradedRing.proj 𝒜 i) '' ↑I))) })
rw [Ideal.toIdeal_homogeneousHull_eq_iSup, toIdeal_iSup]
no goals
case h
ι : Type u_2
σ : Type u_3
R : Type ?u.242958
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (⨆ (i : ι), span (↑(GradedRing.proj 𝒜 i) '' ↑I)) =
    ⨆ (i : ι),
      toIdeal
        { toSubmodule := span (↑(GradedRing.proj 𝒜 i) '' ↑I),
          is_homogeneous' := (_ : IsHomogeneous 𝒜 (span (↑(GradedRing.proj 𝒜 i) '' ↑I))) }
rfl