a few more

Mathlib/Data/ENNReal/Basic.lean

@@ -152,7 +152,7 @@ noncomputable instance : LinearOrderedCommMonoidWithZero ℝ≥0∞ :=
     mul_le_mul_left := fun _ _ => mul_le_mul_left'
     zero_le_one := zero_le 1 }
 
-noncomputable instance : Unique (AddUnits ℝ≥0∞) where
+instance : Unique (AddUnits ℝ≥0∞) where
   default := 0
   uniq a := AddUnits.ext <| le_zero_iff.1 <| by rw [← a.add_neg]; exact le_self_add
 
@@ -192,7 +192,7 @@ protected def toNNReal : ℝ≥0∞ → ℝ≥0 := WithTop.untop' 0
 protected def toReal (a : ℝ≥0∞) : Real := a.toNNReal
 
 /-- `ofReal x` returns `x` if it is nonnegative, `0` otherwise. -/
-protected noncomputable def ofReal (r : Real) : ℝ≥0∞ := r.toNNReal
+protected def ofReal (r : Real) : ℝ≥0∞ := r.toNNReal
 
 @[simp, norm_cast] lemma toNNReal_coe (r : ℝ≥0) : (r : ℝ≥0∞).toNNReal = r := rfl
 

Mathlib/Data/NNReal/Defs.lean

@@ -105,7 +105,7 @@ protected theorem «exists» {p : ℝ≥0 → Prop} :
   Subtype.exists
 
 /-- Reinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`. -/
-noncomputable def _root_.Real.toNNReal (r : ℝ) : ℝ≥0 :=
+def _root_.Real.toNNReal (r : ℝ) : ℝ≥0 :=
   ⟨max r 0, le_max_right _ _⟩
 
 theorem _root_.Real.coe_toNNReal (r : ℝ) (hr : 0 ≤ r) : (Real.toNNReal r : ℝ) = r :=
@@ -127,7 +127,7 @@ example : One ℝ≥0 := by infer_instance
 
 example : Add ℝ≥0 := by infer_instance
 
-noncomputable example : Sub ℝ≥0 := by infer_instance
+example : Sub ℝ≥0 := by infer_instance
 
 example : Mul ℝ≥0 := by infer_instance
 
@@ -325,7 +325,7 @@ theorem _root_.Real.toNNReal_ofNat (n : ℕ) [n.AtLeastTwo] :
   toNNReal_coe_nat n
 
 /-- `Real.toNNReal` and `NNReal.toReal : ℝ≥0 → ℝ` form a Galois insertion. -/
-noncomputable def gi : GaloisInsertion Real.toNNReal (↑) :=
+def gi : GaloisInsertion Real.toNNReal (↑) :=
   GaloisInsertion.monotoneIntro NNReal.coe_mono Real.toNNReal_mono Real.le_coe_toNNReal fun _ =>
     Real.toNNReal_coe