Add Lattice ℤ instance for computability (#9946)

The file `Data.Int.ConditionallyCompleteOrder` defines a noncomputable instance of `ConditionallyCompleteLinearOrder` on `ℤ`.

This noncomputable instance is picked up by the typeclass search when looking for a `Lattice` instance on `ℤ`, making, for instance, `abs` noncomputable on `ℤ`.

This PR restores the computability of `Lattice ℤ`.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/No.20more.20.60Abs.60.3F/near/417546479)

Mathlib/Data/Int/ConditionallyCompleteOrder.lean

@@ -17,9 +17,9 @@ The integers form a conditionally complete linear order.
 
 open Int
 
-open Classical
 
 noncomputable section
+open Classical
 
 instance : ConditionallyCompleteLinearOrder ℤ :=
   { Int.linearOrderedCommRing,
@@ -106,3 +106,9 @@ theorem csInf_mem {s : Set ℤ} (h1 : s.Nonempty) (h2 : BddBelow s) : sInf s ∈
 #align int.cInf_mem Int.csInf_mem
 
 end Int
+
+end
+
+--  this example tests that the `Lattice ℤ` instance is computable;
+-- i.e., that is is not found via the noncomputable instance in this file.
+example : Lattice ℤ := inferInstance

Mathlib/Order/Lattice.lean

@@ -934,6 +934,7 @@ instance (priority := 100) {α : Type u} [LinearOrder α] :
     | Or.inr h => inf_le_of_right_le <| sup_le_sup_left (le_inf h (le_refl c)) _
 
 instance : DistribLattice ℕ := inferInstance
+instance : Lattice ℤ := inferInstance
 
 /-! ### Dual order -/