-- 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 j : ι
h_1 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
k : ι
h_2 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) k
mul :
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + k) : ↥(𝒜 (j + k)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ↥(𝒜 (j + k))) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                  ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                  ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (j + k)) :
      A)
mul₁ :
  ∀ (h : i ≠ j + k),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + k) : ↥(𝒜 (j + k)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 (j + k))) → ⨁ (i : ι), ↥(𝒜 i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k)) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + k) : ↥(𝒜 (j + k)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ↥(𝒜 (j + k))) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                  ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                  ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
obtain rfl | h := eq_or_ne i (j + k)

Premises used: HAdd.hAdd, eq_or_ne, rfl