chore(order/filter/basic): make filter.univ_mem_sets a simp lemma (…

…#5464)

src/data/list/basic.lean

@@ -1309,6 +1309,8 @@ variable {a : α}
 
 @[simp] lemma insert_nth_nil (a : α) : insert_nth 0 a [] = [a] := rfl
 
+@[simp] lemma insert_nth_succ_nil (n : ℕ) (a : α) : insert_nth (n + 1) a [] = [] := rfl
+
 lemma length_insert_nth : ∀n as, n ≤ length as → length (insert_nth n a as) = length as + 1
 | 0     as       h := rfl
 | (n+1) []       h := (nat.not_succ_le_zero _ h).elim

src/data/rel.lean

@@ -140,7 +140,7 @@ set.ext (by simp [mem_core, imp_and_distrib, forall_and_distrib])
 lemma core_union (s t : set β) : r.core s ∪ r.core t ⊆ r.core (s ∪ t) :=
 r.core_mono.le_map_sup s t
 
-lemma core_univ : r.core set.univ = set.univ := set.ext (by simp [mem_core])
+@[simp] lemma core_univ : r.core set.univ = set.univ := set.ext (by simp [mem_core])
 
 lemma core_id (s : set α) : core (@eq α) s = s :=
 by simp [core]

src/order/filter/basic.lean

@@ -119,7 +119,7 @@ by simp only [filter_eq_iff, ext_iff, filter.mem_sets]
 protected lemma ext : (∀ s, s ∈ f ↔ s ∈ g) → f = g :=
 filter.ext_iff.2
 
-lemma univ_mem_sets : univ ∈ f :=
+@[simp] lemma univ_mem_sets : univ ∈ f :=
 f.univ_sets
 
 lemma mem_sets_of_superset : ∀{x y : set α}, x ∈ f → x ⊆ y → y ∈ f :=
@@ -366,7 +366,7 @@ local attribute [instance] original_complete_lattice
 instance : complete_lattice (filter α) := original_complete_lattice.copy
   /- le  -/ filter.partial_order.le rfl
   /- top -/ (filter.has_top).1
-  (top_unique $ assume s hs, by have := univ_mem_sets ; finish)
+  (top_unique $ assume s hs, by simp [mem_top_sets.1 hs])
   /- bot -/ _ rfl
   /- sup -/ _ rfl
   /- inf -/ (filter.has_inf).1

src/order/filter/partial.lean

@@ -18,10 +18,10 @@ Relations.
 -/
 
 def rmap (r : rel α β) (f : filter α) : filter β :=
-{ sets             := {s | r.core s ∈  f},
-  univ_sets        := by { simp [rel.core], apply univ_mem_sets },
+{ sets             := {s | r.core s ∈ f},
+  univ_sets        := by simp,
   sets_of_superset := assume s t hs st, mem_sets_of_superset hs $ rel.core_mono _ st,
-  inter_sets       := by { simp [set.preimage, rel.core_inter], exact λ s t, inter_mem_sets } }
+  inter_sets       := λ s t hs ht, by simp [rel.core_inter, inter_mem_sets hs ht] }
 
 theorem rmap_sets (r : rel α β) (f : filter α) : (rmap r f).sets = r.core ⁻¹' f.sets := rfl
 

src/topology/list.lean

@@ -51,7 +51,7 @@ begin
       exact mem_traverse_sets _ _ (this.imp $ assume a s ⟨hs, ha⟩, mem_nhds_sets hs ha) } }
 end
 
-lemma nhds_nil : 𝓝 ([] : list α) = pure [] :=
+@[simp] lemma nhds_nil : 𝓝 ([] : list α) = pure [] :=
 by rw [nhds_list, list.traverse_nil _]; apply_instance
 
 lemma nhds_cons (a : α) (l : list α) :
@@ -104,16 +104,12 @@ end
 lemma tendsto_insert_nth' {a : α} : ∀{n : ℕ} {l : list α},
   tendsto (λp:α×list α, insert_nth n p.1 p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (insert_nth n a l))
 | 0     l  := tendsto_cons
-| (n+1) [] :=
-  suffices tendsto (λa, []) (𝓝 a) (𝓝 ([] : list α)),
-    by simpa [nhds_nil, tendsto, map_prod, (∘), insert_nth],
-  tendsto_const_nhds
+| (n+1) [] := by simp
 | (n+1) (a'::l) :=
   have 𝓝 a ×ᶠ 𝓝 (a' :: l) =
     (𝓝 a ×ᶠ (𝓝 a' ×ᶠ 𝓝 l)).map (λp:α×α×list α, (p.1, p.2.1 :: p.2.2)),
   begin
-    simp only
-      [nhds_cons, filter.prod_eq, (filter.map_def _ _).symm, (filter.seq_eq_filter_seq _ _).symm],
+    simp only [nhds_cons, filter.prod_eq, ← filter.map_def, ← filter.seq_eq_filter_seq],
     simp [-filter.seq_eq_filter_seq, -filter.map_def, (∘)] with functor_norm
   end,
   begin