diff --git a/library/data/fin.lean b/library/data/fin.lean
index a72f6e47e..23a671afa 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -45,7 +45,7 @@ lemma upto_zero : upto 0 = [] :=
 by rewrite [↑upto, list.upto_nil, dmap_nil]
 
 lemma map_val_upto (n : nat) : map fin.val (upto n) = list.upto n :=
-map_dmap_of_pos_of_inv (val_mk n) (@lt_of_mem_upto n)
+map_dmap_of_inv_of_pos (val_mk n) (@lt_of_mem_upto n)
 
 lemma length_upto (n : nat) : length (upto n) = n :=
 calc
diff --git a/library/data/fintype/function.lean b/library/data/fintype/function.lean
index 44ad6c25e..9e7ebab77 100644
--- a/library/data/fintype/function.lean
+++ b/library/data/fintype/function.lean
@@ -290,7 +290,7 @@ lemma all_funs_complete (f : A → B) : f ∈ all_funs :=
       begin rewrite [fun_eq_list_to_fun_map f (length_map_of_fintype f)], apply Plfin end
 
 lemma all_funs_to_all_lists : map fun_to_list (@all_funs A B _ _ _) = all_lists_of_len (card A) :=
-      map_dmap_of_pos_of_inv list_to_fun_to_list leq_of_mem_all_lists
+      map_dmap_of_inv_of_pos list_to_fun_to_list leq_of_mem_all_lists
 
 lemma length_all_funs : length (@all_funs A B _ _ _) = (card B) ^ (card A) := calc
       length _ = length (map fun_to_list all_funs) : length_map
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index 9036acc83..e14ad966d 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -425,16 +425,16 @@ lemma exists_of_mem_dmap : ∀ {l : list A} {b : B}, b ∈ dmap p f l → ∃ a
   exact exists.intro a' (exists.intro Pa' (and.intro (mem_cons_of_mem a (and.left P')) (and.right P')))
   end)
 
-lemma map_dmap_of_pos_of_inv {g : B → A} (Pinv : ∀ a (Pa : p a), g (f a Pa) = a) :
+lemma map_dmap_of_inv_of_pos {g : B → A} (Pinv : ∀ a (Pa : p a), g (f a Pa) = a) :
                           ∀ {l : list A}, (∀ ⦃a⦄, a ∈ l → p a) → map g (dmap p f l) = l
 | []     := assume Pl, by rewrite [dmap_nil, map_nil]
 | (a::l) := assume Pal,
             assert Pa : p a, from Pal a !mem_cons,
             assert Pl : ∀ a, a ∈ l → p a,
               from take x Pxin, Pal x (mem_cons_of_mem a Pxin),
-            by rewrite [dmap_cons_of_pos Pa, map_cons, Pinv, map_dmap_of_pos_of_inv Pl]
+            by rewrite [dmap_cons_of_pos Pa, map_cons, Pinv, map_dmap_of_inv_of_pos Pl]
 
-lemma mem_of_mem_dmap_of_dinj (Pdi : dinj p f) :
+lemma mem_of_dinj_of_mem_dmap (Pdi : dinj p f) :
       ∀ {l : list A} {a} (Pa : p a), (f a Pa) ∈ dmap p f l → a ∈ l
 | []     := take a Pa Pinnil, by contradiction
 | (b::l) := take a Pa Pmap,
@@ -445,17 +445,17 @@ lemma mem_of_mem_dmap_of_dinj (Pdi : dinj p f) :
                 rewrite mem_cons_iff,
                 apply (or_of_or_of_imp_of_imp Pmap),
                   apply Pdi,
-                  apply mem_of_mem_dmap_of_dinj Pa
+                  apply mem_of_dinj_of_mem_dmap Pa
               end)
               (λ nPb, begin
                  rewrite (dmap_cons_of_neg nPb) at Pmap,
                  apply mem_cons_of_mem,
-                 exact mem_of_mem_dmap_of_dinj Pa Pmap
+                 exact mem_of_dinj_of_mem_dmap Pa Pmap
               end)
 
-lemma not_mem_dmap_of_not_mem_of_dinj (Pdi : dinj p f) {l : list A} {a} (Pa : p a) :
+lemma not_mem_dmap_of_dinj_of_not_mem (Pdi : dinj p f) {l : list A} {a} (Pa : p a) :
   a ∉ l → (f a Pa) ∉ dmap p f l :=
-not_imp_not_of_imp (mem_of_mem_dmap_of_dinj Pdi Pa)
+not_imp_not_of_imp (mem_of_dinj_of_mem_dmap Pdi Pa)
 
 end dmap
 
diff --git a/library/data/list/set.lean b/library/data/list/set.lean
index c3c45d7b6..c8a88a994 100644
--- a/library/data/list/set.lean
+++ b/library/data/list/set.lean
@@ -435,7 +435,7 @@ lemma dmap_nodup_of_dinj {p : A → Prop} [h : decidable_pred p] {f : Π a, p a
                   begin
                     rewrite [dmap_cons_of_pos Pa],
                     apply nodup_cons,
-                    apply (not_mem_dmap_of_not_mem_of_dinj Pdi Pa),
+                    apply (not_mem_dmap_of_dinj_of_not_mem Pdi Pa),
                     exact not_mem_of_nodup_cons Pnodup,
                     exact dmap_nodup_of_dinj (nodup_of_nodup_cons Pnodup)
                   end)