diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean
index efd4130f91..ad642c786e 100644
--- a/library/init/data/list/lemmas.lean
+++ b/library/init/data/list/lemmas.lean
@@ -192,8 +192,7 @@ theorem length_remove_nth : ∀ (l : list α) (i : ℕ), i < length l → length
 
 @[simp] lemma partition_eq_filter_filter (p : α → Prop) [decidable_pred p] : ∀ (l : list α), partition p l = (filter p l, filter (not ∘ p) l)
 | []     := rfl
-| (a::l) := by { by_cases pa : p a; simp [partition, filter, pa, partition_eq_filter_filter l],
-                 rw [if_neg (not_not_intro pa)], rw [if_pos pa] }
+| (a::l) := by { by_cases pa : p a; simp [partition, filter, pa, partition_eq_filter_filter l] }
 
 /- sublists -/
 
diff --git a/library/init/function.lean b/library/init/function.lean
index abcd06a6c2..648a6ea1ef 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -51,6 +51,8 @@ lemma left_id (f : α → β) : id ∘ f = f := rfl
 
 lemma right_id (f : α → β) : f ∘ id = f := rfl
 
+@[simp] lemma comp_app (f : β → φ) (g : α → β) (a : α) : (f ∘ g) a = f (g a) := rfl
+
 lemma comp.assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
 
 lemma comp.left_id (f : α → β) : id ∘ f = f := rfl