refactor(Data/Fintype/Order): g (⨆ i, f i) = ⨆ i, g (f i) holds when the codomain isn't linear (leanprover-community#36672)

This was found while reviewing leanprover-community#35822.

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Author: Komyyy

Mathlib/Data/Fintype/Order.lean

@@ -283,7 +283,7 @@ end CCL
 
 section CCLO
 
-variable {α β ι : Type*} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLinearOrder β]
+variable {α β ι : Type*} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β]
   [Finite ι] [Nonempty ι]
 
 lemma map_iSup_of_monotoneOn {s : Set α} {f : ι → α} {g : α → β} (hg : MonotoneOn g s)