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 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
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₂))
⊢ 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:
rw [Set.image_union]

Premises used: Set.image_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 𝒜)
⊢ 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:
(Submodule.span_union _ _).symm

Premises used: Set.Mem, setOf, Submodule.span_union, Eq.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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₁ ∪
        Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s₂))

Tactic:
exact (Submodule.span_union _ _).symm

Premises used: Submodule.span_union, Eq.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
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))
⊢ IsHomogeneous 𝒜 (⨆ (i : κ), f i)

Tactic:
simp_rw [iff_exists] at h ⊢

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 𝒜
κ : 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)
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))
⊢ ∃ (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
-- 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 𝒜
κ : 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))

Tactic:
⟨⋃ i, s i, ?_⟩

Premises used: Exists.intro, Set.iUnion
-- 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 𝒜
κ : 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)
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)))
⊢ ∃ (S : Set ↥(homogeneousSubmonoid 𝒜)),
    Eq (α := Ideal A) (⨆ (i : κ), f i)
      (span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' S))

Tactic:
refine ⟨⋃ i, s i, ?_⟩
-- 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 𝒜
κ : 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)
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))
⊢ 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:
simp_rw [Set.image_iUnion, Ideal.span_iUnion]

Premises used: Set.image_iUnion, Ideal.span_iUnion
-- 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 𝒜
κ : 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)
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)
⊢ 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:
congr
-- 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 𝒜
κ : 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 (α := κ → Ideal A) (fun (i : κ) ↦ f i) fun (i : κ) ↦
    span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s i)

Tactic:
funext hs

Premises used: funext
-- 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 𝒜
κ : 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 (α := κ → Ideal A) (fun (i : κ) ↦ f i) fun (i : κ) ↦
    span (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (homogeneousSubmonoid 𝒜) x) '' s i)

Tactic:
exact funext hs

Premises used: funext
-- 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 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : Membership.mem (γ := Submodule A A) (⨅ (i : κ), f i) x
simp :
  ∀ (hx : ∀ (i : κ), x ∈ f i) (i_1 : κ),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ f i_1
⊢ Membership.mem (γ := Submodule A A) (⨅ (i : κ), f i)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
simp only [Ideal.mem_iInf] at hx ⊢

Premises used: Ideal.mem_iInf
-- 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 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : ∀ (i : κ), x ∈ f i
⊢ ∀ (i_1 : κ),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ f i_1

Tactic:
fun j => h _ _ (hx j)

Premises used: Set.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 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : ∀ (i : κ), x ∈ f i
⊢ ∀ (i_1 : κ),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ f i_1

Tactic:
exact fun j => h _ _ (hx j)
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
κ : Sort u_4
κ' : κ → Sort u_5
f : (i : κ) → κ' i → Ideal A
h : ∀ (i : κ) (j : κ' i), IsHomogeneous 𝒜 (f i j)
⊢ IsHomogeneous 𝒜 (⨆ (i : κ), ⨆ (j : κ' i), f i j)

Tactic:
IsHomogeneous.iSup fun i => IsHomogeneous.iSup <| h i

Premises used: Ideal.IsHomogeneous.iSup
-- 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 𝒜
κ : Sort u_4
κ' : κ → Sort u_5
f : (i : κ) → κ' i → Ideal A
h : ∀ (i : κ) (j : κ' i), IsHomogeneous 𝒜 (f i j)
⊢ IsHomogeneous 𝒜 (⨅ (i : κ), ⨅ (j : κ' i), f i j)

Tactic:
IsHomogeneous.iInf fun i => IsHomogeneous.iInf <| h i

Premises used: Ideal.IsHomogeneous.iInf
-- 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 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
rw : IsHomogeneous 𝒜 (⨆ a ∈ ℐ, a)
⊢ IsHomogeneous 𝒜 (SupSet.sSup ℐ)

Tactic:
rw [sSup_eq_iSup]

Premises used: sSup_eq_iSup
-- 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 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨆ a ∈ ℐ, a)

Tactic:
iSup₂ h

Premises used: Ideal.IsHomogeneous.iSup₂
-- 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 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨆ a ∈ ℐ, a)

Tactic:
exact iSup₂ h

Premises used: Ideal.IsHomogeneous.iSup₂
-- 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 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
rw : IsHomogeneous 𝒜 (⨅ a ∈ ℐ, a)
⊢ IsHomogeneous 𝒜 (InfSet.sInf ℐ)

Tactic:
rw [sInf_eq_iInf]

Premises used: sInf_eq_iInf
-- 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 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨅ a ∈ ℐ, a)

Tactic:
iInf₂ h

Premises used: Ideal.IsHomogeneous.iInf₂
-- 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 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨅ a ∈ ℐ, a)

Tactic:
exact iInf₂ h

Premises used: Ideal.IsHomogeneous.iInf₂
-- 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 𝒜
⊢ (↑⊤ : Set A) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, 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 𝒜
⊢ (↑⊥ : Set A) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I J : HomogeneousIdeal 𝒜
⊢ (↑(I ⊔ J) : Set A) = (↑I : Set A) + (↑J : Set A)

Tactic:
Submodule.coe_sup _ _

Premises used: Submodule.coe_sup
-- 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 : HomogeneousIdeal 𝒜
⊢ (↑(I ⊓ J) : Set A) = (↑I : Set A) ∩ (↑J : Set A)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, 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 𝒜
⊢ Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
⊢ Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) ⊥) ⊥

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
ℐ : Set (HomogeneousIdeal 𝒜)
⊢ (sSup ℐ).toIdeal = ⨆ s ∈ ℐ, s.toIdeal

Tactic:
rfl

Premises used: Set.Mem, iSup, setOf, 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 𝒜
ℐ : Set (HomogeneousIdeal 𝒜)
⊢ (sInf ℐ).toIdeal = ⨅ s ∈ ℐ, s.toIdeal

Tactic:
rfl

Premises used: iInf, Set.Mem, 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 𝒜
κ : 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)
rw₂ rw₃ : Eq.{u_3 + 1} (α := Ideal A) (⨆ (i : κ), (s i).toIdeal) (⨆ (i : κ), (s i).toIdeal)
⊢ Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (⨆ (i : κ), s i)) (⨆ (i : κ), (s i).toIdeal)

Tactic:
rw [iSup, toIdeal_sSup, iSup_range]

Premises used: iSup, iSup_range, HomogeneousIdeal.toIdeal_sSup
-- 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 𝒜
κ : 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)
rw₂ rw₃ : Eq.{u_3 + 1} (α := Ideal A) (⨅ (i : κ), (s i).toIdeal) (⨅ (i : κ), (s i).toIdeal)
⊢ Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (⨅ (i : κ), s i)) (⨅ (i : κ), (s i).toIdeal)

Tactic:
rw [iInf, toIdeal_sInf, iInf_range]

Premises used: iInf, iInf_range, HomogeneousIdeal.toIdeal_sInf
-- 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 𝒜
κ : Sort u_4
κ' : κ → Sort u_5
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (⨆ (i : κ), ⨆ (j : κ' i), s i j))
    (⨆ (i : κ), ⨆ (j : κ' i), (s i j).toIdeal)

Tactic:
simp_rw [toIdeal_iSup]

Premises used: HomogeneousIdeal.toIdeal_iSup
-- 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 𝒜
κ : Sort u_4
κ' : κ → Sort u_5
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ Eq (α := Ideal A) (toIdeal.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (⨅ (i : κ), ⨅ (j : κ' i), s i j))
    (⨅ (i : κ), ⨅ (j : κ' i), (s i j).toIdeal)

Tactic:
simp_rw [toIdeal_iInf]

Premises used: HomogeneousIdeal.toIdeal_iInf
-- 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 : HomogeneousIdeal 𝒜
⊢ I = ⊤ ↔ I.toIdeal = ⊤

Tactic:
toIdeal_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, HomogeneousIdeal.toIdeal_injective, Iff.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ I = ⊥ ↔ I.toIdeal = ⊥

Tactic:
toIdeal_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, HomogeneousIdeal.toIdeal_injective, Iff.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
I J : HomogeneousIdeal 𝒜
⊢ (I + J).toIdeal = I.toIdeal + J.toIdeal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : 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
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 [Ideal.IsHomogeneous.iff_exists] at HI HJ ⊢

Premises used: Ideal.IsHomogeneous.iff_exists