rerevert

This reverts commit e551a366a0.

src/Init/Data/Array/Lemmas.lean

@@ -57,7 +57,9 @@ open Array
 
 /-! ### Lemmas about `List.toArray`. -/
 
-@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
+@[simp] theorem toArray_size (as : List α) : as.toArray.size = as.length := by simp [size]
+
+@[simp] theorem toArrayAux_size {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
@@ -65,7 +67,6 @@ 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/Prelude.lean

@@ -754,10 +754,10 @@ infer the proof of `Nonempty α`.
 noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α :=
   Classical.choice inferInstance
 
-instance {α : Sort u} {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
+instance (α : Sort u) {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
-instance Pi.instNonempty {α : Sort u} {β : α → Sort v} [(a : α) → Nonempty (β a)] :
+instance Pi.instNonempty (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] :
     Nonempty ((a : α) → β a) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
@@ -767,7 +767,7 @@ instance : Inhabited (Sort u) where
 instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
   default := fun _ => default
 
-instance Pi.instInhabited {α : Sort u} {β : α → Sort v} [(a : α) → Inhabited (β a)] :
+instance Pi.instInhabited (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] :
     Inhabited ((a : α) → β a) where
   default := fun _ => default
 
@@ -2570,9 +2570,7 @@ structure Array (α : Type u) where
   /--
   Converts a `List α` into an `Array α`.
 
-  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
+  At runtime, this constructor is implemented by `List.toArray` and is O(n) in the length of the
   list.
   -/
   mk ::