chore(Order): add to_dual tags in Mathlib/Order/ConditionallyCompleteLattice/Indexed

[CoolRmal]

This PR adds to_dual tags in Mathlib/Order/ConditionallyCompleteLattice/Indexed. I also add to_dual tags to some lemmas in Mathlib/Order/ConditionallyCompleteLattice/Basic in order to make to_dual works in Mathlib/Order/ConditionallyCompleteLattice/Indexed.

Created with the help of codex.

[github-actions]

PR summary bb8990f972

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

- BddBelow.range_iInf_of_iUnion_range
- IsGLB.ciInf_eq
- IsGLB.ciInf_set_eq
- Set.Ici_ciSup
- WithBot.ciSup_empty
- WithBot.coe_iInf
- WithBot.coe_iSup
- WithBot.sSup_empty
- cbiInf_eq_ciInf_subtype
- cbiInf_id
- ciInf_and
- ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
- ciInf_image
- ciInf_inf_eq
- ciInf_le
- ciInf_le_of_le
- ciInf_mono
- ciInf_mono_of_forall_exists
- ciInf_prod
- ciInf_set_le
- ciInf_subtype
- ciInf_subtype_fun
- ciInf₂_le
- csInf_eq_of_forall_ge_of_forall_gt_exists_lt
- csInf_image
- exists_lt_of_ciInf_lt
- isGLB_ciInf
- isGLB_ciInf_set
- le_ciInf
- le_ciInf_exists
- le_ciInf_iff
- le_ciInf_set_iff
- map_ciInf
- map_ciInf_set
- map_csInf
- map_csInf'
- u_ciInf
- u_ciInf_set
- u_csInf
- u_csInf'

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit bb8990f).

• +2 new declarations
• −2 removed declarations

-WithBot.ciSup_empty
+WithBot.iSup_empty
+ciInf_exists_le
-le_ciInf_exists

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit bb8990f972
Reference commit 99a705f943

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