diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index ce98f61e8c..579b1b408d 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -580,7 +580,8 @@ and simplifies these to the function directly taking the value.
   simp [Array.unattach_reverse]
 
 
-@[simp] theorem unattach_append {p : α → Prop} {xs ys : Vector { x // p x } n} :
+@[simp] theorem unattach_append {p : α → Prop}
+    {xs : Vector { x // p x } n} {ys : Vector { x // p x } m} :
     (xs ++ ys).unattach = xs.unattach ++ ys.unattach := by
   rcases xs
   rcases ys
diff --git a/src/Init/Data/Vector/Erase.lean b/src/Init/Data/Vector/Erase.lean
index 0a81bb175f..846d23aae4 100644
--- a/src/Init/Data/Vector/Erase.lean
+++ b/src/Init/Data/Vector/Erase.lean
@@ -64,13 +64,15 @@ theorem mem_of_mem_eraseIdx {xs : Vector α n} {i : Nat} {h} {a : α} (h : a ∈
 
 grind_pattern mem_of_mem_eraseIdx => a ∈ xs.eraseIdx i
 
-theorem eraseIdx_append_of_lt_size {xs : Vector α n} {k : Nat} (hk : k < n) (xs' : Vector α n) (h) :
+theorem eraseIdx_append_of_lt_size {xs : Vector α n} {k : Nat} (hk : k < n)
+    (xs' : Vector α m) (h) :
     eraseIdx (xs ++ xs') k = (eraseIdx xs k ++ xs').cast (by omega) := by
   rcases xs with ⟨xs⟩
   rcases xs' with ⟨xs'⟩
   simp [Array.eraseIdx_append_of_lt_size, *]
 
-theorem eraseIdx_append_of_length_le {xs : Vector α n} {k : Nat} (hk : n ≤ k) (xs' : Vector α n) (h) :
+theorem eraseIdx_append_of_length_le {xs : Vector α n} {k : Nat} (hk : n ≤ k)
+    (xs' : Vector α m) (h) :
     eraseIdx (xs ++ xs') k = (xs ++ eraseIdx xs' (k - n)).cast (by omega) := by
   rcases xs with ⟨xs⟩
   rcases xs' with ⟨xs'⟩
diff --git a/src/Init/Data/Vector/Int.lean b/src/Init/Data/Vector/Int.lean
index d711f332e2..1588dec020 100644
--- a/src/Init/Data/Vector/Int.lean
+++ b/src/Init/Data/Vector/Int.lean
@@ -21,7 +21,8 @@ namespace Vector
 @[simp] theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
   simp [← sum_toArray, Array.sum_replicate_int]
 
-theorem sum_append_int {as₁ as₂ : Vector Int n} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+theorem sum_append_int {as₁ : Vector Int n} {as₂ : Vector Int m} :
+    (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
   simp [← sum_toArray]
 
 theorem sum_reverse_int (xs : Vector Int n) : xs.reverse.sum = xs.sum := by
@@ -33,7 +34,8 @@ theorem sum_eq_foldl_int {xs : Vector Int n} : xs.sum = xs.foldl (b := 0) (· +
 @[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
   simp [← prod_toArray, Array.prod_replicate_int]
 
-theorem prod_append_int {as₁ as₂ : Vector Int n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+theorem prod_append_int {as₁ : Vector Int n} {as₂ : Vector Int m} :
+    (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
   simp [← prod_toArray]
 
 theorem prod_reverse_int (xs : Vector Int n) : xs.reverse.prod = xs.prod := by
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index ef332ffea5..be1220ae22 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -2090,7 +2090,7 @@ theorem flatMap_singleton {f : α → Vector β m} {x : α} : #v[x].flatMap f =
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem flatMap_append {xs ys : Vector α n} {f : α → Vector β m} :
+@[simp] theorem flatMap_append {xs : Vector α n} {ys : Vector α k} {f : α → Vector β m} :
     (xs ++ ys).flatMap f = (xs.flatMap f ++ ys.flatMap f).cast (by simp [Nat.add_mul]) := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
@@ -3118,7 +3118,7 @@ theorem sum_eq_foldr [Add α] [Zero α] {xs : Vector α n} :
 @[simp, grind =]
 theorem sum_append [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     [Std.LeftIdentity (α := α) (· + ·) 0] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
-    {as₁ as₂ : Vector α n} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+    {as₁ : Vector α n} {as₂ : Vector α m} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
   simp [← sum_toList, List.sum_append]
 
 @[simp, grind =]
@@ -3154,7 +3154,7 @@ theorem prod_eq_foldr [Mul α] [One α] {xs : Vector α n} :
 @[simp, grind =]
 theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
     [Std.LeftIdentity (α := α) (· * ·) 1] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
-    {as₁ as₂ : Vector α n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+    {as₁ : Vector α n} {as₂ : Vector α m} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
   simp [← prod_toList, List.prod_append]
 
 @[simp, grind =]
diff --git a/src/Init/Data/Vector/Nat.lean b/src/Init/Data/Vector/Nat.lean
index a30a53bc6a..64dc876db6 100644
--- a/src/Init/Data/Vector/Nat.lean
+++ b/src/Init/Data/Vector/Nat.lean
@@ -28,7 +28,8 @@ protected theorem sum_eq_zero_iff_forall_eq_nat {xs : Vector Nat n} :
 @[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
   simp [← sum_toArray, Array.sum_replicate_nat]
 
-theorem sum_append_nat {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+theorem sum_append_nat {as₁ : Vector Nat n} {as₂ : Vector Nat m} :
+    (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
   simp [← sum_toArray]
 
 theorem sum_reverse_nat (xs : Vector Nat n) : xs.reverse.sum = xs.sum := by
@@ -47,7 +48,8 @@ protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Vector Nat n} :
 @[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
   simp [← prod_toArray, Array.prod_replicate_nat]
 
-theorem prod_append_nat {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+theorem prod_append_nat {as₁ : Vector Nat n} {as₂ : Vector Nat m} :
+    (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
   simp [← prod_toArray]
 
 theorem prod_reverse_nat (xs : Vector Nat n) : xs.reverse.prod = xs.prod := by