awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have 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)
Tactic: rw [decompose_mul, DirectSum.mul_eq_dfinsuppSum]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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)
    (↑(((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)
have 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))
Tactic: rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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))
have 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)
Tactic: refine sum_mem fun j _ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((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)) (j + x_2) : ↥(𝒜 (j + x_2)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 (j + x_2))) → ⨁ (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)
have mul : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
  (∑ i_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y),
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + i_1) : ↥(𝒜 (j + i_1)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ↥(𝒜 (j + i_1))) → ⨁ (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)) i_1)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A))
Tactic: rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (∑ i_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y),
      (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + i_1) : ↥(𝒜 (j + i_1)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 (j + i_1))) → ⨁ (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)) i_1)) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))
have mul : ∀ (k : ι),
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) 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)
Tactic: refine sum_mem fun k _ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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
⊢ 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)
have 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)
Tactic: obtain rfl | h := eq_or_ne i (j + k)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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)
⊢ 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)
have 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)
Tactic: obtain rfl | h := eq_or_ne i (j + k)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have mul : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        i) :
    A)
Tactic: 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, *]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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)
    (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (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)
have 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)
Tactic: 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, *]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have 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)
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, *]
Cleared hypotheses: i, hx