[Merged by Bors] - chore: remove unnecessary term or tactic set_option in with backwards-compatibility flags

[grunweg]

As far as I can tell, this removes all set_option ... false in norm_num 🎉

Inspired by the linter in #13653 (but not covered by it yet; so far, that linter only checks the set_option command).

---

[github-actions]

PR summary 66bd80bbd0

Import changes

No significant changes to the import graph

---

Declarations diff

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

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[grunweg]

!bench

[leanprover-bot]

Here are the benchmark results for commit 8bb74a8.
There were significant changes against commit 491655d:

  Benchmark                                   Metric         Change
  =================================================================
- ~Mathlib.RingTheory.Polynomial.ScaleRoots   instructions    49.6%

[grunweg]

Lesson learned: these options can be performance-sensitive. Reverted the ScaleRoots change and added a comment.
@MichaelStollBayreuth Can I ask you to run your script on the benchmarking run above? I'd like to know if there are any other files with significant regressions. Thank you (that script is really nice - I wish the speed-center also allowed sorting by the absolute change)!

[MichaelStollBayreuth]

General information:
  build:                                               +19.345 * 10⁹ (+0.0159%)

5 files got slower by at least 10⁹ instructions:
  Mathlib.RingTheory.Polynomial.ScaleRoots:            +11.369 * 10⁹ (+49.6%)
  Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds:
                                                       +4.1656 * 10⁹ (+6.95%)
  Mathlib.Topology.Homotopy.Path:                      +2.7929 * 10⁹ (+3.84%)
  Mathlib.Data.Finset.Pointwise:                       +1.8385 * 10⁹ (+1.25%)
  Mathlib.RingTheory.Localization.Basic:               +1.4865 * 10⁹ (+1.33%)

1 file got slower by at least 10%:
  Mathlib.RingTheory.Polynomial.ScaleRoots:                           +49.6%

2 files got faster by at least 10⁹ instructions:
  Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm:
                                                       -3.9465 * 10⁹ (-1.32%)
  Mathlib.Algebra.Category.ModuleCat.ChangeOfRings:    -1.1021 * 10⁹ (-0.278%)

No file got faster by at least 10%.

[grunweg]

I looked at the files which slowed down by more than 10^9 instructions. ScaleRoots clearly needs to be reverted (with a comment). The simp call in Data.Finset.Pointwise speeds up a lot with that option (250 ->50ms locally), hence I also reverted that. In Trigonometric/Bounds, the situation seems murkier (the refine's are slow either way, but perhaps go from 850->800ms)... but I've reverted to try another benchmarking run.
The other changes seems inconclusive or a wash; I tend to leave those in.

So, let's re-benchmark this!

[grunweg]

!bench

[leanprover-bot]

Here are the benchmark results for commit 66bd80b.
There were no significant changes against commit 491655d.

[MichaelStollBayreuth]

General information:
build: +1.0814 * 10⁹ (+0.000889%)

1 file got slower by at least 10⁹ instructions:
Mathlib.Topology.Homotopy.Path: +2.7944 * 10⁹ (+3.84%)

No file got slower by at least 10%.

3 files got faster by at least 10⁹ instructions:

  Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm:
                                                       -2.1722 * 10⁹ (-0.726%)
  Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds:
                                                       -1.9068 * 10⁹ (-3.18%)
  Mathlib.Algebra.Category.ModuleCat.ChangeOfRings:    -1.1096 * 10⁹ (-0.280%)

No file got faster by at least 10%.

[kim-em]

bors merge

[mathlib-bors]

Already running a review

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style