Fix 2 more instances of leanprover/fp-lean#137

[overminder]

This follows Adam's suggestion to use decide instead of simp. I've verified that these 2 lines build on Lean 4.3 and 4.4.

Why a pull request: I did read CONTRIBUTING.md, though I still chose to open a pull request:

• I'm a Microsoft employee, and I've linked my account with the Microsoft org, so I shouldn't need to sign a separate CLA.
• I'm under the impression that this fix falls into the category of "having prior discussion" (Lean v4.3.0 change to simp defaults breaks proofs #137), and I saw similar fix was done in 3a53e94.

[david-christiansen]

Thanks!

The primary concern with pull requests is not the CLA - it's that the whole book needs to make coherent sense, and I don't know a better way to do it than to automate what checks I can and to make sure that I have an understanding of what is where. It's often not just a matter of making the examples compile - the changes to the examples will likely motivate changes to the text, or even restructurings of sections or reordering of content. Every line of example code is connected to the text.

I'll do a maintenance release of the book soon, where I update it to the latest Lean, but this and other changes will require a larger restructuring of how proofs are presented.

Thanks again!

[overminder]

A coherent content makes a lot of sense! Thanks for the detailed explanations. Loved the book as much as "The Little Typer" and the PDX course :)