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 : 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
⊢ 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))
have 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)
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 : 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))
                (HSMul.hSMul (α := A) ((s : (a : { x : A // x ∈ s_1 }) → A) z : A) (↑z : A)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)
have 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)
Tactic: rw [smul_eq_mul]
-- 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 : 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)
have refine_1 : IsHomogeneousElem 𝒜 (↑z : A)
Tactic: refine Ideal.mul_homogeneous_element_mem_of_mem 𝒜 (s z) z ?_ ?_ i
-- 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 : 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)
⊢ 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)
have refine_2 : Membership.mem (γ := Ideal A) (span s_1) (↑z : A)
Tactic: refine Ideal.mul_homogeneous_element_mem_of_mem 𝒜 (s z) z ?_ ?_ i
-- 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 : 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
⊢ IsHomogeneousElem 𝒜 (↑z : A)
have 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)
Tactic: rcases z with ⟨z, hz2⟩
Cleared hypotheses: z, hz1
-- 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 : 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))
⊢ IsHomogeneousElem 𝒜 x
have 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)
Tactic: have := Subtype.image_preimage_coe (setOf (SetLike.IsHomogeneousElem 𝒜)) (I : Set A)
-- 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 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 I) = I
have apply : I ≤ homogeneousCore' 𝒜 I
Tactic: apply le_antisymm (I.homogeneousCore'_le 𝒜) _
-- 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 : 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
⊢ x ∈ homogeneousCore' 𝒜 I
have 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
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 : 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
⊢ x ∈ homogeneousCore' 𝒜 I
have 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
Tactic: classical
  rw [← DirectSum.sum_support_decompose 𝒜 x]
  exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, isHomogeneousElem_coe _⟩, h _ hx, 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 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ Ideal.homogeneousCore 𝒜 I.toIdeal = I
have h : toIdeal (Ideal.homogeneousCore 𝒜 I.toIdeal) = I.toIdeal
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 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
I : Ideal A
⊢ IsHomogeneous 𝒜 I ↔
    ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
      I = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)
have rw : I = HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 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]
-- 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 : ι
r : A
hr : Membership.mem (γ := Submodule A A) ⊥ r
⊢ Membership.mem (γ := Submodule A A) ⊥
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have hr₁ : r = 0
Tactic: simp only [Ideal.mem_bot] at hr
Cleared hypotheses: 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 : ι
r : A
hr : r = 0
⊢ Membership.mem (γ := Submodule A A) ⊥
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have rw : Membership.mem (γ := Submodule A A) ⊥ (↑0 : A)
Tactic: rw [hr, decompose_zero, zero_apply]
-- 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
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 [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 : 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)
⊢ ∃ (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 𝒜)),
    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: 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 : 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))
have 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₂)))
Tactic: refine ⟨s₁ ∪ s₂, ?_⟩
-- 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 𝒜
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₁ ∪ s₂)))
have rw : 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₁ ∪
      Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₂))
Tactic: rw [Set.image_union]
-- 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
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
⊢ IsHomogeneous 𝒜 (⨆ (i : κ), f i)
have simp_rw : ∀
  (h :
    ∀ (i : κ),
      ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
        f i =
          span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)),
  ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    Eq (α := Ideal A) (⨆ (i : κ), f i)
      (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S))
Tactic: simp_rw [iff_exists] at h ⊢
Cleared hypotheses: 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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
κ : Sort u_4
f : κ → Ideal A
h :
  ∀ (i : κ),
    ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
      f i = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S)
⊢ ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    Eq (α := Ideal A) (⨆ (i : κ), f i)
      (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S))
have choose : ∀ (s : (i : κ) → Set ↥(homogeneousSubmonoid 𝒜))
  (hs :
    ∀ (i : κ),
      f i =
        span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s i)),
  ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    Eq (α := Ideal A) (⨆ (i : κ), f i)
      (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S))
Tactic: choose s hs using h
Cleared hypotheses: 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 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
κ : Sort u_4
f : κ → Ideal A
s : (i : κ) → Set ↥(homogeneousSubmonoid 𝒜)
hs :
  ∀ (i : κ),
    f i = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s i)
⊢ ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    Eq (α := Ideal A) (⨆ (i : κ), f i)
      (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S))
have refine : Eq.{u_3 + 1} (α := Ideal A) (⨆ (i : κ), f i)
  (span
    (image (α := ↥(homogeneousSubmonoid 𝒜))
      (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x)) (⋃ (i : κ), s i)))
Tactic: refine ⟨⋃ i, s i, ?_⟩
-- 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
f : κ → Ideal A
s : (i : κ) → Set ↥(homogeneousSubmonoid 𝒜)
hs :
  ∀ (i : κ),
    f i = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s i)
⊢ Eq.{u_3 + 1} (α := Ideal A) (⨆ (i : κ), f i)
    (span
      (image (α := ↥(homogeneousSubmonoid 𝒜))
        (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x))
        (⋃ (i : κ), s i)))
have simp_rw : Eq.{u_3 + 1} (α := Ideal A) (⨆ (i : κ), f i)
  (⨆ (i : κ),
    span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s i))
Tactic: simp_rw [Set.image_iUnion, 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 𝒜
κ : Sort u_4
f : κ → Ideal A
s : (i : κ) → Set ↥(homogeneousSubmonoid 𝒜)
hs :
  ∀ (i : κ),
    f i = span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s i)
⊢ Eq.{u_3 + 1} (α := Ideal A) (⨆ (i : κ), f i)
    (⨆ (i : κ),
      span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s i))
have e_s : Eq (α := κ → Ideal A) (fun (i : κ) ↦ f i) fun (i : κ) ↦
  span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s i)
Tactic: congr
-- 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
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : Membership.mem (γ := Submodule A A) (⨅ (i : κ), f i) x
⊢ Membership.mem (γ := Submodule A A) (⨅ (i : κ), f i)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have simp : ∀ (hx : ∀ (i : κ), x ∈ f i) (i_1 : κ),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ f i_1
Tactic: simp only [Ideal.mem_iInf] at hx ⊢
Cleared hypotheses: 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 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (SupSet.sSup ℐ)
have rw : IsHomogeneous 𝒜 (⨆ a ∈ ℐ, a)
Tactic: rw [sSup_eq_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 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf ℐ)
have rw : IsHomogeneous 𝒜 (⨅ a ∈ ℐ, a)
Tactic: rw [sInf_eq_iInf]
-- 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 𝒜
⊢ Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (⨆ (i : κ), s i)) (⨆ (i : κ), (s i).toIdeal)
have rw : Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (sSup (range fun (i : κ) ↦ s i)))
  (⨆ (i : κ), (s i).toIdeal)
Tactic: rw [iSup, toIdeal_sSup, iSup_range]
-- 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} (ι := ι) (σ := σ) (𝒜 := 𝒜) (sSup (range fun (i : κ) ↦ s i)))
    (⨆ (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)
  (⨆ (s_1 : HomogeneousIdeal 𝒜),
    ⨆ (_ : Membership.mem (γ := Set (HomogeneousIdeal 𝒜)) (range fun (i : κ) ↦ s i) s_1), s_1.toIdeal)
  (⨆ (i : κ), (s i).toIdeal)
Tactic: rw [iSup, toIdeal_sSup, iSup_range]
-- 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} (ι := ι) (σ := σ) (𝒜 := 𝒜) (sSup (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 [iSup, toIdeal_sSup, iSup_range]
-- 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 𝒜
⊢ Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (⨅ (i : κ), s i)) (⨅ (i : κ), (s i).toIdeal)
have rw : Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (sInf (range fun (i : κ) ↦ s i)))
  (⨅ (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 : 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)
⊢ 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)
  (⨅ (s_1 : HomogeneousIdeal 𝒜),
    ⨅ (_ : Membership.mem (γ := Set (HomogeneousIdeal 𝒜)) (range fun (i : κ) ↦ s i) s_1), s_1.toIdeal)
  (⨅ (i : κ), (s i).toIdeal)
Tactic: rw [iInf, toIdeal_sInf, iInf_range]