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 𝒜
I : Ideal A
⊢ Eq (α := HomogeneousIdeal 𝒜) (homogeneousHull 𝒜 I)
    (⨆ (i : ι), { toSubmodule := span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)), is_homogeneous' := ⋯ })
have 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' := sorry })
Tactic: ext1
-- 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) =
    toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (⨆ (i : ι),
        { toSubmodule := span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)), is_homogeneous' := ⋯ })
have 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' := sorry }))
Tactic: rw [Ideal.toIdeal_homogeneousHull_eq_iSup, toIdeal_iSup]
-- 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 :
  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' := ⋯ }))
⊢ toIdeal (homogeneousHull 𝒜 I) =
    toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (⨆ (i : ι),
        { toSubmodule := span ((⇑(GradedRing.proj 𝒜 i) : (a : A) → A) '' (↑I : Set A)), is_homogeneous' := ⋯ })
have 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' := sorry })
Tactic: rw [Ideal.toIdeal_homogeneousHull_eq_iSup, toIdeal_iSup]
-- 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 : 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
⊢ Membership.mem (γ := Submodule A A) (RingHom.ker (F := A →+* A) (projZeroRingHom 𝒜))
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have 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
Tactic: change (decompose 𝒜 (decompose 𝒜 r _ : A) 0 : A) = 0
-- 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 : 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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
have 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
Tactic: by_cases h : i = 0
-- 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 : 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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
have 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
Tactic: by_cases h : i = 0
-- 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 : 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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
have 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
Tactic: rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
-- 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 : 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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
have pos₁ : (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
Tactic: rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
-- 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 : 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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
have pos₂ : (↑(((0 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
Tactic: rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
-- 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 : 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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
have pos₃ : Eq.{u_3 + 1} (α := A) (↑0 : A) 0
Tactic: rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
-- 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 : 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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
have pos₄ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
-- 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 : 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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    0
have neg : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [decompose_of_mem_ne 𝒜 (SetLike.coe_mem _) h]
-- 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 : 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
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜) (𝒜₊) x
have rw : Eq (α := A) ((proj 𝒜 0 : (a : A) → A) x : A) (0 : A)
Tactic: rw [mem_irrelevant_iff, GradedRing.proj_apply, DirectSum.decompose_of_mem _ hx,
    DirectSum.of_eq_of_ne _ _ _ (by aesop), ZeroMemClass.coe_zero]
-- 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 : 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)
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜) (𝒜₊) x
have rw₁ : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
Tactic: rw [mem_irrelevant_iff, GradedRing.proj_apply, DirectSum.decompose_of_mem _ hx,
    DirectSum.of_eq_of_ne _ _ _ (by aesop), ZeroMemClass.coe_zero]
-- 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 : 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
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜) (𝒜₊) x
have 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
Tactic: rw [mem_irrelevant_iff, GradedRing.proj_apply, DirectSum.decompose_of_mem _ hx,
    DirectSum.of_eq_of_ne _ _ _ (by aesop), ZeroMemClass.coe_zero]
-- 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 : 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
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜) (𝒜₊) x
have rw₃ : Eq.{u_3 + 1} (α := A) (↑0 : A) 0
Tactic: rw [mem_irrelevant_iff, GradedRing.proj_apply, DirectSum.decompose_of_mem _ hx,
    DirectSum.of_eq_of_ne _ _ _ (by aesop), ZeroMemClass.coe_zero]
-- 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 : 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
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜) (𝒜₊) x
have rw₄ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [mem_irrelevant_iff, GradedRing.proj_apply, DirectSum.decompose_of_mem _ hx,
    DirectSum.of_eq_of_ne _ _ _ (by aesop), ZeroMemClass.coe_zero]
-- 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 : 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))
have refine : ∀ (x : A)
  (hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x),
  Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)) x
Tactic: refine le_antisymm (fun x hx ↦ ?_) <| iSup₂_le fun i hi x hx ↦ mem_irrelevant_of_mem _ hi 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 : 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)) x
have 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))
Tactic: rw [← DirectSum.sum_support_decompose 𝒜 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 : 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)) x
have 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))
Tactic: classical rw [← DirectSum.sum_support_decompose 𝒜 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 : 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))
have 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)
Tactic: refine sum_mem fun j hj ↦ ?_
-- 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 : 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
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have 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)
Tactic: by_cases hj₀ : j = 0
-- 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 : 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)
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have 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)
Tactic: by_cases hj₀ : j = 0
-- 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 : 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 (𝒜₊)))
    (closure (⋃ (i : ι), ⋃ (_ : i > 0), (↑(𝒜 i) : Set A)))
have rw : Eq.{u_3 + 1} (α := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), ofClass (𝒜 i))
  (closure (⋃ (i : ι), ⋃ (_ : i > 0), (↑(𝒜 i) : Set A)))
Tactic: rw [irrelevant_eq_iSup]