chore(Order/FixedPoints): use where notation (leanprover-community#33952)

This also avoids constructing auxiliary `CompleteSemilatticeInf` and `CompleteSemilatticeSup` instances. These are meant exclusively to build a `CompleteLattice` from one without the other; this isn't what's happening here. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ditch.20CompleteSemilatticeSup/near/567390440).

Author: vihdzp

Mathlib/Order/FixedPoints.lean

@@ -232,47 +232,38 @@ open OrderHom
 
 variable [CompleteLattice α] (f : α →o α)
 
-instance : SemilatticeSup (fixedPoints f) :=
-  { Subtype.partialOrder _ with
-    sup := fun x y => f.nextFixed (x ⊔ y) (f.le_map_sup_fixedPoints x y)
-    le_sup_left := fun _ _ => Subtype.coe_le_coe.1 <| le_sup_left.trans (f.le_nextFixed _)
-    le_sup_right := fun _ _ => Subtype.coe_le_coe.1 <| le_sup_right.trans (f.le_nextFixed _)
-    sup_le := fun _ _ _ hxz hyz => f.nextFixed_le _ <| sup_le hxz hyz }
-
-instance : SemilatticeInf (fixedPoints f) :=
-  { OrderDual.instSemilatticeInf (fixedPoints f.dual) with
-    inf := fun x y => f.prevFixed (x ⊓ y) (f.map_inf_fixedPoints_le x y) }
-
-instance : CompleteSemilatticeSup (fixedPoints f) :=
-  { Subtype.partialOrder _ with
-    sSup := fun s =>
-      f.nextFixed (sSup (Subtype.val '' s))
-        (f.le_map_sSup_subset_fixedPoints (Subtype.val '' s)
-          fun _ ⟨x, hx⟩ => hx.2 ▸ x.2)
-    le_sSup := fun _ _ hx =>
-      Subtype.coe_le_coe.1 <| le_trans (le_sSup <| Set.mem_image_of_mem _ hx) (f.le_nextFixed _)
-    sSup_le := fun _ _ hx => f.nextFixed_le _ <| sSup_le <| Set.forall_mem_image.2 hx }
-
-instance : CompleteSemilatticeInf (fixedPoints f) :=
-  { Subtype.partialOrder _ with
-    sInf := fun s =>
-      f.prevFixed (sInf (Subtype.val '' s))
-        (f.map_sInf_subset_fixedPoints_le (Subtype.val '' s) fun _ ⟨x, hx⟩ => hx.2 ▸ x.2)
-    le_sInf := fun _ _ hx => f.le_prevFixed _ <| le_sInf <| Set.forall_mem_image.2 hx
-    sInf_le := fun _ _ hx =>
-      Subtype.coe_le_coe.1 <| le_trans (f.prevFixed_le _) (sInf_le <| Set.mem_image_of_mem _ hx) }
-
-/-- **Knaster-Tarski Theorem**: The fixed points of `f` form a complete lattice. -/
-instance completeLattice : CompleteLattice (fixedPoints f) where
-  __ := inferInstanceAs (SemilatticeInf (fixedPoints f))
-  __ := inferInstanceAs (SemilatticeSup (fixedPoints f))
-  __ := inferInstanceAs (CompleteSemilatticeInf (fixedPoints f))
-  __ := inferInstanceAs (CompleteSemilatticeSup (fixedPoints f))
+instance : BoundedOrder (fixedPoints f) where
   top := ⟨f.gfp, f.isFixedPt_gfp⟩
   bot := ⟨f.lfp, f.isFixedPt_lfp⟩
   le_top x := f.le_gfp x.2.ge
   bot_le x := f.lfp_le x.2.le
 
+instance : SemilatticeSup (fixedPoints f) where
+  sup x y := f.nextFixed (x ⊔ y) (f.le_map_sup_fixedPoints x y)
+  le_sup_left _ _ := Subtype.coe_le_coe.1 <| le_sup_left.trans (f.le_nextFixed _)
+  le_sup_right _ _ := Subtype.coe_le_coe.1 <| le_sup_right.trans (f.le_nextFixed _)
+  sup_le _ _ _ hxz hyz := f.nextFixed_le _ <| sup_le hxz hyz
+
+instance : SemilatticeInf (fixedPoints f) where
+  inf x y := f.prevFixed (x ⊓ y) (f.map_inf_fixedPoints_le x y)
+  __ := OrderDual.instSemilatticeInf (fixedPoints f.dual)
+
+/-- **Knaster-Tarski Theorem**: The fixed points of `f` form a complete lattice. -/
+instance completeLattice : CompleteLattice (fixedPoints f) where
+  sSup s :=
+    f.nextFixed (sSup (Subtype.val '' s))
+      (f.le_map_sSup_subset_fixedPoints (Subtype.val '' s)
+        fun _ ⟨x, hx⟩ => hx.2 ▸ x.2)
+  le_sSup _ _ hx :=
+    Subtype.coe_le_coe.1 <| le_trans (le_sSup <| Set.mem_image_of_mem _ hx) (f.le_nextFixed _)
+  sSup_le _ _ hx := f.nextFixed_le _ <| sSup_le <| Set.forall_mem_image.2 hx
+  sInf s :=
+    f.prevFixed (sInf (Subtype.val '' s))
+      (f.map_sInf_subset_fixedPoints_le (Subtype.val '' s) fun _ ⟨x, hx⟩ => hx.2 ▸ x.2)
+  le_sInf _ _ hx := f.le_prevFixed _ <| le_sInf <| Set.forall_mem_image.2 hx
+  sInf_le _ _ hx :=
+    Subtype.coe_le_coe.1 <| le_trans (f.prevFixed_le _) (sInf_le <| Set.mem_image_of_mem _ hx)
+
 open OmegaCompletePartialOrder fixedPoints
 
 /-- **Kleene's fixed point Theorem**: The least fixed point in a complete lattice is