fix tests

src/Init/Data/Array/Basic.lean

@@ -171,7 +171,7 @@ def swap (a : Array α) (i j : @& Nat) (hi : i < a.size := by get_elem_tactic) (
   let a'  := a.set i v₂
   a'.set j v₁ (Nat.lt_of_lt_of_eq hj (size_set a i v₂ _).symm)
 
-@[simp] theorem size_swap (a : Array α) (i j : Nat) (hi hj) : (a.swap i j hi hj).size = a.size := by
+@[simp] theorem size_swap (a : Array α) (i j : Nat) {hi hj} : (a.swap i j hi hj).size = a.size := by
   show ((a.set i a[j]).set j a[i]
     (Nat.lt_of_lt_of_eq hj (size_set a i a[j] _).symm)).size = a.size
   rw [size_set, size_set]

tests/lean/run/2899.lean

@@ -6,7 +6,7 @@ def myfun (x : Array α) (i : Fin x.size) : Array α :=
   let next := 2*i.1 + 1
   if h : next < x.size then
       have : x.size - next < x.size - i.1 := sorry
-      myfun (x.swap i ⟨next,h⟩) ⟨next, (x.size_swap _ _).symm ▸ h⟩
+      myfun (x.swap i next) ⟨next, (x.size_swap _ _).symm ▸ h⟩
   else
     x
 termination_by x.size - i.1

tests/lean/run/4051.lean

@@ -2,8 +2,7 @@ def Array.swaps (a : Array α) : List (Fin a.size × Fin a.size) → Array α
   | [] => a
   | (i, j) :: ijs =>
     have : (a.swap i j).size = a.size := a.size_swap _ _
-
-    swaps (a.swap i j) (ijs.map (fun p => ⟨⟨p.1.1, this.symm ▸ p.1.2⟩, ⟨p.2.1, this.symm ▸ p.2.2⟩⟩))
+    swaps (a.swap i j) (ijs.map (fun p => ⟨⟨p.1.1, by simp⟩, ⟨p.2.1, by simp⟩⟩))
 termination_by l => l.length
 
 set_option maxHeartbeats 1000 in

tests/lean/run/986.lean

@@ -11,7 +11,7 @@ info: Array.insertionSort.swapLoop.eq_1.{u_1} {α : Type u_1} (lt : α → α 
 info: Array.insertionSort.swapLoop.eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
   (h : j'.succ < a.size) :
   Array.insertionSort.swapLoop lt a j'.succ h =
-    if lt a[j'.succ] a[j'] = true then Array.insertionSort.swapLoop lt (a.swap ⟨j'.succ, h⟩ ⟨j', ⋯⟩) j' ⋯ else a
+    if lt a[j'.succ] a[j'] = true then Array.insertionSort.swapLoop lt (a.swap j'.succ j' h ⋯) j' ⋯ else a
 -/
 #guard_msgs in
 #check Array.insertionSort.swapLoop.eq_2

tests/lean/run/heapSort.lean

@@ -103,10 +103,10 @@ def popMaxAux {lt} (self : BinaryHeap α lt) : {a' : BinaryHeap α lt // a'.size
   match e: self.1.size with
   | 0 => ⟨self, by simp [size, e]⟩
   | n+1 =>
-    have h0 := by rw [e]; apply Nat.succ_pos
-    have hn := by rw [e]; apply Nat.lt_succ_self
+    have h0 : 0 < self.1.size := by rw [e]; apply Nat.succ_pos
+    have hn : n < self.1.size := by rw [e]; apply Nat.lt_succ_self
     if hn0 : 0 < n then
-      let a := self.1.swap ⟨0, h0⟩ ⟨n, hn⟩ |>.pop
+      let a := self.1.swap 0 n |>.pop
       ⟨⟨heapifyDown lt a ⟨0, sorry⟩⟩,
         by simp [size, a]⟩
     else