chore: adapt to decide := false in simp

[collares]

Future-proofing for leanprover/lean4#2722. A comment on SimpConfig is missing but I didn't exactly know what to write.

[JLimperg]

I'd prefer to match stock simp behaviour, i.e. keep decide := false by default. Reasons:

• Less surprising behaviour; Aesop simp_all is really just simp_all.
• aesop? would otherwise have to start generating simp_all (config := { decide := true }) invocations.

Does decide := false break mathlib a lot?

[collares]

@JLimperg It's easy to fix it on the mathlib side, I just mistakenly thought decide := true would be preferred in aesop. The one remaining non-comment change in this PR is needed to fix this error when decide is not used by default:

./lake-packages/aesop/././Aesop/Search/Expansion/Norm.lean:380:60: error: unsolved goals
rs : RuleSet
normSimpContext : NormSimpContext
options : Options'
goal : MVarId
mvars : UnorderedArraySet MVarId
mvarsHashSet : HashSet MVarId := HashSet.ofArray (UnorderedArraySet.toArray mvars)
normSteps : Array NormStep :=
  #[NormStep.runPreSimpRules options mvars, NormStep.unfold rs options mvarsHashSet,
    NormStep.simp rs normSimpContext options mvarsHashSet, NormStep.runPostSimpRules options mvars]
⊢ 0 < Nat.succ (Nat.succ (Nat.succ 1))

[JLimperg]

Great, thanks! I'll merge when CI is green.