doc(Order/ConditionallyCompleteLattice/Defs): Lean3 structure notation (leanprover-community#36671)

* Some docstrings still use Lean3 structure notation.
* Some mistakenly use `(sup|inf)` instead of `s(Sup|Inf)`
* `conditionallyCompleteLatticeOfs(Sup|Inf)` provides both `sup` & `inf`

These were found while reviewing leanprover-community#35774.

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

Author: Komyyy

Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

@@ -99,14 +99,13 @@ constructor provides poor definitional equalities.  If other fields are known ex
 should be provided; for example, if `inf` is known explicitly, construct the
 `ConditionallyCompleteLattice` instance as
 ```
-@[implicit_reducible]
-instance : ConditionallyCompleteLattice my_T :=
-  { inf := better_inf,
-    le_inf := ...,
-    inf_le_right := ...,
-    inf_le_left := ...
-    -- don't care to fix sup, sInf
-    ..conditionallyCompleteLatticeOfsSup my_T _ }
+instance : ConditionallyCompleteLattice my_T where
+  inf := better_inf
+  le_inf := ...
+  inf_le_right := ...
+  inf_le_left := ...
+  -- don't care to fix sup, sInf
+  __ := conditionallyCompleteLatticeOfsSup my_T ...
 ```
 -/
 @[implicit_reducible]
@@ -141,20 +140,19 @@ def conditionallyCompleteLatticeOfsSup (α : Type*) [H1 : PartialOrder α] [H2 :
   isLUB_csSup _ hn hb := isLUB_sSup _ hb hn
   isGLB_csInf _ hn hb := isLUB_lowerBounds.mp (isLUB_sSup _ hn.bddAbove_lowerBounds hb)
 
-/-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `inf` function
+/-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `sInf` function
 that returns the greatest lower bound of a nonempty set which is bounded below. Usually this
 constructor provides poor definitional equalities.  If other fields are known explicitly, they
 should be provided; for example, if `inf` is known explicitly, construct the
 `ConditionallyCompleteLattice` instance as
 ```
-@[implicit_reducible]
 instance : ConditionallyCompleteLattice my_T :=
-  { inf := better_inf,
-    le_inf := ...,
-    inf_le_right := ...,
-    inf_le_left := ...
-    -- don't care to fix sup, sSup
-    ..conditionallyCompleteLatticeOfsInf my_T _ }
+  inf := better_inf
+  le_inf := ...
+  inf_le_right := ...
+  inf_le_left := ...
+  -- don't care to fix sup, sSup
+  __ := conditionallyCompleteLatticeOfsInf my_T ...
 ```
 -/
 @[implicit_reducible]
@@ -192,7 +190,7 @@ def conditionallyCompleteLatticeOfsInf (α : Type*) [H1 : PartialOrder α] [H2 :
 
 /-- A version of `conditionallyCompleteLatticeOfsSup` when we already know that `α` is a lattice.
 
-This should only be used when it is both hard and unnecessary to provide `inf` explicitly. -/
+This should only be used when it is both hard and unnecessary to provide `sInf` explicitly. -/
 @[implicit_reducible]
 def conditionallyCompleteLatticeOfLatticeOfsSup (α : Type*) [H1 : Lattice α] [SupSet α]
     (isLUB_sSup : ∀ s : Set α, BddAbove s → s.Nonempty → IsLUB s (sSup s)) :
@@ -205,7 +203,7 @@ def conditionallyCompleteLatticeOfLatticeOfsSup (α : Type*) [H1 : Lattice α] [
 
 /-- A version of `conditionallyCompleteLatticeOfsInf` when we already know that `α` is a lattice.
 
-This should only be used when it is both hard and unnecessary to provide `sup` explicitly. -/
+This should only be used when it is both hard and unnecessary to provide `sSup` explicitly. -/
 @[implicit_reducible]
 def conditionallyCompleteLatticeOfLatticeOfsInf (α : Type*) [H1 : Lattice α] [InfSet α]
     (isGLB_sInf : ∀ s : Set α, BddBelow s → s.Nonempty → IsGLB s (sInf s)) :