-- Mathlib.Tactic.Translate.ToDual
/-- The attribute `to_dual` can be used to automatically transport theorems
and definitions (but not inductive types and structures) to their dual version.
It uses the same implementation as `to_additive`.

To use this attribute, just write:

```
@[to_dual]
theorem max_comm' {α} [LinearOrder α] (x y : α) : max x y = max y x := max_comm x y
```

This code will generate a theorem named `min_comm'`. It is also
possible to manually specify the name of the new declaration:

```
@[to_dual le_max_left]
lemma min_le_left (a b : α) : min a b ≤ a := sorry
```

An existing documentation string will _not_ be automatically used, so if the theorem or definition
has a doc string, a doc string for the dual version should be passed explicitly to `to_dual`.

```
/-- The maximum is commutative. -/
@[to_dual /-- The minimum is commutative. -/]
theorem max_comm' {α} [LinearOrder α] (x y : α) : max x y = max y x := max_comm x y
```

Use the `(reorder := ...)` syntax to reorder the arguments compared to the dual declaration.
This is specified using cycle notation. For example `(reorder := α β, 5 6)` swaps the arguments
`α` and `β` with each other and the fifth and the sixth argument and `(reorder := 3 4 5)` will move
the fifth argument before the third argument. For example, this is used when tagging `LE.le`
with `to_dual self (reorder := 3 4)`, so that `a ≤ b` gets transformed into `b ≤ a`.

Use the `to_dual self` syntax to mark the lemma as its own dual. This is needed if the lemma is
its own dual, up to a reordering of its arguments. `to_dual self` (and `to_dual existing`) tries to
autogenerate the `(reorder := ...)` argument, so it is usually not necessary to give it explicitly.

Use the `to_dual existing` syntax to use an existing dual declaration,
instead of automatically generating it.

Use the `(attr := ...)` syntax to apply attributes to both the original and the dual version:
```
@[to_dual (attr := simp)] lemma min_self (a : α) : min a a = a := sorry
```

The `reassoc` attribute in category theory interacts with `to_dual` in a unique way, because it
generates `_assoc` theorems that aren't dual to any other theorem. To deal with this, the `reassoc`
attribute will add a `to_dual none` tag to an `_assoc` theorem if the original theorem was
already tagged with `to_dual`. This also works with `to_dual (attr := reassoc)`.

The `(rename := ...)` syntax can be used for specifying the argument names of the generated
declaration, overriding the automatic translation of names. For example, `(rename := x → a, y ↔ z)`
will translate `lemma min_foo (x y z : α) ...` to `lemma max_foo (a z y : α) ...`.

Some definitions are dual to something other than the dual of their value. Some examples:
- `Ico a b := { x | a ≤ x ∧ x < b }` is dual to `Ioc b a := { x | b < x ∧ x ≤ a }`.
- `Monotone f := ∀ ⦃a b⦄, a ≤ b → f a ≤ f b` is dual to itself.
- `DecidableLE α := ∀ a b : α, Decidable (a ≤ b)` is dual to itself.

To be able to translate a term involving such constants, `to_dual` needs to insert casts,
so that the term's correctness doesn't rely on unfolding them.
You can instruct `to_dual` to do this using the `to_dual_insert_cast` or `to_dual_insert_cast_fun`
commands.

When troubleshooting `to_dual`, you can see what it is doing by replacing it with `to_dual?` and/or
by using `set_option trace.translate_detail true`.
 -/
Mathlib.Tactic.ToDual.to_dual : Lean.ParserDescr