refactor(analysis/specific_limits): generalize has_sum_of_absolute_co…

…nvergence to normed_groups

src/analysis/normed_space/basic.lean

@@ -84,6 +84,20 @@ calc ∥-g∥ = ∥0 - g∥ : by simp
       ... = ∥g - 0∥ : (dist_eq_norm g 0)
       ... = ∥g∥ : by simp
 
+lemma norm_triangle_sub {a b : α} : ∥a - b∥ ≤ ∥a∥ + ∥b∥ :=
+by simpa only [sub_eq_add_neg, norm_neg] using norm_triangle a (-b)
+
+lemma norm_triangle_sum {β} [decidable_eq β] (s : finset β) (f : β → α) :
+  ∥s.sum f∥ ≤ s.sum (λa, ∥ f a ∥) :=
+finset.induction_on s (by simp only [finset.sum_empty, norm_zero]; exact le_refl _)
+begin
+  assume a s has ih,
+  calc ∥(insert a s).sum f∥ ≤ ∥ f a + s.sum f ∥ : by rw [finset.sum_insert has]
+    ... ≤ ∥ f a ∥ + ∥ s.sum f ∥ : norm_triangle _ _
+    ... ≤ ∥ f a ∥ + s.sum (λa, ∥ f a ∥) : add_le_add_left ih _
+    ... = (insert a s).sum (λa, ∥ f a ∥) : by rw [finset.sum_insert has]
+end
+
 lemma abs_norm_sub_norm_le (g h : α) : abs(∥g∥ - ∥h∥) ≤ ∥g - h∥ :=
 abs_le.2 $ and.intro
   (suffices -∥g - h∥ ≤ -(∥h∥ - ∥g∥), by simpa,

src/analysis/specific_limits.lean

@@ -5,64 +5,61 @@ Authors: Johannes Hölzl
 
 A collection of specific limit computations.
 -/
-import algebra.big_operators algebra.group_power tactic.norm_num
-  topology.instances.ennreal topology.algebra.infinite_sum
+import analysis.normed_space.basic
+import topology.instances.ennreal
+
 noncomputable theory
-open classical finset function filter metric
-local attribute [instance] prop_decidable
-
-lemma has_sum_of_absolute_convergence {f : ℕ → ℝ}
-  (hf : ∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (nhds r)) : has_sum f :=
-let f' := λs:finset ℕ, s.sum (λi, abs (f i)) in
-suffices cauchy (map (λs:finset ℕ, s.sum f) at_top),
-  from complete_space.complete this,
-cauchy_iff.mpr $ and.intro (map_ne_bot at_top_ne_bot) $
-assume s hs,
-let ⟨ε, hε, hsε⟩ := mem_uniformity_dist.mp hs, ⟨r, hr⟩ := hf in
-have hε' : {p : ℝ × ℝ | dist p.1 p.2 < ε / 2} ∈ (@uniformity ℝ _).sets,
-  from mem_uniformity_dist.mpr ⟨ε / 2, div_pos_of_pos_of_pos hε two_pos, assume a b h, h⟩,
-have cauchy (at_top.map $ λn, f' (range n)),
-  from cauchy_downwards cauchy_nhds (map_ne_bot at_top_ne_bot) hr,
-have ∃n, ∀{n'}, n ≤ n' → dist (f' (range n)) (f' (range n')) < ε / 2,
-  by simp [cauchy_iff, mem_at_top_sets] at this;
-  from let ⟨t, ⟨u, hu⟩, ht⟩ := this _ hε' in
-    ⟨u, assume n' hn, ht $ set.prod_mk_mem_set_prod_eq.mpr ⟨hu _ (le_refl _), hu _ hn⟩⟩,
-let ⟨n, hn⟩ := this in
-have ∀{s}, range n ⊆ s → abs ((s \ range n).sum f) < ε / 2,
-  from assume s hs,
-  let ⟨n', hn'⟩ := @exists_nat_subset_range s in
-  have range n ⊆ range n', from finset.subset.trans hs hn',
-  have f'_nn : 0 ≤ f' (range n' \ range n), from zero_le_sum $ assume _ _, abs_nonneg _,
-  calc abs ((s \ range n).sum f) ≤ f' (s \ range n) : abs_sum_le_sum_abs
-    ... ≤ f' (range n' \ range n) : sum_le_sum_of_subset_of_nonneg
-      (finset.sdiff_subset_sdiff hn' (finset.subset.refl _))
-      (assume _ _ _, abs_nonneg _)
-    ... = abs (f' (range n' \ range n)) : (abs_of_nonneg f'_nn).symm
-    ... = abs (f' (range n') - f' (range n)) :
-      by simp [f', (sum_sdiff ‹range n ⊆ range n'›).symm]
-    ... = abs (f' (range n) - f' (range n')) : abs_sub _ _
-    ... < ε / 2 : hn $ range_subset.mp this,
-have ∀{s t}, range n ⊆ s → range n ⊆ t → dist (s.sum f) (t.sum f) < ε,
-  from assume s t hs ht,
-  calc abs (s.sum f - t.sum f) = abs ((s \ range n).sum f + - (t \ range n).sum f) :
-      by rw [←sum_sdiff hs, ←sum_sdiff ht]; simp
-    ... ≤ abs ((s \ range n).sum f) + abs ((t \ range n).sum f) :
-      le_trans (abs_add_le_abs_add_abs _ _) $ by rw [abs_neg]; exact le_refl _
-    ... < ε / 2 + ε / 2 : add_lt_add (this hs) (this ht)
-    ... = ε : by rw [←add_div, add_self_div_two],
-⟨(λs:finset ℕ, s.sum f) '' {s | range n ⊆ s}, image_mem_map $ mem_at_top (range n),
-  assume ⟨a, b⟩ ⟨⟨t, ht, ha⟩, ⟨s, hs, hb⟩⟩, by simp at ha hb; exact ha ▸ hb ▸ hsε (this ht hs)⟩
-
-lemma is_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} {r : ℝ} (hf : ∀n, 0 ≤ f n) :
-  is_sum f r ↔ tendsto (λn, (range n).sum f) at_top (nhds r) :=
-⟨tendsto_sum_nat_of_is_sum,
-  assume hr,
-  have tendsto (λn, (range n).sum (λn, abs (f n))) at_top (nhds r),
-    by simp [(λi, abs_of_nonneg (hf i)), hr],
-  let ⟨p, h⟩ := has_sum_of_absolute_convergence ⟨r, this⟩ in
-  have hp : tendsto (λn, (range n).sum f) at_top (nhds p), from tendsto_sum_nat_of_is_sum h,
-  have p = r, from tendsto_nhds_unique at_top_ne_bot hp hr,
-  this ▸ h⟩
+local attribute [instance] classical.prop_decidable
+
+open classical function lattice filter finset metric
+
+variables {α : Type*} {β : Type*} {ι : Type*}
+
+lemma has_sum_iff_cauchy [normed_group α] [complete_space α] {f : ι → α} :
+  has_sum f ↔ ∀ε>0, (∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε) :=
+begin
+  refine iff.trans (cauchy_map_iff_exists_tendsto at_top_ne_bot).symm _,
+  simp only [cauchy_map_iff, and_iff_right at_top_ne_bot, prod_at_top_at_top_eq, uniformity_dist,
+    tendsto_infi, tendsto_at_top_principal, set.mem_set_of_eq],
+  split,
+  { assume h ε hε,
+    rcases h ε hε with ⟨⟨s₁, s₂⟩, h⟩,
+    use [s₁ ∪ s₂],
+    assume t ht,
+    have : (s₁ ∪ s₂) ∩ t = ∅ := finset.disjoint_iff_inter_eq_empty.1 ht.symm,
+    specialize h (s₁ ∪ s₂, (s₁ ∪ s₂) ∪ t) ⟨le_sup_left, le_sup_left_of_le le_sup_right⟩,
+    simpa only [finset.sum_union this, dist_eq_norm,
+      sub_add_eq_sub_sub, sub_self, zero_sub, norm_neg] using h },
+  { assume h' ε hε,
+    rcases h' (ε / 2) (half_pos hε) with ⟨s, h⟩,
+    use [(s, s)],
+    rintros ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩,
+    dsimp at ht₁ ht₂,
+    calc dist (t₁.sum f) (t₂.sum f) = ∥sum (t₁ \ s) f - sum (t₂ \ s) f∥ :
+        by simp only [(finset.sum_sdiff ht₁).symm, (finset.sum_sdiff ht₂).symm,
+          dist_eq_norm, add_sub_add_right_eq_sub]
+      ... ≤ ∥sum (t₁ \ s) f∥ + ∥ sum (t₂ \ s) f∥ : norm_triangle_sub
+      ... < ε / 2 + ε / 2 : add_lt_add (h _ finset.disjoint_sdiff) (h _ finset.disjoint_sdiff)
+      ... = ε : add_halves _ }
+end
+
+lemma has_sum_of_has_sum_norm [normed_group α] [complete_space α] {f : ι → α}
+  (hf : has_sum (λa, norm (f a))) : has_sum f :=
+has_sum_iff_cauchy.2 $ assume ε hε,
+  let ⟨s, hs⟩ := has_sum_iff_cauchy.1 hf ε hε in
+  ⟨s, assume t ht,
+    have ∥t.sum (λa, ∥f a∥)∥ < ε := hs t ht,
+    have nn : 0 ≤ t.sum (λa, ∥f a∥) := finset.zero_le_sum (assume a _, norm_nonneg _),
+    lt_of_le_of_lt (norm_triangle_sum t f) $ by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
+
+lemma has_sum_of_absolute_convergence_real {f : ℕ → ℝ} (hf : ∀n, 0 ≤ f n) :
+  (∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (nhds r)) → has_sum f
+| ⟨r, hr⟩ :=
+  begin
+    refine has_sum_of_has_sum_norm ⟨r, (is_sum_iff_tendsto_nat_of_nonneg _ _).2 _⟩,
+    exact assume i, norm_nonneg _,
+    simpa only using hr
+  end
 
 lemma tendsto_pow_at_top_at_top_of_gt_1 {r : ℝ} (h : r > 1) : tendsto (λn:ℕ, r ^ n) at_top at_top :=
 tendsto_infi.2 $ assume p, tendsto_principal.2 $
@@ -126,7 +123,7 @@ have r + -1 ≠ 0,
 have tendsto (λn, (r ^ n - 1) * (r - 1)⁻¹) at_top (nhds ((0 - 1) * (r - 1)⁻¹)),
   from tendsto_mul
     (tendsto_sub (tendsto_pow_at_top_nhds_0_of_lt_1 h₁ h₂) tendsto_const_nhds) tendsto_const_nhds,
-(is_sum_iff_tendsto_nat_of_nonneg $ pow_nonneg h₁).mpr $
+(is_sum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr $
   by simp [neg_inv, geom_sum, div_eq_mul_inv, *] at *
 
 lemma is_sum_geometric_two (a : ℝ) : is_sum (λn:ℕ, (a / 2) / 2 ^ n) a :=

src/data/finset.lean

@@ -1571,6 +1571,9 @@ by simp only [disjoint_left, mem_union, or_imp_distrib, forall_and_distrib]
   disjoint s (t ∪ u) ↔ disjoint s t ∧ disjoint s u :=
 by simp only [disjoint_right, mem_union, or_imp_distrib, forall_and_distrib]
 
+lemma disjoint_sdiff {s t : finset α} : disjoint (t \ s) s :=
+disjoint_left.2 $ assume a ha, (mem_sdiff.1 ha).2
+
 @[simp] theorem card_disjoint_union {s t : finset α} :
     disjoint s t → card (s ∪ t) = card s + card t :=
 finset.induction_on s (λ _, by simp only [empty_union, card_empty, zero_add]) $ λ a s ha ih H,

src/measure_theory/decomposition.lean

@@ -18,6 +18,11 @@ open set lattice filter
 
 variables {α : Type*} [measurable_space α] {μ ν : measure α}
 
+-- suddenly this is necessary?!
+private lemma aux {m : ℕ} {γ d : ℝ} (h : γ - (1 / 2) ^ m < d) :
+  γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d :=
+by linarith
+
 lemma hahn_decomposition (hμ : μ univ < ⊤) (hν : ν univ < ⊤) :
   ∃s, is_measurable s ∧
     (∀t, is_measurable t → t ⊆ s → ν t ≤ μ t) ∧
@@ -116,7 +121,7 @@ begin
     { have := he₂ m,
       simp only [f],
       rw [finset.Ico.succ_singleton, finset.inf_singleton],
-      linarith },
+      exact aux this },
     { assume n (hmn : m ≤ n) ih,
       have : γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n + 1)) ≤ γ + d (f m (n + 1)),
       { calc γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n+1)) ≤

src/measure_theory/measure_space.lean

@@ -26,26 +26,6 @@ local attribute [instance] prop_decidable
 
 universes u v w x
 
-section tendsto
-variables {α : Type*} [topological_space α]
-open lattice filter
-
-lemma tendsto_at_top_supr_nat [complete_linear_order α] [orderable_topology α]
-  (f : ℕ → α) (hf : monotone f) : tendsto f at_top (nhds (⨆i, f i)) :=
-tendsto_orderable.2 $ and.intro
-  (assume a ha, let ⟨n, hn⟩ := lt_supr_iff.1 ha in
-    mem_at_top_sets.2 ⟨n, assume i hi, lt_of_lt_of_le hn (hf hi)⟩)
-  (assume a ha, univ_mem_sets' (assume n, lt_of_le_of_lt (le_supr _ n) ha))
-
-lemma tendsto_at_top_infi_nat [complete_linear_order α] [orderable_topology α]
-  (f : ℕ → α) (hf : ∀{n m}, n ≤ m → f m ≤ f n) : tendsto f at_top (nhds (⨅i, f i)) :=
-tendsto_orderable.2 $ and.intro
-  (assume a ha, univ_mem_sets' (assume n, lt_of_lt_of_le ha (infi_le _ _)))
-  (assume a ha, let ⟨n, hn⟩ := infi_lt_iff.1 ha in
-    mem_at_top_sets.2 ⟨n, assume i hi, lt_of_le_of_lt (hf hi) hn⟩)
-
-end tendsto
-
 namespace measure_theory
 
 section of_measurable

src/order/filter/basic.lean

@@ -1390,6 +1390,10 @@ lemma tendsto_at_top {α β} [preorder β] (m : α → β) (f : filter α) :
   tendsto m f at_top ↔ (∀b, {a | b ≤ m a} ∈ f.sets) :=
 by simp only [at_top, tendsto_infi, tendsto_principal]; refl
 
+theorem tendsto_at_top_principal [nonempty β] [semilattice_sup β] {f : β → α} {s : set α} :
+  tendsto f at_top (principal s) ↔ ∃N, ∀n≥N, f n ∈ s :=
+by rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_at_top_sets]; refl
+
 /-- A function `f` grows to infinity independent of an order-preserving embedding `e`. -/
 lemma tendsto_at_top_embedding {α β γ : Type*} [preorder β] [preorder γ]
   {f : α → β} {e : β → γ} {l : filter α}
@@ -1405,15 +1409,9 @@ begin
     filter_upwards [hb b] assume a ha, le_trans hc ((hm b (f a)).2 ha) }
 end
 
-lemma tendsto_at_top_at_top {α β} [preorder α] [preorder β]
-  [hα : nonempty α] (h : directed (@has_le.le α _) id)
-  (f : α → β) :
+lemma tendsto_at_top_at_top [nonempty α] [semilattice_sup α] [preorder β] (f : α → β) :
   tendsto f at_top at_top ↔ ∀ b : β, ∃ i : α, ∀ a : α, i ≤ a → b ≤ f a :=
-have directed ge (λ (a : α), principal {b : α | a ≤ b}),
-  from λ a b, let ⟨z, hz⟩ := h b a in
-    ⟨z, λ s h x hzx, h (le_trans hz.2 hzx),
-      λ s h x hzx, h (le_trans hz.1 hzx)⟩,
-by rw [tendsto_at_top, at_top, infi_sets_eq this hα]; simp
+iff.trans tendsto_infi $ forall_congr $ assume b, tendsto_at_top_principal
 
 lemma tendsto_finset_image_at_top_at_top {i : β → γ} {j : γ → β} (h : ∀x, j (i x) = x) :
   tendsto (λs:finset γ, s.image j) at_top at_top :=

src/topology/algebra/topological_structures.lean

@@ -1367,14 +1367,24 @@ begin
         infi_le_of_le (a + r) $ infi_le _ (or.inr rfl)) } }
 end
 
+lemma tendsto_at_top_supr_nat [topological_space α] [complete_linear_order α] [orderable_topology α]
+  (f : ℕ → α) (hf : monotone f) : tendsto f at_top (nhds (⨆i, f i)) :=
+tendsto_orderable.2 $ and.intro
+  (assume a ha, let ⟨n, hn⟩ := lt_supr_iff.1 ha in
+    mem_at_top_sets.2 ⟨n, assume i hi, lt_of_lt_of_le hn (hf hi)⟩)
+  (assume a ha, univ_mem_sets' (assume n, lt_of_le_of_lt (le_supr _ n) ha))
+
+lemma tendsto_at_top_infi_nat [topological_space α] [complete_linear_order α] [orderable_topology α]
+  (f : ℕ → α) (hf : ∀{n m}, n ≤ m → f m ≤ f n) : tendsto f at_top (nhds (⨅i, f i)) :=
+tendsto_orderable.2 $ and.intro
+  (assume a ha, univ_mem_sets' (assume n, lt_of_lt_of_le ha (infi_le _ _)))
+  (assume a ha, let ⟨n, hn⟩ := infi_lt_iff.1 ha in
+    mem_at_top_sets.2 ⟨n, assume i hi, lt_of_le_of_lt (hf hi) hn⟩)
+
 lemma supr_eq_of_tendsto {α} [topological_space α] [complete_linear_order α] [orderable_topology α]
-  {f : ℕ → α} {a : α} (hf : monotone f) (h : tendsto f at_top (nhds a)) : supr f = a :=
-le_antisymm
-  (supr_le $ assume i, le_of_not_gt $ assume hi,
-    have {n | i ≤ n} ∈ (at_top : filter ℕ).sets, from mem_at_top _,
-    let ⟨n, h₁, h₂⟩ := inhabited_of_mem_sets at_top_ne_bot
-      (inter_mem_sets this ((tendsto_orderable.1 h).2 _ hi)) in
-    not_lt_of_ge (hf h₁) h₂)
-  (le_of_not_gt $ assume ha,
-    let ⟨n, hn⟩ := inhabited_of_mem_sets at_top_ne_bot ((tendsto_orderable.1 h).1 _ ha) in
-    not_lt_of_ge (le_supr _ _) hn)
+  {f : ℕ → α} {a : α} (hf : monotone f) : tendsto f at_top (nhds a) → supr f = a :=
+tendsto_nhds_unique at_top_ne_bot (tendsto_at_top_supr_nat f hf)
+
+lemma infi_eq_of_tendsto {α} [topological_space α] [complete_linear_order α] [orderable_topology α]
+  {f : ℕ → α} {a : α} (hf : ∀n m, n ≤ m → f m ≤ f n) : tendsto f at_top (nhds a) → infi f = a :=
+tendsto_nhds_unique at_top_ne_bot (tendsto_at_top_infi_nat f hf)

src/topology/instances/ennreal.lean

@@ -390,14 +390,23 @@ le_antisymm
   (calc f a ≤ (⨆ (h : a = a), f a) : le_supr (λh:a=a, f a) rfl
     ... ≤ (∑b:α, ⨆ (h : a = b), f b) : ennreal.le_tsum _)
 
+lemma is_sum_iff_tendsto_nat {f : ℕ → ennreal} (r : ennreal) :
+  is_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (nhds r) :=
+begin
+  refine ⟨tendsto_sum_nat_of_is_sum, assume h, _⟩,
+  rw [← supr_eq_of_tendsto _ h, ← ennreal.tsum_eq_supr_nat],
+  { exact is_sum_tsum ennreal.has_sum },
+  { exact assume s t hst, finset.sum_le_sum_of_subset (finset.range_subset.2 hst) }
+end
+
 end tsum
 
 end ennreal
 
 namespace nnreal
 
-lemma exists_le_is_sum_of_le {f g : β → nnreal} {r : nnreal} (hgf : ∀b, g b ≤ f b) (hfr : is_sum f r) :
-  ∃p≤r, is_sum g p :=
+lemma exists_le_is_sum_of_le {f g : β → nnreal} {r : nnreal}
+  (hgf : ∀b, g b ≤ f b) (hfr : is_sum f r) : ∃p≤r, is_sum g p :=
 have (∑b, (g b : ennreal)) ≤ r,
 begin
   refine is_sum_le (assume b, _) (is_sum_tsum ennreal.has_sum) (ennreal.is_sum_coe.2 hfr),
@@ -409,16 +418,40 @@ let ⟨p, eq, hpr⟩ := ennreal.le_coe_iff.1 this in
 lemma has_sum_of_le {f g : β → nnreal} (hgf : ∀b, g b ≤ f b) : has_sum f → has_sum g
 | ⟨r, hfr⟩ := let ⟨p, _, hp⟩ := exists_le_is_sum_of_le hgf hfr in has_sum_spec hp
 
+lemma is_sum_iff_tendsto_nat {f : ℕ → nnreal} (r : nnreal) :
+  is_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (nhds r) :=
+begin
+  rw [← ennreal.is_sum_coe, ennreal.is_sum_iff_tendsto_nat],
+  simp only [ennreal.coe_finset_sum.symm],
+  exact ennreal.tendsto_coe
+end
+
 end nnreal
 
-lemma has_sum_of_nonneg_of_le {f g : β → ℝ} (hg : ∀b, 0 ≤ g b) (hgf : ∀b, g b ≤ f b) (hf : has_sum f) :
-  has_sum g :=
+lemma has_sum_of_nonneg_of_le {f g : β → ℝ}
+  (hg : ∀b, 0 ≤ g b) (hgf : ∀b, g b ≤ f b) (hf : has_sum f) : has_sum g :=
 let f' (b : β) : nnreal := ⟨f b, le_trans (hg b) (hgf b)⟩ in
 let g' (b : β) : nnreal := ⟨g b, hg b⟩ in
 have has_sum f', from nnreal.has_sum_coe.1 hf,
-have has_sum g', from nnreal.has_sum_of_le (assume b, (@nnreal.coe_le (g' b) (f' b)).2 $ hgf b) this,
+have has_sum g', from
+  nnreal.has_sum_of_le (assume b, (@nnreal.coe_le (g' b) (f' b)).2 $ hgf b) this,
 show has_sum (λb, g' b : β → ℝ), from nnreal.has_sum_coe.2 this
 
+lemma is_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} (hf : ∀i, 0 ≤ f i) (r : ℝ) :
+  is_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (nhds r) :=
+⟨tendsto_sum_nat_of_is_sum,
+  assume hfr,
+  have 0 ≤ r := ge_of_tendsto at_top_ne_bot hfr $ univ_mem_sets' $ assume i,
+    show 0 ≤ (finset.range i).sum f, from finset.zero_le_sum $ assume i _, hf i,
+  let f' (n : ℕ) : nnreal := ⟨f n, hf n⟩, r' : nnreal := ⟨r, this⟩ in
+  have f_eq : f = (λi:ℕ, (f' i : ℝ)) := rfl,
+  have r_eq : r = r' := rfl,
+  begin
+    rw [f_eq, r_eq, nnreal.is_sum_coe, nnreal.is_sum_iff_tendsto_nat, ← nnreal.tendsto_coe],
+    simp only [nnreal.sum_coe],
+    exact hfr
+  end⟩
+
 lemma infi_real_pos_eq_infi_nnreal_pos {α : Type*} [complete_lattice α] {f : ℝ → α} :
   (⨅(n:ℝ) (h : n > 0), f n) = (⨅(n:nnreal) (h : n > 0), f n) :=
 le_antisymm

src/topology/metric_space/basic.lean

@@ -374,21 +374,16 @@ let ⟨δ, δ_pos, hδ⟩ := continuous_iff.1 hf b ε hε in
 
 theorem tendsto_nhds {f : filter β} {u : β → α} {a : α} :
   tendsto u f (nhds a) ↔ ∀ ε > 0, ∃ n ∈ f.sets, ∀x ∈ n,  dist (u x) a < ε :=
-⟨λ H ε ε0, ⟨u⁻¹' (ball a ε), H (ball_mem_nhds _ ε0), by simp⟩,
- λ H s hs,
-  let ⟨ε, ε0, hε⟩ := mem_nhds_iff.1 hs, ⟨δ, δ0, hδ⟩ := H _ ε0 in
-  f.sets_of_superset δ0 (λx xδ, hε (hδ x xδ))⟩
+by simp only [metric.nhds_eq, tendsto_infi, subtype.forall, tendsto_principal, mem_ball];
+  exact forall_congr (assume ε, forall_congr (assume hε, exists_sets_subset_iff.symm))
 
 theorem continuous_iff' [topological_space β] {f : β → α} :
   continuous f ↔ ∀a (ε > 0), ∃ n ∈ (nhds a).sets, ∀b ∈ n, dist (f b) (f a) < ε :=
 continuous_iff_continuous_at.trans $ forall_congr $ λ b, tendsto_nhds
 
-theorem tendsto_at_top [inhabited β] [semilattice_sup β] {u : β → α} {a : α} :
+theorem tendsto_at_top [nonempty β] [semilattice_sup β] {u : β → α} {a : α} :
   tendsto u at_top (nhds a) ↔ ∀ε>0, ∃N, ∀n≥N, dist (u n) a < ε :=
-tendsto_nhds.trans $ ball_congr $ λ ε ε0,
-by simp; exact ⟨
-  λ ⟨s, ⟨N, hN⟩, hs⟩, ⟨N, λn hn, hs _ (hN _ hn)⟩,
-  λ ⟨N, hN⟩, ⟨{n | n ≥ N}, ⟨⟨N, by simp⟩, hN⟩⟩⟩
+by simp only [metric.nhds_eq, tendsto_infi, subtype.forall, tendsto_at_top_principal]; refl
 
 end metric
 

src/topology/uniform_space/basic.lean

@@ -546,6 +546,10 @@ lemma cauchy_iff [uniform_space α] {f : filter α} :
   cauchy f ↔ (f ≠ ⊥ ∧ (∀s∈(@uniformity α _).sets, ∃t∈f.sets, set.prod t t ⊆ s)) :=
 and_congr (iff.refl _) $ forall_congr $ assume s, forall_congr $ assume hs, mem_prod_same_iff
 
+lemma cauchy_map_iff [uniform_space α] {l : filter β} {f : β → α} :
+  cauchy (l.map f) ↔ (l ≠ ⊥ ∧ tendsto (λp:β×β, (f p.1, f p.2)) (l.prod l) uniformity) :=
+by rw [cauchy, (≠), map_eq_bot_iff, prod_map_map_eq]; refl
+
 lemma cauchy_downwards {f g : filter α} (h_c : cauchy f) (hg : g ≠ ⊥) (h_le : g ≤ f) : cauchy g :=
 ⟨hg, le_trans (filter.prod_mono h_le h_le) h_c.right⟩
 
@@ -926,6 +930,14 @@ end
 lemma complete_space_of_is_complete_univ (h : is_complete (univ : set α)) : complete_space α :=
 ⟨λ f hf, let ⟨x, _, hx⟩ := h f hf ((@principal_univ α).symm ▸ le_top) in ⟨x, hx⟩⟩
 
+lemma cauchy_iff_exists_le_nhds [uniform_space α] [complete_space α] {l : filter α} (hl : l ≠ ⊥) :
+  cauchy l ↔ (∃x, l ≤ nhds x) :=
+⟨complete_space.complete, assume ⟨x, hx⟩, cauchy_downwards cauchy_nhds hl hx⟩
+
+lemma cauchy_map_iff_exists_tendsto [uniform_space α] [complete_space α] {l : filter β} {f : β → α}
+  (hl : l ≠ ⊥) : cauchy (l.map f) ↔ (∃x, tendsto f l (nhds x)) :=
+cauchy_iff_exists_le_nhds (map_ne_bot hl)
+
 /-- A Cauchy sequence in a complete space converges -/
 theorem cauchy_seq_tendsto_of_complete [inhabited β] [semilattice_sup β] [complete_space α]
   {u : β → α} (H : cauchy_seq u) : ∃x, tendsto u at_top (nhds x) :=