fix: revert CCL/Group.lean and CCL/Finset.lean to master

The @[to_dual existing] attributes in these files are incompatible
with the ConditionallyCompletePartialOrder instance from leanprover-community#35047.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

@@ -175,21 +175,6 @@ theorem exists_eq_ciSup_of_finite [Nonempty ι] [Finite ι] {f : ι → α} : 
 theorem exists_eq_ciInf_of_finite [Nonempty ι] [Finite ι] {f : ι → α} : ∃ i, f i = ⨅ i, f i :=
   Nonempty.csInf_mem (range_nonempty f) (finite_range f)
 
--- Register dual pairs in this section for downstream `@[to_dual]` usage.
--- Note: Finset.Nonempty.csSup_eq_max' and Finset.ciSup_eq_max'_image cannot be registered
--- because Finset.max' / Finset.min' are not registered as @[to_dual] pairs.
-attribute [to_dual existing] Finset.Nonempty.csSup_mem
-attribute [to_dual existing] Set.Nonempty.csSup_mem
-attribute [to_dual existing Set.Finite.lt_csInf_iff] Set.Finite.csSup_lt_iff
-attribute [to_dual existing] Finset.ciSup_mem_image
-attribute [to_dual existing] Set.Finite.ciSup_mem_image
-attribute [to_dual existing Set.Finite.lt_ciInf_iff] Set.Finite.ciSup_lt_iff
-attribute [to_dual existing List.iInf_mem_map_of_exists_le_sInf_empty]
-  List.iSup_mem_map_of_exists_sSup_empty_le
-attribute [to_dual existing Multiset.iInf_mem_map_of_exists_le_sInf_empty]
-  Multiset.iSup_mem_map_of_exists_sSup_empty_le
-attribute [to_dual existing] exists_eq_ciSup_of_finite
-
 end ListMultiset
 
 end ConditionallyCompleteLinearOrder
@@ -208,8 +193,6 @@ lemma le_ciSup (i : ι) : f i ≤ ⨆ j, f j := by
 lemma ciInf_le (i : ι) : ⨅ j, f j ≤ f i :=
   le_ciSup (α := αᵒᵈ) f i
 
-attribute [to_dual existing Finite.ciInf_le] Finite.le_ciSup
-
 end Finite
 
 /-!
@@ -247,9 +230,6 @@ lemma sup'_univ_eq_ciSup (f : ι → α) : univ.sup' univ_nonempty f = ⨆ i, f
 lemma inf'_univ_eq_ciInf (f : ι → α) : univ.inf' univ_nonempty f = ⨅ i, f i := by
   simp [inf'_eq_csInf_image, iInf]
 
--- Note: sup'_eq_csSup_image / inf'_eq_csInf_image cannot be registered because
--- Finset.sup' / Finset.inf' are not registered as @[to_dual] pairs.
-
 end ConditionallyCompleteLattice
 
 section ConditionallyCompleteLinearOrderBot

Mathlib/Order/ConditionallyCompleteLattice/Group.lean

@@ -34,8 +34,6 @@ lemma ciInf_mul_ciInf_le_ciInf_mul [MulLeftMono α] [MulRightMono α]
     (⨅ i, f i) * ⨅ i, g i ≤ ⨅ i, f i * g i :=
   le_ciInf fun i ↦ mul_le_mul' (ciInf_le hf i) (ciInf_le hg i)
 
-attribute [to_dual existing ciInf_mul_ciInf_le_ciInf_mul] ciSup_mul_le_ciSup_mul_ciSup
-
 end Mul
 
 section Group
@@ -73,8 +71,4 @@ theorem ciSup_mul_ciSup_le [MulLeftMono α] [MulRightMono α] {a : α} {g : ι 
     (H : ∀ i j, g i * h j ≤ a) : iSup g * iSup h ≤ a :=
   ciSup_mul_le fun _ => mul_ciSup_le <| H _
 
-attribute [to_dual existing le_mul_ciInf] mul_ciSup_le
-attribute [to_dual existing le_ciInf_mul] ciSup_mul_le
-attribute [to_dual existing le_ciInf_mul_ciInf] ciSup_mul_ciSup_le
-
 end Group