ι : Type u_1
σ : Type u_3
S : Type ?u.100155
R : Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ∑ i in Dfinsupp.support r ×ˢ Dfinsupp.support r',
      ↑(↑(↑(of (fun i => (fun i => { x // x ∈ A i }) i) (i.fst + i.snd)) (GradedMonoid.GMul.mul (↑r i.fst) (↑r' i.snd)))
          n) =
    ∑ ij in Finset.filter (fun ij => ij.fst + ij.snd = n) (Dfinsupp.support r ×ˢ Dfinsupp.support r'),
      ↑(↑r ij.fst) * ↑(↑r' ij.snd)
ι : Type u_1
σ : Type u_3
S : Type ?u.100155
R : Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ↑(↑(r * r') n) =
    ∑ ij in Finset.filter (fun ij => ij.fst + ij.snd = n) (Dfinsupp.support r ×ˢ Dfinsupp.support r'),
      ↑(↑r ij.fst) * ↑(↑r' ij.snd)
rw [mul_eq_sum_support_ghas_mul, Dfinsupp.finset_sum_apply, AddSubmonoidClass.coe_finset_sum]
no goals
ι : Type u_1
σ : Type u_3
S : Type ?u.100155
R : Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ∑ i in Dfinsupp.support r ×ˢ Dfinsupp.support r',
      ↑(↑(↑(of (fun i => (fun i => { x // x ∈ A i }) i) (i.fst + i.snd)) (GradedMonoid.GMul.mul (↑r i.fst) (↑r' i.snd)))
          n) =
    ∑ ij in Finset.filter (fun ij => ij.fst + ij.snd = n) (Dfinsupp.support r ×ˢ Dfinsupp.support r'),
      ↑(↑r ij.fst) * ↑(↑r' ij.snd)
simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]