diff --git a/src/Init/Data/BitVec/Decidable.lean b/src/Init/Data/BitVec/Decidable.lean
index f956d8b1f3..5bf7ebd621 100644
--- a/src/Init/Data/BitVec/Decidable.lean
+++ b/src/Init/Data/BitVec/Decidable.lean
@@ -49,11 +49,11 @@ instance instDecidableForallBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePre
 
 instance instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] :
     Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+  decidable_of_iff (¬ ∀ v, ¬ P v) (by exact Classical.not_forall_not)
 
 instance instDecidableExistsBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
     [Decidable (∀ (x : Bool) (v : BitVec n), ¬ P (v.cons x))] : Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+  decidable_of_iff (¬ ∀ v, ¬ P v) (by exact Classical.not_forall_not)
 
 /--
 For small numerals this isn't necessary (as typeclass search can use the above two instances),
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 743c0ab0a4..ba12a6027b 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -140,7 +140,7 @@ Modulus of bounded numbers, usually invoked via the `%` operator.
 The resulting value is that computed by the `%` operator on `Nat`.
 -/
 protected def mod : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b,  Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Division of bounded numbers, usually invoked via the `/` operator.
@@ -154,7 +154,7 @@ Examples:
  * `(5 : Fin 10) / (7 : Fin 10) = (0 : Fin 10)`
 -/
 protected def div : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
 
 /--
 Modulus of bounded numbers with respect to a `Nat`.
@@ -162,7 +162,7 @@ Modulus of bounded numbers with respect to a `Nat`.
 The resulting value is that computed by the `%` operator on `Nat`.
 -/
 def modn : Fin n → Nat → Fin n
-  | ⟨a, h⟩, m => ⟨a % m, Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, m => ⟨a % m, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Bitwise and.
diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 56e01f61be..639f01deda 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -122,8 +122,8 @@ theorem eq_one_of_mul_eq_one_right {a b : Int} (H : 0 ≤ a) (H' : a * b = 1) :
 theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b = 1 :=
   eq_one_of_mul_eq_one_right (b := a) H <| by rw [Int.mul_comm, H']
 
-instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun _ _ =>
-  decidable_of_decidable_of_iff (dvd_iff_emod_eq_zero ..).symm
+instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun a b =>
+  decidable_of_decidable_of_iff (p := b % a = 0) (by exact (dvd_iff_emod_eq_zero ..).symm)
 
 protected theorem mul_dvd_mul_iff_left {a b c : Int} (h : a ≠ 0) : (a * b) ∣ (a * c) ↔ b ∣ c :=
   ⟨by rintro ⟨d, h'⟩; exact ⟨d, by rw [Int.mul_assoc] at h'; exact (mul_eq_mul_left_iff h).mp h'⟩,
diff --git a/src/Init/Data/Range/Polymorphic/BitVec.lean b/src/Init/Data/Range/Polymorphic/BitVec.lean
index 34e42bb0d9..ae13cac9f9 100644
--- a/src/Init/Data/Range/Polymorphic/BitVec.lean
+++ b/src/Init/Data/Range/Polymorphic/BitVec.lean
@@ -49,7 +49,6 @@ instance : LawfulUpwardEnumerableLE (BitVec n) where
     · rintro ⟨n, hn, rfl⟩
       simp [BitVec.ofNatLT]
 
-instance : LawfulOrderLT (BitVec n) := inferInstance
 instance : LawfulUpwardEnumerableLT (BitVec n) := inferInstance
 instance : LawfulUpwardEnumerableLT (BitVec n) := inferInstance
 instance : LawfulUpwardEnumerableLowerBound .closed (BitVec n) := inferInstance
diff --git a/src/Init/Data/Range/Polymorphic/UInt.lean b/src/Init/Data/Range/Polymorphic/UInt.lean
index 23b3c7b8b9..9eecc8259f 100644
--- a/src/Init/Data/Range/Polymorphic/UInt.lean
+++ b/src/Init/Data/Range/Polymorphic/UInt.lean
@@ -57,7 +57,6 @@ instance : LawfulUpwardEnumerableLE UInt8 where
     simpa [upwardEnumerableLE_ofBitVec, UInt8.le_iff_toBitVec_le] using
       LawfulUpwardEnumerableLE.le_iff _ _
 
-instance : LawfulOrderLT UInt8 := inferInstance
 instance : LawfulUpwardEnumerableLT UInt8 := inferInstance
 instance : LawfulUpwardEnumerableLT UInt8 := inferInstance
 instance : LawfulUpwardEnumerableLowerBound .closed UInt8 := inferInstance
@@ -130,7 +129,6 @@ instance : LawfulUpwardEnumerableLE UInt16 where
     simpa [upwardEnumerableLE_ofBitVec, UInt16.le_iff_toBitVec_le] using
       LawfulUpwardEnumerableLE.le_iff _ _
 
-instance : LawfulOrderLT UInt16 := inferInstance
 instance : LawfulUpwardEnumerableLT UInt16 := inferInstance
 instance : LawfulUpwardEnumerableLT UInt16 := inferInstance
 instance : LawfulUpwardEnumerableLowerBound .closed UInt16 := inferInstance
@@ -203,7 +201,6 @@ instance : LawfulUpwardEnumerableLE UInt32 where
     simpa [upwardEnumerableLE_ofBitVec, UInt32.le_iff_toBitVec_le] using
       LawfulUpwardEnumerableLE.le_iff _ _
 
-instance : LawfulOrderLT UInt32 := inferInstance
 instance : LawfulUpwardEnumerableLT UInt32 := inferInstance
 instance : LawfulUpwardEnumerableLT UInt32 := inferInstance
 instance : LawfulUpwardEnumerableLowerBound .closed UInt32 := inferInstance
@@ -276,7 +273,6 @@ instance : LawfulUpwardEnumerableLE UInt64 where
     simpa [upwardEnumerableLE_ofBitVec, UInt64.le_iff_toBitVec_le] using
       LawfulUpwardEnumerableLE.le_iff _ _
 
-instance : LawfulOrderLT UInt64 := inferInstance
 instance : LawfulUpwardEnumerableLT UInt64 := inferInstance
 instance : LawfulUpwardEnumerableLT UInt64 := inferInstance
 instance : LawfulUpwardEnumerableLowerBound .closed UInt64 := inferInstance
@@ -349,7 +345,6 @@ instance : LawfulUpwardEnumerableLE USize where
     simpa [upwardEnumerableLE_ofBitVec, USize.le_iff_toBitVec_le] using
       LawfulUpwardEnumerableLE.le_iff _ _
 
-instance : LawfulOrderLT USize := inferInstance
 instance : LawfulUpwardEnumerableLT USize := inferInstance
 instance : LawfulUpwardEnumerableLT USize := inferInstance
 instance : LawfulUpwardEnumerableLowerBound .closed USize := inferInstance
diff --git a/src/Init/Data/Rat/Basic.lean b/src/Init/Data/Rat/Basic.lean
index c2e8d20a67..a01b881a04 100644
--- a/src/Init/Data/Rat/Basic.lean
+++ b/src/Init/Data/Rat/Basic.lean
@@ -181,12 +181,12 @@ because you don't want to unfold it. Use `Rat.inv_def` instead.)
 @[irreducible] protected def inv (a : Rat) : Rat :=
   if h : a.num < 0 then
     { num := -a.den, den := a.num.natAbs
-      den_nz := Nat.ne_of_gt (Int.natAbs_pos.2 (Int.ne_of_lt h))
-      reduced := Int.natAbs_neg a.den ▸ a.reduced.symm }
+      den_nz := by exact Nat.ne_of_gt (Int.natAbs_pos.2 (Int.ne_of_lt h))
+      reduced := by exact Int.natAbs_neg a.den ▸ a.reduced.symm }
   else if h : a.num > 0 then
     { num := a.den, den := a.num.natAbs
-      den_nz := Nat.ne_of_gt (Int.natAbs_pos.2 (Int.ne_of_gt h))
-      reduced := a.reduced.symm }
+      den_nz := by exact Nat.ne_of_gt (Int.natAbs_pos.2 (Int.ne_of_gt h))
+      reduced := by exact a.reduced.symm }
   else
     a
 
diff --git a/src/Init/Data/Slice.lean b/src/Init/Data/Slice.lean
index 6b66394265..a48da8ae54 100644
--- a/src/Init/Data/Slice.lean
+++ b/src/Init/Data/Slice.lean
@@ -10,6 +10,7 @@ public import Init.Data.Slice.Basic
 public import Init.Data.Slice.Notation
 public import Init.Data.Slice.Operations
 public import Init.Data.Slice.Array
+public import Init.Data.Slice.Lemmas
 
 public section
 
diff --git a/src/Std/Time/Date/PlainDate.lean b/src/Std/Time/Date/PlainDate.lean
index f50c155e8d..30fbee1024 100644
--- a/src/Std/Time/Date/PlainDate.lean
+++ b/src/Std/Time/Date/PlainDate.lean
@@ -15,7 +15,6 @@ public section
 
 namespace Std
 namespace Time
-open Std.Internal
 open Std.Time
 open Internal
 open Lean
diff --git a/src/Std/Time/Date/Unit/Month.lean b/src/Std/Time/Date/Unit/Month.lean
index 6426879ad3..a8d184508e 100644
--- a/src/Std/Time/Date/Unit/Month.lean
+++ b/src/Std/Time/Date/Unit/Month.lean
@@ -13,7 +13,6 @@ public section
 namespace Std
 namespace Time
 namespace Month
-open Std.Internal
 open Internal
 
 set_option linter.all true
diff --git a/src/Std/Time/Date/Unit/Week.lean b/src/Std/Time/Date/Unit/Week.lean
index 93b79978b9..8d903074e5 100644
--- a/src/Std/Time/Date/Unit/Week.lean
+++ b/src/Std/Time/Date/Unit/Week.lean
@@ -13,7 +13,6 @@ public section
 namespace Std
 namespace Time
 namespace Week
-open Std.Internal
 open Internal
 
 set_option linter.all true
diff --git a/src/Std/Time/Date/Unit/Weekday.lean b/src/Std/Time/Date/Unit/Weekday.lean
index 88102160b6..5afa5a4fec 100644
--- a/src/Std/Time/Date/Unit/Weekday.lean
+++ b/src/Std/Time/Date/Unit/Weekday.lean
@@ -12,7 +12,6 @@ public section
 
 namespace Std
 namespace Time
-open Std.Internal
 open Internal
 
 set_option linter.all true
diff --git a/src/Std/Time/Date/Unit/Year.lean b/src/Std/Time/Date/Unit/Year.lean
index 1ca24bd6ea..229c32ed92 100644
--- a/src/Std/Time/Date/Unit/Year.lean
+++ b/src/Std/Time/Date/Unit/Year.lean
@@ -15,7 +15,6 @@ public section
 namespace Std
 namespace Time
 namespace Year
-open Std.Internal
 open Internal
 
 set_option linter.all true
diff --git a/src/Std/Time/Internal/UnitVal.lean b/src/Std/Time/Internal/UnitVal.lean
index 6ef5eb39ef..a2cb3f59c4 100644
--- a/src/Std/Time/Internal/UnitVal.lean
+++ b/src/Std/Time/Internal/UnitVal.lean
@@ -14,7 +14,6 @@ public import Init.Data.Rat.Basic
 namespace Std
 namespace Time
 namespace Internal
-open Std.Internal
 open Lean
 
 set_option linter.all true
diff --git a/src/Std/Time/Time/Unit/Hour.lean b/src/Std/Time/Time/Unit/Hour.lean
index 926495ef31..5eb59d2a6f 100644
--- a/src/Std/Time/Time/Unit/Hour.lean
+++ b/src/Std/Time/Time/Unit/Hour.lean
@@ -15,7 +15,6 @@ public section
 namespace Std
 namespace Time
 namespace Hour
-open Std.Internal
 open Internal
 
 set_option linter.all true
diff --git a/src/Std/Time/Time/Unit/Millisecond.lean b/src/Std/Time/Time/Unit/Millisecond.lean
index 6d8e709402..cc104237ff 100644
--- a/src/Std/Time/Time/Unit/Millisecond.lean
+++ b/src/Std/Time/Time/Unit/Millisecond.lean
@@ -14,7 +14,6 @@ public section
 namespace Std
 namespace Time
 namespace Millisecond
-open Std.Internal
 open Internal
 
 set_option linter.all true
diff --git a/src/Std/Time/Time/Unit/Minute.lean b/src/Std/Time/Time/Unit/Minute.lean
index 81bcf73f20..734f327ffd 100644
--- a/src/Std/Time/Time/Unit/Minute.lean
+++ b/src/Std/Time/Time/Unit/Minute.lean
@@ -14,7 +14,6 @@ public section
 namespace Std
 namespace Time
 namespace Minute
-open Std.Internal
 open Internal
 
 set_option linter.all true
diff --git a/src/Std/Time/Time/Unit/Nanosecond.lean b/src/Std/Time/Time/Unit/Nanosecond.lean
index ec7676983d..626e760e77 100644
--- a/src/Std/Time/Time/Unit/Nanosecond.lean
+++ b/src/Std/Time/Time/Unit/Nanosecond.lean
@@ -13,7 +13,6 @@ public section
 namespace Std
 namespace Time
 namespace Nanosecond
-open Std.Internal
 open Internal
 
 set_option linter.all true
diff --git a/src/Std/Time/Time/Unit/Second.lean b/src/Std/Time/Time/Unit/Second.lean
index 55c65bd58e..4e087b356b 100644
--- a/src/Std/Time/Time/Unit/Second.lean
+++ b/src/Std/Time/Time/Unit/Second.lean
@@ -13,7 +13,6 @@ public import Std.Time.Time.Unit.Nanosecond
 namespace Std
 namespace Time
 namespace Second
-open Std.Internal
 open Internal
 
 set_option linter.all true