awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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 𝒜
κ : Sort u_4
s : κ → HomogeneousIdeal 𝒜
rw :
  Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (sInf (range fun (i : κ) ↦ s i)))
    (⨅ (i : κ), (s i).toIdeal)
rw₁ :
  Eq.{u_3 + 1} (α := Ideal A)
    (⨅ (s_1 : HomogeneousIdeal 𝒜),
      ⨅ (_ : Membership.mem (γ := Set (HomogeneousIdeal 𝒜)) (range fun (i : κ) ↦ s i) s_1), s_1.toIdeal)
    (⨅ (i : κ), (s i).toIdeal)
⊢ Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (⨅ (i : κ), s i)) (⨅ (i : κ), (s i).toIdeal)
have rw₂ : Eq.{u_3 + 1} (α := Ideal A) (⨅ (i : κ), (s i).toIdeal) (⨅ (i : κ), (s i).toIdeal)
Tactic: rw [iInf, toIdeal_sInf, iInf_range]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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 : IsHomogeneous 𝒜 I
HJ : IsHomogeneous 𝒜 J
⊢ IsHomogeneous 𝒜 (I * J)
have 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)
Tactic: rw [Ideal.IsHomogeneous.iff_exists] at HI HJ ⊢
Cleared hypotheses: HI, HJ
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    I * J = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)
have 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)
Tactic: obtain ⟨⟨s₁, rfl⟩, ⟨s₂, rfl⟩⟩ := HI, HJ
Cleared hypotheses: I, J, HI, HJ
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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 𝒜)),
    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)
have 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))
Tactic: rw [Ideal.span_mul_span']
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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}
have refine : IsLUB {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
Tactic: refine (IsLUB.sSup_eq ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ IsLUB {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
have h : IsGreatest {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
Tactic: apply IsGreatest.isLUB
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (hypothesis)
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
⊢ IsGreatest {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
have coe_mono : Monotone (α := HomogeneousIdeal 𝒜) toIdeal
Tactic: have coe_mono : Monotone (toIdeal : HomogeneousIdeal 𝒜 → Ideal A) := fun x y => id
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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 {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
have h : Eq (α := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I}
  (image (α := HomogeneousIdeal 𝒜) toIdeal {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I})
Tactic: convert! coe_mono.map_isGreatest (Ideal.homogeneousCore.gc 𝒜).isGreatest_u using 1
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ Eq (α := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I}
    (image (α := HomogeneousIdeal 𝒜) toIdeal {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I})
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
have h : (∃ (x_1 : HomogeneousIdeal 𝒜),
    Membership.mem (γ := Set (HomogeneousIdeal 𝒜)) {b : HomogeneousIdeal 𝒜 | b.toIdeal ≤ I} x_1 ∧ x_1.toIdeal = x) →
  IsHomogeneous 𝒜 x ∧ x ≤ I
Tactic: refine ⟨fun hI => ⟨⟨x, hI.1⟩, ⟨hI.2, rfl⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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})
    𝒜
have 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
Tactic: refine Ideal.homogeneous_span _ _ fun x hx => ?_
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ IsHomogeneousElem 𝒜 x
have obtain : ∀ (i : ι) (x : ↥I),
  IsHomogeneousElem 𝒜
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
Tactic: obtain ⟨i, x, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ r ∈ toIdeal (homogeneousHull 𝒜 I)
have 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)
Tactic: rw [← DirectSum.sum_support_decompose 𝒜 r]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
have 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)
Tactic: refine Ideal.sum_mem _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) ∈
    toIdeal (homogeneousHull 𝒜 I)
have 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: apply Ideal.subset_span
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ 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)
have 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)
Tactic: use j
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ ∃ (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)
have w : ↥I
Tactic: use ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
w : ↥I
⊢ ∃ (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)
have 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)
Tactic: use ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ r ∈ toIdeal (homogeneousHull 𝒜 I)
have 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)
Tactic: classical
  rw [← DirectSum.sum_support_decompose 𝒜 r]
  refine Ideal.sum_mem _ ?_
  intro j _
  apply Ideal.subset_span
  use j
  use ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ r ∈ toIdeal (homogeneousHull 𝒜 I)
have rw₃ : ∀ (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)
Tactic: classical
  rw [← DirectSum.sum_support_decompose 𝒜 r]
  refine Ideal.sum_mem _ ?_
  intro j _
  apply Ideal.subset_span
  use j
  use ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ r ∈ toIdeal (homogeneousHull 𝒜 I)
have 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)
Tactic: classical
  rw [← DirectSum.sum_support_decompose 𝒜 r]
  refine Ideal.sum_mem _ ?_
  intro j _
  apply Ideal.subset_span
  use j
  use ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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)
⊢ r ∈ toIdeal (homogeneousHull 𝒜 I)
have 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)
Tactic: classical
  rw [← DirectSum.sum_support_decompose 𝒜 r]
  refine Ideal.sum_mem _ ?_
  intro j _
  apply Ideal.subset_span
  use j
  use ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ LE.le (α := HomogeneousIdeal 𝒜) (homogeneousHull 𝒜 I) (homogeneousHull 𝒜 J)
have 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}
Tactic: apply Ideal.span_mono
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ toIdeal (homogeneousHull 𝒜 I) = I
have apply : toIdeal (homogeneousHull 𝒜 I) ≤ I
Tactic: apply le_antisymm _ (Ideal.le_toIdeal_homogeneousHull _ _)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ toIdeal (homogeneousHull 𝒜 I) ≤ I
have apply : {r : A |
    ∃ (i : ι) (x : ↥I),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) = r} ⊆
  (↑I : Set A)
Tactic: apply Ideal.span_le.2
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ toIdeal (homogeneousHull 𝒜 I) = ⨆ (i : ι), span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A))
have rw : toIdeal (homogeneousHull 𝒜 I) = span (⋃ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A))
Tactic: rw [← Ideal.span_iUnion]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ toIdeal (homogeneousHull 𝒜 I) = span (⋃ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A))
have 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))
Tactic: apply congr_arg Ideal.span _
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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.{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))
have 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
Tactic: ext1