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 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
refine :
  ∀ c ∈ s.support,
    Membership.mem (γ := Ideal A) (span s_1)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                  (HSMul.hSMul (α := A) ((s : (a : { x : A // x ∈ s_1 }) → A) c : A) (↑c : A)) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A)
⊢ Membership.mem (γ := Submodule A A) (span s_1)
    (∑ i_1 ∈ s.support,
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                  (HSMul.hSMul (α := A) ((s : (a : { x : A // x ∈ s_1 }) → A) i_1 : A) (↑i_1 : A)) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))

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 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
z : { x : A // x ∈ s_1 }
hz1 : z ∈ s.support
rw :
  Membership.mem (γ := Ideal A) (span s_1)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (HMul.hMul (α := A) ((s : (a : { x : A // x ∈ s_1 }) → A) z : A) (↑z : A)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)
⊢ Membership.mem (γ := Ideal A) (span s_1)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (HSMul.hSMul (α := A) ((s : (a : { x : A // x ∈ s_1 }) → A) z : A) (↑z : A)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
rw [smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
z : { x : A // x ∈ s_1 }
hz1 : z ∈ s.support
⊢ Membership.mem (γ := Ideal A) (span s_1)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (HMul.hMul (α := A) ((s : (a : { x : A // x ∈ s_1 }) → A) z : A) (↑z : A)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
Ideal.mul_homogeneous_element_mem_of_mem 𝒜 (s z) z ?_ ?_ i

Premises used: Set.Mem, Ideal.mul_homogeneous_element_mem_of_mem, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
z : { x : A // x ∈ s_1 }
hz1 : z ∈ s.support
refine_1 : IsHomogeneousElem 𝒜 (↑z : A)
refine_2 : Membership.mem (γ := Ideal A) (span s_1) (↑z : A)
⊢ Membership.mem (γ := Ideal A) (span s_1)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (HMul.hMul (α := A) ((s : (a : { x : A // x ∈ s_1 }) → A) z : A) (↑z : A)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
refine Ideal.mul_homogeneous_element_mem_of_mem 𝒜 (s z) z ?_ ?_ i

Premises used: Ideal.mul_homogeneous_element_mem_of_mem, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
z : { x : A // x ∈ s_1 }
hz1 : z ∈ s.support
refine_1 :
  ∀ (z : A) (hz2 : z ∈ s_1) (hz1 : Subtype.mk (p := fun (x : A) ↦ x ∈ s_1) z hz2 ∈ s.support),
    IsHomogeneousElem 𝒜 (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ s_1) z hz2) : A)
⊢ IsHomogeneousElem 𝒜 (↑z : A)

Tactic:
rcases z with ⟨z, hz2⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
z : A
hz2 : z ∈ s_1
hz1 : Subtype.mk (p := fun (x : A) ↦ x ∈ s_1) z hz2 ∈ s.support
⊢ IsHomogeneousElem 𝒜 (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ s_1) z hz2) : A)

Tactic:
apply h _ hz2
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
z : { x : A // x ∈ s_1 }
hz1 : z ∈ s.support
⊢ Membership.mem (γ := Ideal A) (span s_1) (↑z : A)

Tactic:
Ideal.subset_span z.2

Premises used: Ideal.subset_span, Subtype.property
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
s_1 : Set A
h : ∀ x ∈ s_1, IsHomogeneousElem 𝒜 x
i : ι
s : { x : A // x ∈ s_1 } →₀ A
z : { x : A // x ∈ s_1 }
hz1 : z ∈ s.support
⊢ Membership.mem (γ := Ideal A) (span s_1) (↑z : A)

Tactic:
exact Ideal.subset_span z.2

Premises used: Ideal.subset_span, Subtype.property
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
x : A
h :
  x ∈
    image (α := Subtype (IsHomogeneousElem 𝒜)) (Subtype.val (p := IsHomogeneousElem 𝒜))
      (Subtype.val (p := IsHomogeneousElem 𝒜) ⁻¹' (↑I : Set A))
⊢ image (α := { x : A // x ∈ setOf (IsHomogeneousElem 𝒜) })
      (Subtype.val (p := fun (x : A) ↦ x ∈ setOf (IsHomogeneousElem 𝒜)))
      (Subtype.val (p := fun (x : A) ↦ x ∈ setOf (IsHomogeneousElem 𝒜)) ⁻¹' (↑I : Set A)) =
    setOf (IsHomogeneousElem 𝒜) ∩ (↑I : Set A)

Tactic:
have := Subtype.image_preimage_coe (setOf (SetLike.IsHomogeneousElem 𝒜)) (I : Set A)
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
x : A
h :
  x ∈
    image (α := Subtype (IsHomogeneousElem 𝒜)) (Subtype.val (p := IsHomogeneousElem 𝒜))
      (Subtype.val (p := IsHomogeneousElem 𝒜) ⁻¹' (↑I : Set A))
this :
  image (α := { x : A // x ∈ setOf (IsHomogeneousElem 𝒜) })
      (Subtype.val (p := fun (x : A) ↦ x ∈ setOf (IsHomogeneousElem 𝒜)))
      (Subtype.val (p := fun (x : A) ↦ x ∈ setOf (IsHomogeneousElem 𝒜)) ⁻¹' (↑I : Set A)) =
    setOf (IsHomogeneousElem 𝒜) ∩ (↑I : Set A)
⊢ IsHomogeneousElem 𝒜 x

Tactic:
(cast congr(_ ∈ $this) h).1

Premises used: congrArg, Set.Mem, setOf, cast, Membership.mem, id, And.left, SetLike.IsHomogeneousElem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
x : A
h :
  x ∈
    image (α := Subtype (IsHomogeneousElem 𝒜)) (Subtype.val (p := IsHomogeneousElem 𝒜))
      (Subtype.val (p := IsHomogeneousElem 𝒜) ⁻¹' (↑I : Set A))
this :
  image (α := { x : A // x ∈ setOf (IsHomogeneousElem 𝒜) })
      (Subtype.val (p := fun (x : A) ↦ x ∈ setOf (IsHomogeneousElem 𝒜)))
      (Subtype.val (p := fun (x : A) ↦ x ∈ setOf (IsHomogeneousElem 𝒜)) ⁻¹' (↑I : Set A)) =
    setOf (IsHomogeneousElem 𝒜) ∩ (↑I : Set A)
⊢ IsHomogeneousElem 𝒜 x

Tactic:
exact (cast congr(_ ∈ $this) h).1

Premises used: congrArg, cast, Membership.mem, id, And.left
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
⊢ Monotone (α := Ideal A) (β := HomogeneousIdeal 𝒜) (homogeneousCore 𝒜)

Tactic:
Ideal.homogeneousCore'_mono 𝒜

Premises used: Set.Mem, Monotone, Submodule.span, Ideal.homogeneousCore, Ideal.homogeneousCore', Ideal.homogeneousCore'_mono
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
⊢ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 I) ≤ I

Tactic:
Ideal.homogeneousCore'_le 𝒜 I

Premises used: Set.Mem, Ideal.homogeneousCore'_le
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
x : A
h : IsHomogeneousElem 𝒜 x
hmem : x ∈ I
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜) (homogeneousCore 𝒜 I) x

Tactic:
Ideal.subset_span ⟨⟨x, h⟩, hmem, rfl⟩

Premises used: Ideal.subset_span, Set.Mem, Subtype.mk, And.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 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
apply : I ≤ homogeneousCore' 𝒜 I
⊢ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 I) = I

Tactic:
apply le_antisymm (I.homogeneousCore'_le 𝒜) _

Premises used: Ideal.homogeneousCore'_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 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
rw :
  ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈
    homogeneousCore' 𝒜 I
⊢ x ∈ homogeneousCore' 𝒜 I

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 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ 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) ∈
    homogeneousCore' 𝒜 I

Tactic:
Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, isHomogeneousElem_coe _⟩, h _ hx, rfl⟩

Premises used: Ideal.subset_span, Set.Mem, SetLike.isHomogeneousElem_coe, Ideal.sum_mem, Subtype.mk, And.intro, Exists.intro, Subtype.val, DFunLike.coe, rfl, DirectSum.decompose
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ 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) ∈
    homogeneousCore' 𝒜 I

Tactic:
exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, isHomogeneousElem_coe _⟩, h _ hx, rfl⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
rw rw₁ rw₂ :
  ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈
    homogeneousCore' 𝒜 I
⊢ x ∈ homogeneousCore' 𝒜 I

Tactic:
classical
  rw [← DirectSum.sum_support_decompose 𝒜 x]
  exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, isHomogeneousElem_coe _⟩, h _ hx, rfl⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
h : toIdeal (Ideal.homogeneousCore 𝒜 I.toIdeal) = I.toIdeal
⊢ Ideal.homogeneousCore 𝒜 I.toIdeal = I

Tactic:
ext1
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ toIdeal (Ideal.homogeneousCore 𝒜 I.toIdeal) = I.toIdeal

Tactic:
Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self I.isHomogeneous

Premises used: HomogeneousIdeal.isHomogeneous, Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ toIdeal (Ideal.homogeneousCore 𝒜 I.toIdeal) = I.toIdeal

Tactic:
convert! Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self I.isHomogeneous

Premises used: HomogeneousIdeal.isHomogeneous, Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
⊢ IsHomogeneous 𝒜 I ↔ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 I) = I

Tactic:
⟨fun hI => hI.toIdeal_homogeneousCore_eq_self, fun hI => hI ▸ (Ideal.homogeneousCore 𝒜 I).2⟩

Premises used: HomogeneousSubmodule.is_homogeneous', Eq.rec, Iff.intro, Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self, Ideal.homogeneousCore
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
rw :
  I = HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 I) ↔
    ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
      I = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)
⊢ IsHomogeneous 𝒜 I ↔
    ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
      I = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)

Tactic:
rw [Ideal.IsHomogeneous.iff_eq, eq_comm]

Premises used: eq_comm, Ideal.IsHomogeneous.iff_eq
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
⊢ I = HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 I) ↔
    ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
      I = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)

Tactic:
((Set.image_preimage.compose (Submodule.gi _ _).gc).exists_eq_l _).symm

Premises used: Submodule.gi, GaloisConnection.exists_eq_l, Set.Mem, setOf, Set.image_preimage, Set.preimage, Submodule.span, Ideal.homogeneousCore', GaloisConnection.compose, Iff.symm, SetLike.IsHomogeneousElem, GaloisInsertion.gc
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
⊢ I = HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 I) ↔
    ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
      I = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)

Tactic:
exact ((Set.image_preimage.compose (Submodule.gi _ _).gc).exists_eq_l _).symm

Premises used: Submodule.gi, GaloisConnection.exists_eq_l, Set.image_preimage, GaloisConnection.compose, Iff.symm, GaloisInsertion.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 : ι
r : A
hr : Membership.mem (γ := Submodule A A) ⊥ r
⊢ r = 0

Tactic:
simp only [Ideal.mem_bot] at hr

Premises used: Ideal.mem_bot
-- 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 : ι
r : A
hr : r = 0
rw : Membership.mem (γ := Submodule A A) ⊥ (↑0 : A)
⊢ Membership.mem (γ := Submodule A A) ⊥
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
rw [hr, decompose_zero, zero_apply]

Premises used: 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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
i : ι
r : A
hr : r = 0
⊢ Membership.mem (γ := Submodule A A) ⊥ (↑0 : A)

Tactic:
apply Ideal.zero_mem

Premises used: Ideal.zero_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 : ι
r : A
h : Membership.mem (γ := Submodule A A) ⊤ r
⊢ Membership.mem (γ := Submodule A A) ⊤
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
simp only [Submodule.mem_top]

Premises used: Submodule.mem_top
-- 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
HI : IsHomogeneous 𝒜 I
HJ : IsHomogeneous 𝒜 J
⊢ IsHomogeneous 𝒜 (I ⊓ J)

Tactic:
fun _ _ hr => ⟨HI _ hr.1, HJ _ hr.2⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro, DirectSum.SetLike.IsHomogeneous, Submodule.IsHomogeneous
-- 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
HI : IsHomogeneous 𝒜 I
HJ : IsHomogeneous 𝒜 J
rw :
  ∀
    (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)),
    ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
      I ⊔ J = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)
⊢ IsHomogeneous 𝒜 (I ⊔ J)

Tactic:
rw [iff_exists] at HI HJ ⊢

Premises used: Ideal.IsHomogeneous.iff_exists
-- 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
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 𝒜)),
      Eq (α := 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 : Semiring 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₁) ⊔
        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:
⟨s₁ ∪ s₂, ?_⟩

Premises used: Exists.intro, Union.union
-- 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 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
refine :
  Eq (α := 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₂)))
⊢ ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    Eq (α := 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:
refine ⟨s₁ ∪ s₂, ?_⟩