chore(data/list/basic): drop append_foldl and append_foldr, add map_nil and prod_singleton (#2057)

`append_foldl` and `append_foldr` were unused duplicates of
`foldl_append` and `foldr_append`

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: urkud

src/data/list/basic.lean

@@ -2,15 +2,18 @@
 Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
-
-Basic properties of lists.
 -/
 import
   tactic.interactive tactic.mk_iff_of_inductive_prop
   logic.basic logic.function logic.relator
   algebra.group order.basic
   data.list.defs data.nat.basic data.option.basic
   data.bool data.prod data.fin
+
+/-!
+# Basic properties of lists
+-/
+
 open function nat
 
 namespace list
@@ -306,12 +309,6 @@ by induction s; intros; contradiction
 theorem append_ne_nil_of_ne_nil_right (s t : list α) : t ≠ [] → s ++ t ≠ [] :=
 by induction s; intros; contradiction
 
-theorem append_foldl (f : α → β → α) (a : α) (s t : list β) : foldl f a (s ++ t) = foldl f (foldl f a s) t :=
-by {induction s with b s H generalizing a, refl, simp only [foldl, cons_append], rw H _}
-
-theorem append_foldr (f : α → β → β) (a : β) (s t : list α) : foldr f a (s ++ t) = foldr f (foldr f a t) s :=
-by {induction s with b s H generalizing a, refl, simp only [foldr, cons_append], rw H _}
-
 @[simp] lemma append_eq_nil {p q : list α} : (p ++ q) = [] ↔ p = [] ∧ q = [] :=
 by cases p; simp only [nil_append, cons_append, eq_self_iff_true, true_and, false_and]
 
@@ -1086,6 +1083,8 @@ end insert_nth
 
 /- map -/
 
+@[simp] lemma map_nil (f : α → β) : map f [] = [] := rfl
+
 lemma map_congr {f g : α → β} : ∀ {l : list α}, (∀ x ∈ l, f x = g x) → map f l = map g l
 | []     _ := rfl
 | (a::l) h := let ⟨h₁, h₂⟩ := forall_mem_cons.1 h in
@@ -1495,6 +1494,9 @@ variables [monoid α] {l l₁ l₂ : list α} {a : α}
 @[simp, to_additive]
 theorem prod_nil : ([] : list α).prod = 1 := rfl
 
+@[to_additive]
+theorem prod_singleton : [a].prod = a := one_mul a
+
 @[simp, to_additive]
 theorem prod_cons : (a::l).prod = a * l.prod :=
 calc (a::l).prod = foldl (*) (a * 1) l : by simp only [list.prod, foldl_cons, one_mul, mul_one]