chore: use Array.mk instead of List.toArray

Requested [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/heq_comm/near/472516757).

src/Init/Core.lean

@@ -837,6 +837,9 @@ instance : Trans Iff Iff Iff where
 theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm
 theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm
 
+theorem HEq.comm {a : α} {b : β} : HEq a b ↔ HEq b a := Iff.intro HEq.symm HEq.symm
+theorem heq_comm {a : α} {b : β} : HEq a b ↔ HEq b a := HEq.comm
+
 @[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
 theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
 theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm

src/Init/Data/Array/Basic.lean

@@ -18,7 +18,7 @@ universe u v w
 syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
 
 macro_rules
-  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
+  | `(#[ $elems,* ]) => `(Array.mk [ $elems,* ])
 
 variable {α : Type u}
 

src/Init/Data/Array/Lemmas.lean

@@ -57,9 +57,7 @@ open Array
 
 /-! ### Lemmas about `List.toArray`. -/
 
-@[simp] theorem toArray_size (as : List α) : as.toArray.size = as.length := by simp [size]
-
-@[simp] theorem toArrayAux_size {a : List α} {b : Array α} :
+@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
@@ -67,6 +65,7 @@ open Array
 
 @[deprecated toArray_toList (since := "2024-09-09")]
 abbrev toArray_data := @toArray_toList
+
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
 

src/Init/NotationExtra.lean

@@ -154,6 +154,10 @@ end Lean
     | _          => throw ()
   | _ => throw ()
 
+@[app_unexpander Array.mk] def unexpandArrayMk : Lean.PrettyPrinter.Unexpander
+  | `($(_) [$xs,*]) => `(#[$xs,*])
+  | _               => throw ()
+
 @[app_unexpander List.toArray] def unexpandListToArray : Lean.PrettyPrinter.Unexpander
   | `($(_) [$xs,*]) => `(#[$xs,*])
   | _               => throw ()

src/Init/Prelude.lean

@@ -2570,7 +2570,9 @@ structure Array (α : Type u) where
   /--
   Converts a `List α` into an `Array α`.
 
-  At runtime, this constructor is implemented by `List.toArray` and is O(n) in the length of the
+  You can also use the synonym `List.toArray` when dot notation is convenient.
+
+  At runtime, this constructor is implemented by `List.toArrayImpl` and is O(n) in the length of the
   list.
   -/
   mk ::

src/Lean/Meta/AppBuilder.lean

@@ -502,7 +502,7 @@ def mkListLit (type : Expr) (xs : List Expr) : MetaM Expr := do
 def mkArrayLit (type : Expr) (xs : List Expr) : MetaM Expr := do
   let u ← getDecLevel type
   let listLit ← mkListLit type xs
-  return mkApp (mkApp (mkConst ``List.toArray [u]) type) listLit
+  return mkApp (mkApp (mkConst ``Array.mk [u]) type) listLit
 
 def mkNone (type : Expr) : MetaM Expr := do
   let u ← getDecLevel type

src/Lean/Meta/LitValues.lean

@@ -202,19 +202,19 @@ def getListLit? (e : Expr) : MetaM (Option (Array Expr)) := getListLitOf? e fun
 
 /--
 Check if an expression is an array literal
-(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
+(i.e. `Array.mk` applied to a nested chain of `List.cons`, ending at a `List.nil`),
 where each element is "recognised" by a given function `f : Expr → MetaM (Option α)`,
 and return the array of recognised values.
 -/
 def getArrayLitOf? (e : Expr) (f : Expr → MetaM (Option α)) : MetaM (Option (Array α)) := do
   let e ← instantiateMVars e.consumeMData
   match_expr e with
-  | List.toArray _ as => getListLitOf? as f
+  | Array.mk _ as => getListLitOf? as f
   | _ => return none
 
 /--
 Check if an expression is an array literal
-(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
+(i.e. `Array.mk` applied to a nested chain of `List.cons`, ending at a `List.nil`),
 returning the array of `Expr` values.
 -/
 def getArrayLit? (e : Expr) : MetaM (Option (Array Expr)) := getArrayLitOf? e fun s => return some s

src/Lean/Util/Recognizers.lean

@@ -97,7 +97,7 @@ partial def listLit? (e : Expr) : Option (Expr × List Expr) :=
   loop e []
 
 def arrayLit? (e : Expr) : Option (Expr × List Expr) :=
-  if e.isAppOfArity' ``List.toArray 2 then
+  if e.isAppOfArity' ``Array.mk 2 then
     listLit? e.appArg!'
   else
     none