chore: List/Array/Vector implicitness changes

src/Init/Data/Array/Range.lean

@@ -88,7 +88,7 @@ theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ #[s + n]
     fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
     fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩
 
-theorem map_sub_range' {a s n : Nat} (h : a ≤ s) :
+theorem map_sub_range' {a s : Nat} (h : a ≤ s) (n : Nat) :
     map (· - a) (range' s n step) = range' (s - a) n step := by
   conv => lhs; rw [← Nat.add_sub_cancel' h]
   rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id]

src/Init/Data/List/Count.lean

@@ -209,7 +209,7 @@ theorem count_eq_countP' {a : α} : count a = countP (· == a) := by
   funext l
   apply count_eq_countP
 
-theorem count_tail : ∀ {l : List α} {a : α} (h : l ≠ []),
+theorem count_tail : ∀ {l : List α} (h : l ≠ []) (a : α),
       l.tail.count a = l.count a - if l.head h == a then 1 else 0
   | _ :: _, a, _ => by simp [count_cons]
 

src/Init/Data/List/Nat/InsertIdx.lean

@@ -48,14 +48,14 @@ theorem length_insertIdx : ∀ {i} {as : List α}, (as.insertIdx i a).length = i
     simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_le_add_iff_right]
     split <;> rfl
 
-theorem length_insertIdx_of_le_length (h : i ≤ length as) : (as.insertIdx i a).length = as.length + 1 := by
+theorem length_insertIdx_of_le_length (h : i ≤ length as) (a : α) : (as.insertIdx i a).length = as.length + 1 := by
   simp [length_insertIdx, h]
 
-theorem length_insertIdx_of_length_lt (h : length as < i) : (as.insertIdx i a).length = as.length := by
+theorem length_insertIdx_of_length_lt (h : length as < i) (a : α) : (as.insertIdx i a).length = as.length := by
   simp [length_insertIdx, h]
 
 @[simp]
-theorem eraseIdx_insertIdx {i : Nat} {l : List α} : (l.insertIdx i a).eraseIdx i = l := by
+theorem eraseIdx_insertIdx {i : Nat} {l : List α} (a : α) : (l.insertIdx i a).eraseIdx i = l := by
   rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
   exact modifyTailIdx_id _ _
 

src/Init/Data/List/Nat/Range.lean

@@ -74,7 +74,7 @@ theorem pairwise_le_range' {s n} (step := 1) :
 theorem nodup_range' {s n : Nat} (step := 1) (h : 0 < step := by simp) : Nodup (range' s n step) :=
   (pairwise_lt_range' step h).imp Nat.ne_of_lt
 
-theorem map_sub_range' {a s n : Nat} (h : a ≤ s) :
+theorem map_sub_range' {a s : Nat} (h : a ≤ s) (n : Nat) :
     map (· - a) (range' s n step) = range' (s - a) n step := by
   conv => lhs; rw [← Nat.add_sub_cancel' h]
   rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id]

src/Init/Data/Vector/Range.lean

@@ -86,7 +86,7 @@ theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ #v[s + n]
     fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
     fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩
 
-theorem map_sub_range' {a s n : Nat} (h : a ≤ s) :
+theorem map_sub_range' {a s : Nat} (h : a ≤ s) (n : Nat) :
     map (· - a) (range' s n step) = range' (s - a) n step := by
   conv => lhs; rw [← Nat.add_sub_cancel' h]
   rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id]