feat(init/function): comp_app simp lemma

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 -/
 

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