chore: cleanups uncovered by Shake (#10572)

* Wrap proof subterms in `by exact` so dependencies can be demoted to
private `import`s
* Remove trivial instance re-definitions that may cause name collisions
on import changes
* Remove unused `open`s that may fail on import removals

Author: Kha

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),

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,15 +154,15 @@ 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`.
 
 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.

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'⟩,

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

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

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
 

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
 

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

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

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