feat: complete API for List.replicate (#4487)

This is not the most exciting place to start, but I started here to:
* pick a function with little development in Batteries and Mathlib, so I
wouldn't have conflicts
* that is easy!
* to see how much effort it is to get fairly complete coverage
* and to set up some infrastructure to be used later, i.e.
`tests/lean/run/list_simp.lean`

src/Init/Data/List/Basic.lean

@@ -567,10 +567,12 @@ def replicate : (n : Nat) → (a : α) → List α
   | n+1, a => a :: replicate n a
 
 @[simp] theorem replicate_zero : replicate 0 a = [] := rfl
-@[simp] theorem replicate_succ (a : α) (n) : replicate (n+1) a = a :: replicate n a := rfl
+theorem replicate_succ (a : α) (n) : replicate (n+1) a = a :: replicate n a := rfl
 
 @[simp] theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
-  induction n <;> simp_all
+  induction n with
+  | zero => simp
+  | succ n ih => simp only [ih, replicate_succ, length_cons, Nat.succ_eq_add_one]
 
 /-! ## List membership
 
@@ -609,13 +611,13 @@ def isEmpty : List α → Bool
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false
-  | b::bs => match b == a with
+  | b::bs => match a == b with
     | true  => true
     | false => elem a bs
 
 @[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
 theorem elem_cons [BEq α] {a : α} :
-    (a::as).elem b = match a == b with | true => true | false => as.elem b := rfl
+    (b::bs).elem a = match a == b with | true => true | false => bs.elem a := rfl
 
 /-- `notElem a l` is `!(elem a l)`. -/
 @[deprecated (since := "2024-06-15")]
@@ -850,6 +852,9 @@ That is, there exists a `t` such that `l₂ == t ++ l₁`. -/
 def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
   isPrefixOf l₁.reverse l₂.reverse
 
+@[simp] theorem isSuffixOf_nil_left [BEq α] : isSuffixOf ([] : List α) l = true := by
+  simp [isSuffixOf]
+
 /-! ### isSuffixOf? -/
 
 /-- `isSuffixOf? l₁ l₂` returns `some t` when `l₂ == t ++ l₁`.-/
@@ -906,13 +911,13 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α :=
 -/
 def replace [BEq α] : List α → α → α → List α
   | [],    _, _ => []
-  | a::as, b, c => match a == b with
+  | a::as, b, c => match b == a with
     | true  => c::as
     | false => a :: replace as b c
 
 @[simp] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
 theorem replace_cons [BEq α] {a : α} :
-    (a::as).replace b c = match a == b with | true => c::as | false => a :: replace as b c :=
+    (a::as).replace b c = match b == a with | true => c::as | false => a :: replace as b c :=
   rfl
 
 /-! ### insert -/

src/Init/Data/List/Impl.lean

@@ -258,7 +258,7 @@ theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++
   unless `b` is not found in `xs` in which case it returns `l`. -/
   @[specialize] go : List α → Array α → List α
   | [], _ => l
-  | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a)
+  | a::as, acc => bif b == a then acc.toListAppend (c::as) else go as (acc.push a)
 
 @[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
   funext α _ l b c; simp [replaceTR]