chore(Int/LeastGreatest): use classical logic (#11163)

Mathlib/Data/Int/LeastGreatest.lean

@@ -60,9 +60,9 @@ def leastOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ,
     `[DecidablePred P]`. See `Int.leastOfBdd` for a constructive counterpart. -/
 theorem exists_least_of_bdd
     {P : ℤ → Prop}
-    [DecidablePred P]
     (Hbdd : ∃ b : ℤ , ∀ z : ℤ , P z → b ≤ z)
     (Hinh : ∃ z : ℤ , P z) : ∃ lb : ℤ , P lb ∧ ∀ z : ℤ , P z → lb ≤ z := by
+  classical
   let ⟨b , Hb⟩ := Hbdd
   let ⟨lb , H⟩ := leastOfBdd b Hb Hinh
   exact ⟨lb , H⟩
@@ -95,12 +95,12 @@ def greatestOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : 
     `[DecidablePred P]`. See `Int.greatestOfBdd` for a constructive counterpart. -/
 theorem exists_greatest_of_bdd
     {P : ℤ → Prop}
-    [DecidablePred P]
     (Hbdd : ∃ b : ℤ , ∀ z : ℤ , P z → z ≤ b)
     (Hinh : ∃ z : ℤ , P z) : ∃ ub : ℤ , P ub ∧ ∀ z : ℤ , P z → z ≤ ub := by
-  let ⟨ b , Hb ⟩ := Hbdd
-  let ⟨ lb , H ⟩ := greatestOfBdd b Hb Hinh
-  exact ⟨ lb , H ⟩
+  classical
+  let ⟨b, Hb⟩ := Hbdd
+  let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
+  exact ⟨lb, H⟩
 #align int.exists_greatest_of_bdd Int.exists_greatest_of_bdd
 
 theorem coe_greatestOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ}

Mathlib/NumberTheory/ClassNumber/Finite.lean

@@ -128,14 +128,12 @@ theorem norm_lt {T : Type*} [LinearOrderedRing T] (a : S) {y : T}
 
 
 /-- A nonzero ideal has an element of minimal norm. -/
--- Porting note: port of Int.exists_least_of_bdd requires DecidablePred, so we use classical
 theorem exists_min (I : (Ideal S)⁰) :
     ∃ b ∈ (I : Ideal S),
       b ≠ 0 ∧ ∀ c ∈ (I : Ideal S), abv (Algebra.norm R c) < abv (Algebra.norm R b) → c =
       (0 : S) := by
-  classical
   obtain ⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩, min⟩ := @Int.exists_least_of_bdd
-      (fun a => ∃ b ∈ (I : Ideal S), b ≠ (0 : S) ∧ abv (Algebra.norm R b) = a) _
+      (fun a => ∃ b ∈ (I : Ideal S), b ≠ (0 : S) ∧ abv (Algebra.norm R b) = a)
     (by
       use 0
       rintro _ ⟨b, _, _, rfl⟩