diff --git a/doc/monads/applicatives.lean b/doc/monads/applicatives.lean
index dd19b081401c..3bf69c0260dd 100644
--- a/doc/monads/applicatives.lean
+++ b/doc/monads/applicatives.lean
@@ -138,8 +138,8 @@ definition:
 
 -/
 instance : Applicative List where
-  pure := List.pure
-  seq f x := List.bind f fun y => Functor.map y (x ())
+  pure := List.singleton
+  seq f x := List.flatMap f fun y => Functor.map y (x ())
 /-!
 
 Notice you can now sequence a _list_ of functions and a _list_ of items.
diff --git a/doc/monads/laws.lean b/doc/monads/laws.lean
index bef495a1c3c8..d37c70b08185 100644
--- a/doc/monads/laws.lean
+++ b/doc/monads/laws.lean
@@ -128,8 +128,8 @@ Applying the identity function through an applicative structure should not chang
 values or structure.  For example:
 -/
 instance : Applicative List where
-  pure := List.pure
-  seq f x := List.bind f fun y => Functor.map y (x ())
+  pure := List.singleton
+  seq f x := List.flatMap f fun y => Functor.map y (x ())
 
 #eval pure id <*> [1, 2, 3]  -- [1, 2, 3]
 /-!
@@ -235,8 +235,8 @@ structure or its values.
 Left identity is `x >>= pure = x` and is demonstrated by the following examples on a monadic `List`:
 -/
 instance : Monad List  where
-  pure := List.pure
-  bind := List.bind
+  pure := List.singleton
+  bind := List.flatMap
 
 def a := ["apple", "orange"]
 
diff --git a/doc/monads/monads.lean b/doc/monads/monads.lean
index c8919709a616..f2a44685aad2 100644
--- a/doc/monads/monads.lean
+++ b/doc/monads/monads.lean
@@ -192,8 +192,8 @@ implementation of `pure` and `bind`.
 
 -/
 instance : Monad List  where
-  pure := List.pure
-  bind := List.bind
+  pure := List.singleton
+  bind := List.flatMap
 /-!
 
 Like you saw with the applicative `seq` operator, the `bind` operator applies the given function
diff --git a/tests/lean/run/subexpr.lean b/tests/lean/run/subexpr.lean
index 742f803a4fc8..8f23ff87b37f 100644
--- a/tests/lean/run/subexpr.lean
+++ b/tests/lean/run/subexpr.lean
@@ -8,7 +8,7 @@ theorem Pos.roundtrip :
 
 theorem Pos.append_roundtrip :
   true = (List.all
-    (ps.bind fun p => ps.map fun q => (p,q))
+    (ps.flatMap fun p => ps.map fun q => (p,q))
     (fun (x,y) => (x ++ y) == (Pos.toArray <| (Pos.append (Pos.ofArray x) (Pos.ofArray y))))
   ) := by native_decide
 
diff --git a/tests/lean/run/treeNode.lean b/tests/lean/run/treeNode.lean
index 12958ee83c80..961386d87b69 100644
--- a/tests/lean/run/treeNode.lean
+++ b/tests/lean/run/treeNode.lean
@@ -1,4 +1,4 @@
-inductive TreeNode :=
+inductive TreeNode where
  | mkLeaf (name : String) : TreeNode
  | mkNode (name : String) (children : List TreeNode) : TreeNode
 
@@ -13,11 +13,11 @@ def treeToList (t : TreeNode) : List String :=
      r := r ++ treeToList child
    return r
 
-@[simp] theorem treeToList_eq (name : String) (children : List TreeNode) : treeToList (.mkNode name children) =  name :: List.join (children.map treeToList) := by
+@[simp] theorem treeToList_eq (name : String) (children : List TreeNode) : treeToList (.mkNode name children) =  name :: List.flatten (children.map treeToList) := by
   simp only [treeToList, Id.run, Id.pure_eq, Id.bind_eq, List.forIn'_eq_forIn, forIn, List.forIn]
-  have : ∀ acc, (Id.run do List.forIn.loop (fun a b => ForInStep.yield (b ++ treeToList a)) children acc) = acc ++ List.join (List.map treeToList children) := by
+  have : ∀ acc, (Id.run do List.forIn.loop (fun a b => ForInStep.yield (b ++ treeToList a)) children acc) = acc ++ List.flatten (List.map treeToList children) := by
     intro acc
-    induction children generalizing acc with simp [List.forIn.loop, List.map, List.join, Id.run]
+    induction children generalizing acc with simp [List.forIn.loop, List.map, List.flatten, Id.run]
     | cons c cs ih => simp [Id.run] at ih; simp [ih, List.append_assoc]
   apply this
 
@@ -35,7 +35,7 @@ theorem length_treeToList_eq_numNames (t : TreeNode) : (treeToList t).length = n
   | .mkLeaf .. => simp [treeToList, numNames]
   | .mkNode _ cs => simp_arith [numNames, helper cs]
 where
-  helper (cs : List TreeNode) : (cs.map treeToList).join.length = numNamesLst cs := by
+  helper (cs : List TreeNode) : (cs.map treeToList).flatten.length = numNamesLst cs := by
     match cs with
-    | [] => simp [List.join, numNamesLst]
-    | c::cs' => simp [List.join, List.map, numNamesLst, length_treeToList_eq_numNames c, helper cs']
+    | [] => simp [List.flatten, numNamesLst]
+    | c::cs' => simp [List.flatten, List.map, numNamesLst, length_treeToList_eq_numNames c, helper cs']
diff --git a/tests/lean/treeMap.lean b/tests/lean/treeMap.lean
index c18f36b4c800..ac5adbaa803b 100644
--- a/tests/lean/treeMap.lean
+++ b/tests/lean/treeMap.lean
@@ -1,9 +1,9 @@
-inductive TreeNode :=
+inductive TreeNode where
  | mkLeaf (name : String) : TreeNode
  | mkNode (name : String) (children : List TreeNode) : TreeNode
 
 open TreeNode in def treeToList (t : TreeNode) : List String :=
  match t with
  | mkLeaf name => [name]
- | mkNode name children => name :: List.join (children.map treeToList)
+ | mkNode name children => name :: List.flatten (children.map treeToList)
 termination_by t
diff --git a/tests/lean/treeMap.lean.expected.out b/tests/lean/treeMap.lean.expected.out
index 58a4d88893e7..14574d68e743 100644
--- a/tests/lean/treeMap.lean.expected.out
+++ b/tests/lean/treeMap.lean.expected.out
@@ -1,4 +1,4 @@
-treeMap.lean:8:59-8:69: error: failed to prove termination, possible solutions:
+treeMap.lean:8:62-8:72: error: failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal