awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I J : HomogeneousSubmodule 𝒜 ℳ
h : ∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J
x : M
⊢ ∀ (a : ιM),
    (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) a) : M) ∈
        I.toSubmodule ↔
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) a) : M) ∈
        J.toSubmodule

Tactic:
fun i ↦ h i _ (decompose ℳ _ i).2

Premises used: Set.Mem, Subtype.val, DFunLike.coe, Subtype.property, DirectSum.decompose
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I J : HomogeneousSubmodule 𝒜 ℳ
h : ∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J
x : M
⊢ ∀ (a : ιM),
    (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) a) : M) ∈
        I.toSubmodule ↔
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) a) : M) ∈
        J.toSubmodule

Tactic:
exact fun i ↦ h i _ (decompose ℳ _ i).2

Premises used: Subtype.val, DFunLike.coe, Subtype.property, DirectSum.decompose
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I : HomogeneousSubmodule 𝒜 ℳ
x : M
⊢ x ∈ I.toSubmodule ↔ x ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R : Subsemiring A
hR : IsHomogeneous 𝒜 R
a : A
⊢ a ∈ R ↔
    ∀ (i : ι), (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ R

Tactic:
AddSubmonoidClass.IsHomogeneous.mem_iff 𝒜 _ hR

Premises used: DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
x_1 x_2 : HomogeneousSubsemiring 𝒜
x : Subsemiring A
hx : IsHomogeneous 𝒜 x
y : Subsemiring A
hy : IsHomogeneous 𝒜 y
h : x = y
⊢ { toSubsemiring := x, is_homogeneous' := hx : HomogeneousSubsemiring 𝒜 } =
    { toSubsemiring := y, is_homogeneous' := hy }

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R : HomogeneousSubsemiring 𝒜
⊢ IsHomogeneous 𝒜 R

Tactic:
R.is_homogeneous'

Premises used: Set.Mem, HomogeneousSubsemiring.is_homogeneous', DirectSum.SetLike.IsHomogeneous
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R S : HomogeneousSubsemiring 𝒜
h : R.toSubsemiring = S.toSubsemiring
⊢ R = S

Tactic:
HomogeneousSubsemiring.toSubsemiring_injective h

Premises used: HomogeneousSubsemiring.toSubsemiring_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R S : HomogeneousSubsemiring 𝒜
h : ∀ (i : ι), ∀ a ∈ 𝒜 i, a ∈ R ↔ a ∈ S
⊢ R = S

Tactic:
AddSubmonoidClass.IsHomogeneous.ext R.2 S.2 h

Premises used: DirectSum.AddSubmonoidClass.IsHomogeneous.ext, HomogeneousSubsemiring.is_homogeneous'
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R : HomogeneousSubsemiring 𝒜
a : A
⊢ a ∈ R.toSubsemiring ↔ a ∈ R

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x x_1 : A
hx : x_1 ∈ s
i : ι
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
Subsemiring.subset_closure <| h i hx

Premises used: Subsemiring.subset_closure
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x x_1 : A
hx : x_1 ∈ s
i : ι
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
exact Subsemiring.subset_closure <| h i hx

Premises used: Subsemiring.subset_closure
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x : A
i : ι
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x : A
i : ι
one :
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
rw [decompose_one, one_def]

Premises used: DirectSum.one_def, DirectSum.decompose_one
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x : A
i : ι
one :
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A)
one₁ :
  ∀ (h : i ≠ 0),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                  (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
obtain rfl | h := eq_or_ne i 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x : A
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A)

Tactic:
simp [of_eq_of_ne, *]

Premises used: DirectSum.of_eq_of_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h_1 :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x : A
i : ι
h : i ≠ 0
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
simp [of_eq_of_ne, *]

Premises used: DirectSum.of_eq_of_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x x_1 y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x_1
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
i : ι
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x_1 + y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
simpa using add_mem (h₁ i) (h₂ i)

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x_1 x y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
i : ι
mul :
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)
                fun (x : ι) (ai : ↥(𝒜 x)) ↦
                DFinsupp.sum (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)
                  fun (x_2 : ι) (aj : ↥(𝒜 x_2)) ↦
                  ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (x + x_2) : ↥(𝒜 (x + x_2)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 (x + x_2))) → ⨁ (i : ι), ↥(𝒜 i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _ ai aj) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
rw [decompose_mul, DirectSum.mul_eq_dfinsuppSum]

Premises used: DirectSum.mul_eq_dfinsuppSum, DirectSum.decompose_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x_1 x y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
i : ι
mul :
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (∑ i_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)
                  fun (x_2 : ι) (aj : ↥(𝒜 x_2)) ↦
                  ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (i_1 + x_2) : ↥(𝒜 (i_1 + x_2)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 (i_1 + x_2))) → ⨁ (i : ι), ↥(𝒜 i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                      ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i_1)
                      aj) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)
                fun (x : ι) (ai : ↥(𝒜 x)) ↦
                DFinsupp.sum (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)
                  fun (x_2 : ι) (aj : ↥(𝒜 x_2)) ↦
                  ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (x + x_2) : ↥(𝒜 (x + x_2)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 (x + x_2))) → ⨁ (i : ι), ↥(𝒜 i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _ ai aj) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]

Premises used: AddSubmonoidClass.coe_finsetSum, DFinsupp.sum, DFinsupp.sum_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x_1 x y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
i : ι
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (∑ i_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)
                  fun (x_2 : ι) (aj : ↥(𝒜 x_2)) ↦
                  ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (i_1 + x_2) : ↥(𝒜 (i_1 + x_2)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 (i_1 + x_2))) → ⨁ (i : ι), ↥(𝒜 i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                      ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i_1)
                      aj) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))

Tactic:
sum_mem fun j _ ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x_1 x y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
i : ι
mul :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j →
      Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
        (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)
                    fun (x_3 : ι) (aj : ↥(𝒜 x_3)) ↦
                    ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + x_3) : ↥(𝒜 (j + x_3)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                        (a : ↥(𝒜 (j + x_3))) → ⨁ (i : ι), ↥(𝒜 i))
                      (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                        ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                        aj) :
                  ⨁ (i : ι), ↥(𝒜 i)) :
                (a : ι) → ↥(𝒜 a))
              i) :
          A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (∑ i_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)
                  fun (x_2 : ι) (aj : ↥(𝒜 x_2)) ↦
                  ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (i_1 + x_2) : ↥(𝒜 (i_1 + x_2)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 (i_1 + x_2))) → ⨁ (i : ι), ↥(𝒜 i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                      ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i_1)
                      aj) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))

Tactic:
refine sum_mem fun j _ ↦ ?_

Premises used: sum_mem