grind freeze

Stream: lean4

[Frédéric Dupuis]

The following example seems to just freeze on the grind call on v4.29.0-rc1 (i.e. the orange bar just stays forever, it doesn't even time out):

import Mathlib.Algebra.BigOperators.Group.Finset.Basic

variable {ι M : Type} [AddCommMonoid M] [Fintype ι]

example (f g : ι → M) : ∑ x, (f x + g x) = ∑ x, f x + ∑ x, g x := by
  grind [Finset.sum_add_distrib]
  sorry

(I briefly tried to get a mathlib-free MWE by defining a toy version of Finset.sum, to no avail.)