refactor(Analysis): golf Mathlib/Analysis/Complex/Hadamard

[yuanyi-350]

• simplifies scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip by closing the strip inequalities with nlinarith
• rewrites scale_bddAbove to use BddAbove.mono and a direct image witness for the scaled strip

Extracted from #37968

[yuanyi-350]

!bench

[leanprover-radar]

Benchmark results for 552cc8c against d104ce7 are in. No significant results found. @yuanyi-350

• 🟥 build//instructions: +20.5G (+0.01%)

Small changes (1✅, 1🟥)

• 🟥 build/module/Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner//instructions: +380.7M (+4.96%)
• ✅ build/module/Mathlib.Tactic.Attr.Core//instructions: -417.7M (-14.92%)

[github-actions]

PR summary d104ce7317

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 technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[yuanyi-350]

I ran a profiler comparison for the changed declarations in this PR.

Results (seconds):

• Complex.HadamardThreeLines.scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip: 1.370519 -> 0.408817 (-70.17%)
• Complex.HadamardThreeLines.scale_bddAbove: 0.293973 -> 0.013563 (-95.39%)

Overall:

• both changed declarations are faster, with no regression among the profiled declarations

[themathqueen]

!bench

Like I said before, you really don't need to be benching for these small golfing PRs. It's not going to give you an accurate reading. Your profiler performance comparison is more than enough in this situation.