fix: allow various Vector append lemmas to take vectors of different sizes (#13693)

This PR generalizes a number of `Vector` lemmas about `++` so that the
two appended vectors no longer need to share the same size index:
`sum_append`, `prod_append`, their `_nat` / `_int` variants,
`flatMap_append`, `unattach_append`, `eraseIdx_append_of_lt_size`, and
`eraseIdx_append_of_length_le`.

Reported on Zulip:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Vector.2Esum_append.20should.20allow.20vectors.20of.20different.20size

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

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

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

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

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 =]

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