awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I J : Ideal A
I_le_J : I ≤ J
hr1 : ι
x : A
hx : x ∈ I
⊢ Membership.mem (γ := Set A)
    {r : A |
      ∃ (i : ι) (x : ↥J),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) = r}
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ I) x hx) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          hr1) :
      A)

Tactic:
exact ⟨hr1, ⟨⟨x, I_le_J hx⟩, rfl⟩⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
apply : toIdeal (homogeneousHull 𝒜 I) ≤ I
⊢ toIdeal (homogeneousHull 𝒜 I) = I

Tactic:
apply le_antisymm _ (Ideal.le_toIdeal_homogeneousHull _ _)

Premises used: Ideal.le_toIdeal_homogeneousHull, le_antisymm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
apply :
  {r : A |
      ∃ (i : ι) (x : ↥I),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
          r} ⊆
    (↑I : Set A)
⊢ toIdeal (homogeneousHull 𝒜 I) ≤ I

Tactic:
apply Ideal.span_le.2

Premises used: Ideal.span_le, Iff.mpr
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
i : ι
x : ↥I
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈
    (↑I : Set A)

Tactic:
h _ x.prop

Premises used: Set.Mem, Subtype.prop
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
i : ι
x : ↥I
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈
    (↑I : Set A)

Tactic:
exact h _ x.prop

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ Ideal.homogeneousHull 𝒜 I.toIdeal = I

Tactic:
HomogeneousIdeal.toIdeal_injective <| I.isHomogeneous.toIdeal_homogeneousHull_eq_self

Premises used: HomogeneousIdeal.toIdeal_injective, HomogeneousIdeal.isHomogeneous, Ideal.IsHomogeneous.toIdeal_homogeneousHull_eq_self
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
rw : toIdeal (homogeneousHull 𝒜 I) = span (⋃ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A))
⊢ toIdeal (homogeneousHull 𝒜 I) = ⨆ (i : ι), span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A))

Tactic:
rw [← Ideal.span_iUnion]

Premises used: Ideal.span_iUnion
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
apply :
  Eq.{u_3 + 1} (α := Set A)
    {r : A |
      ∃ (i : ι) (x : ↥I),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) = r}
    (⋃ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A))
⊢ toIdeal (homogeneousHull 𝒜 I) = span (⋃ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A))

Tactic:
apply congr_arg Ideal.span _

Premises used: congr_arg, Ideal.span
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
h :
  ∀ (x : A),
    Membership.mem (γ := Set A)
        {r : A |
          ∃ (i : ι) (x : ↥I),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
              r}
        x ↔
      Membership.mem (γ := Set A) (⋃ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)) x
⊢ Eq.{u_3 + 1} (α := Set A)
    {r : A |
      ∃ (i : ι) (x : ↥I),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) = r}
    (⋃ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A))

Tactic:
ext1
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
x : A
⊢ Membership.mem (γ := Set A)
      {r : A |
        ∃ (i : ι) (x : ↥I),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
            r}
      x ↔
    Membership.mem (γ := Set A) (⋃ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)) x

Tactic:
simp only [Set.mem_iUnion, Set.mem_image, mem_setOf_eq, GradedRing.proj_apply, SetLike.exists,
    exists_prop, SetLike.mem_coe]

Premises used: Set.mem_iUnion, Set.mem_image, Set.mem_setOf_eq, exists_prop, SetLike.mem_coe, SetLike.exists, GradedRing.proj_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
i : ι
x : A
⊢ IsHomogeneousElem (R := A) 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) x : A)

Tactic:
apply SetLike.isHomogeneousElem_coe

Premises used: SetLike.isHomogeneousElem_coe
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
h :
  toIdeal (homogeneousHull 𝒜 I) =
    toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (⨆ (i : ι),
        { toSubmodule := span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)), is_homogeneous' := ⋯ })
⊢ Eq (α := HomogeneousIdeal 𝒜) (homogeneousHull 𝒜 I)
    (⨆ (i : ι), { toSubmodule := span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)), is_homogeneous' := ⋯ })

Tactic:
ext1
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
h :
  Eq (α := Ideal A) (⨆ (i : ι), span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)))
    (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (⨆ (i : ι),
        { toSubmodule := span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)), is_homogeneous' := ⋯ }))
h₁ h₂ :
  Eq.{u_3 + 1} (α := Ideal A) (⨆ (i : ι), span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)))
    (⨆ (i : ι),
      toIdeal { toSubmodule := span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)), is_homogeneous' := ⋯ })
⊢ toIdeal (homogeneousHull 𝒜 I) =
    toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (⨆ (i : ι),
        { toSubmodule := span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)), is_homogeneous' := ⋯ })

Tactic:
rw [Ideal.toIdeal_homogeneousHull_eq_iSup, toIdeal_iSup]

Premises used: Ideal.toIdeal_homogeneousHull_eq_iSup, HomogeneousIdeal.toIdeal_iSup
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
⊢ GaloisConnection (α := Ideal A) (β := HomogeneousIdeal 𝒜) (homogeneousHull 𝒜) toIdeal

Tactic:
fun _ J =>
  ⟨le_trans (Ideal.le_toIdeal_homogeneousHull _ _),
    fun H => J.homogeneousHull_toIdeal_eq_self ▸ Ideal.homogeneousHull_mono 𝒜 H⟩

Premises used: Eq.rec, Ideal.homogeneousHull_mono, Ideal.le_toIdeal_homogeneousHull, Iff.intro, HomogeneousIdeal.homogeneousHull_toIdeal_eq_self, le_trans, GaloisConnection
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
⊢ Eq (α := HomogeneousIdeal 𝒜) (homogeneousHull 𝒜 I) (sInf {J : HomogeneousIdeal 𝒜 | I ≤ J.toIdeal})

Tactic:
Eq.symm <| IsGLB.sInf_eq <| (Ideal.homogeneousHull.gc 𝒜).isLeast_l.isGLB

Premises used: IsGLB.sInf_eq, IsLeast.isGLB, Ideal.homogeneousHull.gc, GaloisConnection.isLeast_l, Eq.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
i : ι
r : A
hr : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
change :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
⊢ Membership.mem (γ := Submodule A A) (RingHom.ker (F := A →+* A) (projZeroRingHom 𝒜))
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
change (decompose 𝒜 (decompose 𝒜 r _ : A) 0 : A) = 0

Premises used: OfNat.ofNat, Subtype.val, DFunLike.coe, DirectSum.decompose
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
i : ι
r : A
hr : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
pos :
  ∀ (h : i = 0),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) =
      0
neg :
  ∀ (h : ¬i = 0),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) =
      0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0

Tactic:
by_cases h : i = 0
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
i : ι
r : A
hr : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
h : i = 0
pos :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
pos₁ : (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
pos₂ : (↑(((0 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
pos₃ : Eq.{u_3 + 1} (α := A) (↑0 : A) 0
pos₄ pos₅ : Eq.{u_3 + 1} (α := A) 0 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0

Tactic:
rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]

Premises used: ZeroMemClass.coe_zero, DirectSum.decompose_zero, DirectSum.zero_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
i : ι
r : A
hr : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
h : ¬i = 0
neg neg₁ : Eq.{u_3 + 1} (α := A) 0 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0

Tactic:
rw [decompose_of_mem_ne 𝒜 (SetLike.coe_mem _) h]

Premises used: SetLike.coe_mem, DirectSum.decompose_of_mem_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
a : A
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜) (𝒜₊) a ↔ Eq (α := A) ((proj 𝒜 0 : (a : A) → A) a : A) (0 : A)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
⊢ Eq (α := Ideal A) (toIdeal (𝒜₊)) (RingHom.ker (F := A →+* A) (projZeroRingHom 𝒜))

Tactic:
rfl

Premises used: Ideal.comap, rfl, RingHom.ker
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
x : A
i : ι
hi : 0 < i
hx : x ∈ 𝒜 i
⊢ 0 ≠ i

Tactic:
aesop
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
x : A
i : ι
hi : 0 < i
hx : x ∈ 𝒜 i
rw : Eq (α := A) ((proj 𝒜 0 : (a : A) → A) x : A) (0 : A)
rw₁ : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
rw₂ :
  (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) x hx) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
rw₃ : Eq.{u_3 + 1} (α := A) (↑0 : A) 0
rw₄ rw₅ : Eq.{u_3 + 1} (α := A) 0 0
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜) (𝒜₊) x

Tactic:
rw [mem_irrelevant_iff, GradedRing.proj_apply, DirectSum.decompose_of_mem _ hx,
    DirectSum.of_eq_of_ne _ _ _ (by aesop), ZeroMemClass.coe_zero]

Premises used: DirectSum.decompose_of_mem, HomogeneousIdeal.mem_irrelevant_iff, ZeroMemClass.coe_zero, GradedRing.proj_apply, DirectSum.of_eq_of_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
⊢ Eq (α := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊)))
    (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))

Tactic:
le_antisymm (fun x hx ↦ ?_) <| iSup₂_le fun i hi x hx ↦ mem_irrelevant_of_mem _ hi hx

Premises used: iSup₂_le, HomogeneousIdeal.mem_irrelevant_of_mem, le_antisymm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
refine :
  ∀ (x : A)
    (hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x),
    Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)) x
⊢ Eq (α := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊)))
    (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))

Tactic:
refine le_antisymm (fun x hx ↦ ?_) <| iSup₂_le fun i hi x hx ↦ mem_irrelevant_of_mem _ hi hx

Premises used: iSup₂_le, le_antisymm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
rw :
  Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)) x

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 x]

Premises used: DirectSum.sum_support_decompose
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
classical :
  Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)) x

Tactic:
classical rw [← DirectSum.sum_support_decompose 𝒜 x]
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))

Tactic:
sum_mem fun j hj ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
refine :
  ∀ (j : ι)
    (hj :
      Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j),
    Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))

Tactic:
refine sum_mem fun j hj ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
j : ι
hj :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
pos :
  ∀ (hj₀ : j = 0),
    Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
neg :
  ∀ (hj₀ : ¬j = 0),
    Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)

Tactic:
by_cases hj₀ : j = 0
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
j : ι
hj :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
hj₀ : j = 0
⊢ Eq (α := ↥(𝒜 0)) ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) 0

Tactic:
simpa using hx