doc(Tactic/Translate/ToDual): add deployment guide for @[to_dual]

[kim-em]

This PR expands the documentation for @[to_dual] with practical advice for deploying it to existing code.

Module docstring (Mathlib/Tactic/Translate/ToDual.lean): adds a "Deploying @[to_dual] to existing code" section covering name agreement, attribute propagation, docstring syntax ordering, declaration order dependencies, and known structural mismatches (conjunct reordering, type class gaps, interval argument swapping).

Attribute docstring: adds a note that @[simp] is not auto-copied (must use (attr := simp)), and shows the correct ordering when combining (attr := ...) with docstrings.

Agent skill (.claude/skills/to_dual/SKILL.md): detailed step-by-step instructions for an AI agent deploying @[to_dual], including how to identify candidates, common patterns, and debugging.

🤖 Prepared with Claude Code

[github-actions]

PR summary 3efa02168f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ OrderBot.bddBelow
+ isGLB_lt_iff
+ lowerBounds_empty
+ lt_isGLB_iff
+ lt_isLUB_iff
++ isLUB_lt_iff
+++ OrderTop.bddAbove
++++++ upperBounds_empty
- min_self

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[vihdzp]

As for the claude stuff, have we come to a consensus on whether this belongs on the Mathlib repo or on users' config files? I recall the last time something like this got brought up, the consensus was the latter.

[JovanGerb]

The claude file doesn't mention anything about to_dual self, to_dual none or to_dual existing, and also nothing about (reorder := ...).

When a theorem has hypotheses or parameters as explicit arguments that appear in a different order in the dual declaration, it is important to use the (reorder := ...) option to reorder them. For example

@[to_dual (reorder := hx hy)]
lemma unbot_le_unbot_iff (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x.unbot hx ≤ y.unbot hy ↔ x ≤ y := by simp

[kim-em]

The claude file doesn't mention anything about to_dual self, to_dual none or to_dual existing, and also nothing about (reorder := ...).

When a theorem has hypotheses or parameters as explicit arguments that appear in a different order in the dual declaration, it is important to use the (reorder := ...) option to reorder them. For example

@[to_dual (reorder := hx hy)]
lemma unbot_le_unbot_iff (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x.unbot hx ≤ y.unbot hy ↔ x ≤ y := by simp

Added in 2e25372.

[kim-em]

As for the claude stuff, have we come to a consensus on whether this belongs on the Mathlib repo or on users' config files? I recall the last time something like this got brought up, the consensus was the latter.

At this point, a repository without a .claude seems sort of mean. :-) How are your assistants meant to find their way around. It means people reduplicate work explaining things work. It's just an essential facet of modern documentation!

[kim-em]

Thanks, @vihdzp and @JovanGerb for your helpful and patient corrections! I hope this will be a good experiment in writing more detailed docs, eventually. I think I've addressed your comments above.

[JovanGerb]

At this point, a repository without a .claude seems sort of mean. :-)

I honestly can't tell if this was written by Claude lol

[MichaelStollBayreuth]

This had no labels, which usually leads to a wrong person to be assigned by the bot. Assigning @JovanGerb instead.

[JovanGerb]

The added explanation in the ToDual module docstring seems reasonable. Though I don't know why we would have a separate documentation in the module docstring from the docstring on the to_dual attribute itself, it seems a bit inefficient like this.

I have more trouble with the .claude folder. If I understand it correctly, this adds a pay-walled feature to mathlib that users need to pay for if they want to use it. This seems undesirable to me. So you'd have to find another reviewer to approve this.

[JovanGerb]

Suggested change

	2. Guessing the dual declaration's name using `nameDict` below
	2. Guessing the dual declaration's name using `nameDict` and `abbreviationDict` below