feat(*): assorted simple lemmas, simplify some proofs (#1895)

* feat(*): assorted simple lemmas, simplify some proofs

* +1 lemma, +1 simplified proof

Author: urkud

src/data/real/ennreal.lean

@@ -870,6 +870,10 @@ by rw [ennreal.of_real, ennreal.of_real, coe_le_coe, nnreal.of_real_le_of_real_i
 @[simp] lemma of_real_lt_of_real_iff {p q : ℝ} (h : 0 < q) : ennreal.of_real p < ennreal.of_real q ↔ p < q :=
 by rw [ennreal.of_real, ennreal.of_real, coe_lt_coe, nnreal.of_real_lt_of_real_iff h]
 
+lemma of_real_lt_of_real_iff_of_nonneg {p q : ℝ} (hp : 0 ≤ p) :
+  ennreal.of_real p < ennreal.of_real q ↔ p < q :=
+by rw [ennreal.of_real, ennreal.of_real, coe_lt_coe, nnreal.of_real_lt_of_real_iff_of_nonneg hp]
+
 @[simp] lemma of_real_pos {p : ℝ} : 0 < ennreal.of_real p ↔ 0 < p :=
 by simp [ennreal.of_real]
 

src/data/real/nnreal.lean

@@ -294,6 +294,10 @@ lemma of_real_lt_of_real_iff {r p : ℝ} (h : 0 < p) :
   nnreal.of_real r < nnreal.of_real p ↔ r < p :=
 of_real_lt_of_real_iff'.trans (and_iff_left h)
 
+lemma of_real_lt_of_real_iff_of_nonneg {r p : ℝ} (hr : 0 ≤ r) :
+  nnreal.of_real r < nnreal.of_real p ↔ r < p :=
+of_real_lt_of_real_iff'.trans ⟨and.left, λ h, ⟨h, lt_of_le_of_lt hr h⟩⟩
+
 @[simp] lemma of_real_add {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :
   nnreal.of_real (r + p) = nnreal.of_real r + nnreal.of_real p :=
 nnreal.eq $ by simp [nnreal.of_real, hr, hp, add_nonneg]

src/data/set/basic.lean

@@ -990,6 +990,9 @@ by simp only [eq_empty_iff_forall_not_mem]; exact
 lemma inter_singleton_ne_empty {s : set α} {a : α} : s ∩ {a} ≠ ∅ ↔ a ∈ s :=
 by finish  [set.inter_singleton_eq_empty]
 
+lemma inter_singleton_nonempty {s : set α} {a : α} : (s ∩ {a}).nonempty ↔ a ∈ s :=
+ne_empty_iff_nonempty.symm.trans inter_singleton_ne_empty
+
 theorem fix_set_compl (t : set α) : compl t = - t := rfl
 
 -- TODO(Jeremy): there is an issue with - t unfolding to compl t

src/data/set/intervals/basic.lean

@@ -109,6 +109,10 @@ set.ext $ λ x, and_comm _ _
 @[simp] lemma nonempty_Ioo [densely_ordered α] : (Ioo a b).nonempty ↔ a < b :=
 ⟨λ ⟨x, ha, hb⟩, lt_trans ha hb, dense⟩
 
+@[simp] lemma nonempty_Ioi [no_top_order α] : (Ioi a).nonempty := no_top a
+
+@[simp] lemma nonempty_Iio [no_bot_order α] : (Iio a).nonempty := no_bot a
+
 @[simp] lemma Ioo_eq_empty (h : b ≤ a) : Ioo a b = ∅ :=
 eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, not_le_of_lt (lt_trans h₁ h₂) h
 

src/order/basic.lean

@@ -578,6 +578,11 @@ theorem directed_mono {s : α → α → Prop} {ι} (f : ι → α)
   (H : ∀ a b, r a b → s a b) (h : directed r f) : directed s f :=
 λ a b, let ⟨c, h₁, h₂⟩ := h a b in ⟨c, H _ _ h₁, H _ _ h₂⟩
 
+theorem directed.mono_comp {ι} {rb : β → β → Prop} {g : α → β} {f : ι → α}
+  (hg : ∀ ⦃x y⦄, x ≼ y → rb (g x) (g y)) (hf : directed r f) :
+  directed rb (g ∘ f) :=
+(directed_comp rb f g).2 $ directed_mono _ _ hg hf
+
 section prio
 set_option default_priority 100 -- see Note [default priority]
 class directed_order (α : Type u) extends preorder α :=

src/order/bounded_lattice.lean

@@ -716,6 +716,10 @@ instance densely_ordered [partial_order α] [densely_ordered α] [no_top_order 
     ⟨a, coe_lt_coe.2 ha₁, coe_lt_coe.2 ha₂⟩
   end⟩
 
+lemma dense_coe [partial_order α] [densely_ordered α] [no_top_order α] {a b : with_top α}
+  (h : a < b) : ∃ x : α, a < ↑x ∧ ↑x < b :=
+let ⟨y, hy⟩ := dense h, ⟨x, hx⟩ := (lt_iff_exists_coe _ _).1 hy.2 in ⟨x, hx.1 ▸ hy⟩
+
 end with_top
 
 namespace order_dual

src/order/filter/basic.lean

@@ -407,6 +407,10 @@ by
   simp only [(@empty_in_sets_eq_bot α f).symm, ne.def];
   exact ⟨assume h hs, h _ hs rfl, assume h s hs eq, h $ eq ▸ hs⟩
 
+lemma forall_sets_nonempty_iff_ne_bot {f : filter α} :
+  (∀ (s : set α), s ∈ f → s.nonempty) ↔ f ≠ ⊥ :=
+by simpa only [ne_empty_iff_nonempty] using forall_sets_ne_empty_iff_ne_bot
+
 lemma mem_sets_of_eq_bot {f : filter α} {s : set α} (h : f ⊓ principal (-s) = ⊥) : s ∈ f :=
 have ∅ ∈ f ⊓ principal (- s), from h.symm ▸ mem_bot_sets,
 let ⟨s₁, hs₁, s₂, (hs₂ : -s ⊆ s₂), (hs : s₁ ∩ s₂ ⊆ ∅)⟩ := this in
@@ -455,7 +459,7 @@ by simp only [infi_sets_eq h ne, mem_Union]
 
 @[nolint] -- Intentional use of `≥`
 lemma binfi_sets_eq {f : β → filter α} {s : set β}
-  (h : directed_on (f ⁻¹'o (≥)) s) (ne : ∃i, i ∈ s) :
+  (h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) :
   (⨅ i∈s, f i).sets = (⋃ i ∈ s, (f i).sets) :=
 let ⟨i, hi⟩ := ne in
 calc (⨅ i ∈ s, f i).sets  = (⨅ t : {t // t ∈ s}, (f t.val)).sets : by rw [infi_subtype]; refl
@@ -466,7 +470,7 @@ calc (⨅ i ∈ s, f i).sets  = (⨅ t : {t // t ∈ s}, (f t.val)).sets : by rw
 
 @[nolint] -- Intentional use of `≥`
 lemma mem_binfi {f : β → filter α} {s : set β}
-  (h : directed_on (f ⁻¹'o (≥)) s) (ne : ∃i, i ∈ s) {t : set α} :
+  (h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) {t : set α} :
   t ∈ (⨅ i∈s, f i) ↔ ∃ i ∈ s, t ∈ f i :=
 by simp only [binfi_sets_eq h ne, mem_bUnion_iff]
 

src/topology/basic.lean

@@ -280,13 +280,7 @@ by rw subset.antisymm subset_closure h; exact is_closed_closure
 closure_eq_of_is_closed is_closed_empty
 
 lemma closure_empty_iff (s : set α) : closure s = ∅ ↔ s = ∅ :=
-begin
-  split; intro h,
-  { rw set.eq_empty_iff_forall_not_mem,
-    intros x H,
-    simpa only [h] using subset_closure H },
-  { exact (eq.symm h) ▸ closure_empty },
-end
+⟨subset_eq_empty subset_closure, λ h, h.symm ▸ closure_empty⟩
 
 @[simp] lemma closure_univ : closure (univ : set α) = univ :=
 closure_eq_of_is_closed is_closed_univ

src/topology/continuous_on.lean

@@ -65,11 +65,7 @@ lemma mem_nhds_within_of_mem_nhds {s t : set α} {a : α} (h : s ∈ 𝓝 a) :
 mem_inf_sets_of_left h
 
 theorem self_mem_nhds_within {a : α} {s : set α} : s ∈ nhds_within a s :=
-begin
-  rw [nhds_within, mem_inf_principal],
-  simp only [imp_self],
-  exact univ_mem_sets
-end
+mem_inf_sets_of_right (mem_principal_self s)
 
 theorem inter_mem_nhds_within (s : set α) {t : set α} {a : α} (h : t ∈ 𝓝 a) :
   s ∩ t ∈ nhds_within a s :=

src/topology/sequences.lean

@@ -74,21 +74,8 @@ show A = sequential_closure A, from subset.antisymm
 /-- The sequential closure of a set is contained in the closure of that set.
 The converse is not true. -/
 lemma sequential_closure_subset_closure (M : set α) : sequential_closure M ⊆ closure M :=
-show ∀ p, p ∈ sequential_closure M → p ∈ closure M, from
-assume p,
-assume : ∃ x : ℕ → α, (∀ n : ℕ, ((x n) ∈ M)) ∧ (x ⟶ p),
-let ⟨x, ⟨_, _⟩⟩ := this in
-show p ∈ closure M, from
--- we have to show that p is in the closure of M
--- using mem_closure_iff, this is equivalent to proving that every open neighbourhood
--- has nonempty intersection with M, but this is witnessed by our sequence x
-suffices ∀ O, is_open O → p ∈ O → O ∩ M ≠ ∅, from mem_closure_iff.mpr this,
-have ∀ (U : set α), p ∈ U → is_open U → (∃ n0, ∀ n, n ≥ n0 → x n ∈ U), by rwa[←topological_space.seq_tendsto_iff],
-assume O is_open_O p_in_O,
-let ⟨n0, _⟩ := this O ‹p ∈ O› ‹is_open O› in
-have (x n0) ∈ O, from ‹∀ n ≥ n0, x n ∈ O› n0 (show n0 ≥ n0, from le_refl n0),
-have (x n0) ∈ O ∩ M, from ⟨this, ‹∀n, x n ∈ M› n0⟩,
-set.ne_empty_of_mem this
+assume p ⟨x, xM, xp⟩,
+mem_closure_of_tendsto at_top_ne_bot xp (univ_mem_sets' xM)
 
 /-- A set is sequentially closed if it is closed. -/
 lemma is_seq_closed_of_is_closed (M : set α) (_ : is_closed M) : is_seq_closed M :=