Lean v4.3.0 change to `simp` defaults breaks proofs

[coproduct]

In Lean v4.3.0, "simp will no longer try to use Decidable instances to rewrite terms" by default (release notes). This change broke these proofs in chapter 3:

theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := by simp

with unsolved goal ⊢ String.append "Str" "ing" = "String" and

#eval third woodlandCritters (by simp)

with simp made no progress.

These can be fixed with the decide config option like so:

theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := (by simp (config := {decide := true}))

#eval third woodlandCritters (by simp (config := {decide := true}))

Thanks for the book! If I find other instances of this breakage, would you rather I comment on this issue or make new ones?