no goals
ι : Type u_2
inst✝⁴ : DecidableEq ι
A : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ a * a' =
    ∑ ij in Dfinsupp.support a ×ˢ Dfinsupp.support a',
      ↑(of (fun i => (fun i => A i) i) (ij.fst + ij.snd)) (GradedMonoid.GMul.mul (↑a ij.fst) (↑a' ij.snd))
simp only [mul_eq_dfinsupp_sum, Dfinsupp.sum, Finset.sum_product]