-- 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
i : ι
x : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
mem :
  ∀ (x : A) (hx : x ∈ s) (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
zero :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) i) : A)
one :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 : (a : ι) → ↥(𝒜 a)) i) : A)
add :
  ∀ (x y : A),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x →
      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)
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x + y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
mul :
  ∀ (x y : A),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x →
      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)
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
induction hx using Subsemiring.closure_induction generalizing i with
  | mem _ hx => exact Subsemiring.subset_closure <| h i hx
  | zero => simp
  | one =>
    rw [decompose_one, one_def]
    obtain rfl | h := eq_or_ne i 0 <;> simp [of_eq_of_ne, *]
  | add _ _ _ _ h₁ h₂ => simpa using add_mem (h₁ i) (h₂ i)
  | mul x y _ _ h₁ h₂ =>
    classical
    rw [decompose_mul, DirectSum.mul_eq_dfinsuppSum]
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun j _ ↦ ?_
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun k _ ↦ ?_
    obtain rfl | h := eq_or_ne i (j + k) <;> simp [of_eq_of_ne, mul_mem, *]

Premises used: DirectSum.one_def, Subsemiring.subset_closure, AddSubmonoidClass.coe_finsetSum, DFinsupp.sum, DFinsupp.sum_apply, DirectSum.mul_eq_dfinsuppSum, eq_or_ne, DirectSum.decompose_mul, DirectSum.decompose_one, OfNat.ofNat, sum_mem, rfl, MulMemClass.mul_mem, DirectSum.of_eq_of_ne