refactor: replace length_dropLast theorem

doc/examples/palindromes.lean

@@ -81,12 +81,10 @@ theorem List.palindrome_ind (motive : List α → Prop)
   | []  => h₁
   | [a] => h₂ a
   | a₁::a₂::as' =>
-    have : [a₁] ++ (a₂::as').dropLast ++ [(a₂::as').last (by simp)] = a₁::a₂::as' := by simp
     have ih := palindrome_ind motive h₁ h₂ h₃ (a₂::as').dropLast
+    have : [a₁] ++ (a₂::as').dropLast ++ [(a₂::as').last (by simp)] = a₁::a₂::as' := by simp
     this ▸ h₃ _ _ _ ih
 termination_by _ as => as.length
--- TODO: remove the following tactic after we add `linarith`
-decreasing_by simp_wf; rw [Nat.succ_sub_succ, Nat.sub_zero]; simp_arith
 
 /-|
 We use our new induction principle to prove that if `as.reverse = as`, then `Palindrome as` holds.

src/Init/Data/Array/Basic.lean

@@ -628,8 +628,10 @@ def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
   rw [size_set, size_set]
 
-@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 :=
-  List.length_dropLast ..
+@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
+  match a with
+  | ⟨[]⟩ => rfl
+  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub]
 
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then

src/Init/Data/List/Basic.lean

@@ -485,14 +485,12 @@ def dropLast {α} : List α → List α
     | zero => rfl
     | succ i => simp [set, ih]
 
-@[simp] theorem length_dropLast (as : List α) : as.dropLast.length = as.length - 1 := by
+@[simp] theorem length_dropLast_cons (a : α) (as : List α) : (a :: as).dropLast.length = as.length := by
   match as with
   | []       => rfl
-  | [a]      => rfl
-  | a::b::as =>
-    have ih := length_dropLast (b::as)
+  | b::bs =>
+    have ih := length_dropLast_cons b bs
     simp[dropLast, ih]
-    rfl
 
 @[simp] theorem length_append (as bs : List α) : (as ++ bs).length = as.length + bs.length := by
   induction as with