chore: remove (d)simp only []

[grunweg]

Either remove them (when they were unnecessary), or replace by something more low-level.

---

I'm happy to make them simp only instead, if that is preferred.

[github-actions]

PR summary 6f6e20aa30

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[b-mehta]

I'd instinctively do simp only in these cases, but there's a strong argument that beta_reduce should be preferred. Is it the case that if simp only works, then beta_reduce does too? And if so, should we insist on that (eg with a linter)?

[grunweg]

IIUC, simp only applies more than beta reduction (but also reduces recursors, let bindings, matches, for instance). So, beta_reduce working (almost surely) means simp only works, but not conversely.

[b-mehta]

Oh right, good point. I still think we should try to make beta_reduce more discoverable, and perhaps use the tactic analysis linter to suggest using it over simp only in the case that both work, but that's not so important for your PR.