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 : CommSemiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I J : Ideal A
HI :
  ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    I = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)
HJ :
  ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    J = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)
obtain :
  ∀ (s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)),
    ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
      HMul.hMul (α := Ideal A)
          (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₁))
          (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₂)) =
        span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)
⊢ ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    I * J = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)

Tactic:
obtain ⟨⟨s₁, rfl⟩, ⟨s₂, rfl⟩⟩ := HI, HJ

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommSemiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
rw :
  ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    Eq (α := Ideal A)
      (span
        (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₁ *
          Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₂))
      (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S))
⊢ ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    HMul.hMul (α := Ideal A)
        (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₁))
        (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₂)) =
      span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)

Tactic:
rw [Ideal.span_mul_span']

Premises used: Ideal.span_mul_span'
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommSemiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    Eq (α := Ideal A)
      (span
        (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₁ *
          Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₂))
      (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S))

Tactic:
⟨s₁ * s₂, congr_arg _ <| (Set.image_mul (homogeneousSubmonoid 𝒜).subtype).symm⟩

Premises used: HMul.hMul, SetLike.homogeneousSubmonoid, Set.image_mul, congr_arg, Exists.intro, Submonoid.subtype, Eq.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommSemiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    Eq (α := Ideal A)
      (span
        (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₁ *
          Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₂))
      (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S))

Tactic:
exact ⟨s₁ * s₂, congr_arg _ <| (Set.image_mul (homogeneousSubmonoid 𝒜).subtype).symm⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommSemiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I J : HomogeneousIdeal 𝒜
⊢ (I * J).toIdeal = I.toIdeal * J.toIdeal

Tactic:
rfl

Premises used: 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 𝒜
⊢ GaloisConnection (α := HomogeneousIdeal 𝒜) toIdeal (homogeneousCore 𝒜)

Tactic:
fun I _ =>
  ⟨fun H => I.toIdeal_homogeneousCore_eq_self ▸ Ideal.homogeneousCore_mono 𝒜 H,
    fun H => le_trans H (Ideal.homogeneousCore'_le _ _)⟩

Premises used: HomogeneousIdeal.toIdeal_homogeneousCore_eq_self, Eq.rec, Ideal.homogeneousCore'_le, Iff.intro, Ideal.homogeneousCore_mono, 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 𝒜) (homogeneousCore 𝒜 I) (sSup {J : HomogeneousIdeal 𝒜 | J.toIdeal ≤ I})

Tactic:
Eq.symm <| IsLUB.sSup_eq <| (Ideal.homogeneousCore.gc 𝒜).isGreatest_u.isLUB

Premises used: GaloisConnection.isGreatest_u, IsLUB.sSup_eq, IsGreatest.isLUB, Eq.symm, Ideal.homogeneousCore.gc
-- 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
⊢ homogeneousCore' 𝒜 I = sSup {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I}

Tactic:
(IsLUB.sSup_eq ?_).symm

Premises used: IsLUB.sSup_eq, 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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
refine : IsLUB {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
⊢ homogeneousCore' 𝒜 I = sSup {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I}

Tactic:
refine (IsLUB.sSup_eq ?_).symm

Premises used: IsLUB.sSup_eq, 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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsGreatest {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
⊢ IsLUB {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)

Tactic:
apply IsGreatest.isLUB

Premises used: IsGreatest.isLUB
-- 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
⊢ Monotone (α := HomogeneousIdeal 𝒜) toIdeal

Tactic:
have coe_mono : Monotone (toIdeal : HomogeneousIdeal 𝒜 → Ideal A) := fun x y => id
-- 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
coe_mono : Monotone (α := HomogeneousIdeal 𝒜) toIdeal
⊢ IsGreatest (image (α := HomogeneousIdeal 𝒜) toIdeal {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I})
    (toIdeal (homogeneousCore 𝒜 I))

Tactic:
coe_mono.map_isGreatest (Ideal.homogeneousCore.gc 𝒜).isGreatest_u

Premises used: GaloisConnection.isGreatest_u, Monotone.map_isGreatest, Ideal.homogeneousCore.gc
-- 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
coe_mono : Monotone (α := HomogeneousIdeal 𝒜) toIdeal
h :
  Eq (α := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I}
    (image (α := HomogeneousIdeal 𝒜) toIdeal {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I})
⊢ IsGreatest {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)

Tactic:
convert! coe_mono.map_isGreatest (Ideal.homogeneousCore.gc 𝒜).isGreatest_u using 1

Premises used: GaloisConnection.isGreatest_u, Monotone.map_isGreatest, Ideal.homogeneousCore.gc
-- 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
coe_mono : Monotone (α := HomogeneousIdeal 𝒜) toIdeal
h :
  ∀ (x : Ideal A),
    Membership.mem (γ := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} x ↔
      Membership.mem (γ := Set (Ideal A))
        (image (α := HomogeneousIdeal 𝒜) toIdeal {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I}) x
⊢ Eq (α := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I}
    (image (α := HomogeneousIdeal 𝒜) toIdeal {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I})

Tactic:
ext 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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone (α := HomogeneousIdeal 𝒜) toIdeal
x : Ideal A
⊢ IsHomogeneous 𝒜 x ∧ x ≤ I ↔
    ∃ (x_1 : HomogeneousIdeal 𝒜),
      Membership.mem (γ := Set (HomogeneousIdeal 𝒜)) {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I} x_1 ∧ x_1.toIdeal = x

Tactic:
⟨fun hI => ⟨⟨x, hI.1⟩, ⟨hI.2, rfl⟩⟩, ?_⟩

Premises used: HomogeneousSubmodule.mk, And.right, And.left, And.intro, Iff.intro, Exists.intro, 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
coe_mono : Monotone (α := HomogeneousIdeal 𝒜) toIdeal
x : Ideal A
h :
  (∃ (x_1 : HomogeneousIdeal 𝒜),
      Membership.mem (γ := Set (HomogeneousIdeal 𝒜)) {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I} x_1 ∧ x_1.toIdeal = x) →
    IsHomogeneous 𝒜 x ∧ x ≤ I
⊢ IsHomogeneous 𝒜 x ∧ x ≤ I ↔
    ∃ (x_1 : HomogeneousIdeal 𝒜),
      Membership.mem (γ := Set (HomogeneousIdeal 𝒜)) {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I} x_1 ∧ x_1.toIdeal = x

Tactic:
refine ⟨fun hI => ⟨⟨x, hI.1⟩, ⟨hI.2, 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
coe_mono : Monotone (α := HomogeneousIdeal 𝒜) toIdeal
x : HomogeneousIdeal 𝒜
hx : Membership.mem (γ := Set (HomogeneousIdeal 𝒜)) {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I} x
⊢ IsHomogeneous 𝒜 x.toIdeal ∧ x.toIdeal ≤ I

Tactic:
⟨x.isHomogeneous, hx⟩

Premises used: HomogeneousIdeal.isHomogeneous, And.intro
-- 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
coe_mono : Monotone (α := HomogeneousIdeal 𝒜) toIdeal
x : HomogeneousIdeal 𝒜
hx : Membership.mem (γ := Set (HomogeneousIdeal 𝒜)) {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I} x
⊢ IsHomogeneous 𝒜 x.toIdeal ∧ x.toIdeal ≤ I

Tactic:
exact ⟨x.isHomogeneous, hx⟩
-- 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
⊢ Submodule.IsHomogeneous
    (span
      {r : A |
        ∃ (i : ι) (x : ↥I),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
            r})
    𝒜

Tactic:
Ideal.homogeneous_span _ _ fun x hx => ?_

Premises used: Ideal.homogeneous_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
refine :
  ∀ (x : A)
    (hx :
      Membership.mem (γ := Set A)
        {r : A |
          ∃ (i : ι) (x : ↥I),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
              r}
        x),
    IsHomogeneousElem 𝒜 x
⊢ Submodule.IsHomogeneous
    (span
      {r : A |
        ∃ (i : ι) (x : ↥I),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
            r})
    𝒜

Tactic:
refine Ideal.homogeneous_span _ _ fun x hx => ?_

Premises used: Ideal.homogeneous_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
x : A
hx :
  Membership.mem (γ := Set A)
    {r : A |
      ∃ (i : ι) (x : ↥I),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) = r}
    x
obtain :
  ∀ (i : ι) (x : ↥I),
    IsHomogeneousElem 𝒜
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
⊢ IsHomogeneousElem 𝒜 x

Tactic:
obtain ⟨i, x, rfl⟩ := hx

Premises used: 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
i : ι
x : ↥I
⊢ IsHomogeneousElem 𝒜
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : 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
r : A
hr : r ∈ I
rw :
  ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈
    toIdeal (homogeneousHull 𝒜 I)
⊢ r ∈ toIdeal (homogeneousHull 𝒜 I)

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 r]

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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈
    toIdeal (homogeneousHull 𝒜 I)

Tactic:
Ideal.sum_mem _ ?_

Premises used: Set.Mem, Ideal.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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
refine :
  ∀ (c : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) c →
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) c) : A) ∈
        toIdeal (homogeneousHull 𝒜 I)
⊢ ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈
    toIdeal (homogeneousHull 𝒜 I)

Tactic:
refine Ideal.sum_mem _ ?_

Premises used: Ideal.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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
_ :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) j →
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) ∈
      toIdeal (homogeneousHull 𝒜 I)
⊢ Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) j →
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) ∈
      toIdeal (homogeneousHull 𝒜 I)

Tactic:
_
-- 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
r : A
hr : r ∈ I
j : ι
h :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) j
a :
  Membership.mem (γ := Set A)
    {r : A |
      ∃ (i : ι) (x : ↥I),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) = r}
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) ∈
    toIdeal (homogeneousHull 𝒜 I)

Tactic:
apply Ideal.subset_span

Premises used: Ideal.subset_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
r : A
hr : r ∈ I
j : ι
h_1 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) j
h :
  ∃ (x : ↥I),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ Membership.mem (γ := Set A)
    {r : A |
      ∃ (i : ι) (x : ↥I),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) = r}
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)

Tactic:
use j
-- 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
r : A
hr : r ∈ I
j : ι
h_1 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) j
w : ↥I
h :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ I) r hr) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          j) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ ∃ (x : ↥I),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)

Tactic:
use ⟨r, hr⟩
-- 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
r : A
hr : r ∈ I
rw rw₁ rw₂ :
  ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈
    toIdeal (homogeneousHull 𝒜 I)
rw₃ rw₄ :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) j →
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) ∈
        toIdeal (homogeneousHull 𝒜 I)
a :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) j →
      Membership.mem (γ := Set A)
        {r : A |
          ∃ (i : ι) (x : ↥I),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
              r}
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
h :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) j →
      ∃ (x : ↥I),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ r ∈ toIdeal (homogeneousHull 𝒜 I)

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

Premises used: Ideal.subset_span, Ideal.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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I J : Ideal A
I_le_J : I ≤ J
a :
  Subset.{u_3} (α := Set A)
    {r : A |
      ∃ (i : ι) (x : ↥I),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) = r}
    {r : A |
      ∃ (i : ι) (x : ↥J),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) = r}
⊢ LE.le (α := HomogeneousIdeal 𝒜) (homogeneousHull 𝒜 I) (homogeneousHull 𝒜 J)

Tactic:
apply Ideal.span_mono

Premises used: Ideal.span_mono
-- 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:
⟨hr1, ⟨⟨x, I_le_J hx⟩, rfl⟩⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, rfl