[Merged by Bors] - chore: reorder arguments in DirSupClosed

[vihdzp]

We move d ⊆ s out of an unrelated binder.

---

• depends on: [Merged by Bors] - chore: new file for sets closed under directed suprema #37273

[github-actions]

PR summary 251d9c0ff4

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

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./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).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore: new file for sets closed under directed suprema #37273
  By Dependent Issues (🤖). Happy coding!

[Vierkantor]

I'm going to (weakly) push back on this change. Even though I agree with you: of the two versions, the new one is better code. It's because I don't see that this makes things better enough. Is there a proof in a downstream project that becomes noticeably easier when you change this? And if that is the case, this PR is not enough, I think we should not change only one def: can we turn this into a general code style guideline, write a linter (optional but would be very good to have) and then make the improvement everywhere in Mathlib?

[vihdzp]

I wouldn't say this makes the proofs easier, but I do think it makes writing them easier. The binders are in a more predictable order, and I it means I don't have to introduce four other variables before being reminded "ah! d is a subset of s".

If we want to turn this into a guideline, I'd imagine it be saying that h → ∀ a, p a is the preferred spelling of ∀ a, h → p a.

[Vierkantor]

If we want to turn this into a guideline, I'd imagine it be saying that h → ∀ a, p a is the preferred spelling of ∀ a, h → p a.

Agreed! I think we have a simproc even that does this rewrite. So if you could add this rule to the review checklist (or similar) then I'll approve it and we can look together at doing this in more places in Mathlib.

[b-mehta]

I agree we should make this change globally too, but perhaps for pragmatic reasons (and since there's a few PRs around Scott and ScottHausdorff I'd like to prioritise right now), @Vierkantor do you think we could merge this one and do the broader changes in another PR?
(I also suspect there won't be many changes like this to make!)

[Vierkantor]

Okay! It was only weak pushback, so if you feel it is valuable in this form then I retract my objection. :)

bors r+

[mathlib-bors]

Build failed (retrying...):

• ci (staging) / Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Lint style