diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean
index fdf4104d52..744e000923 100644
--- a/library/theories/analysis/metric_space.lean
+++ b/library/theories/analysis/metric_space.lean
@@ -5,7 +5,7 @@ Author: Jeremy Avigad
 
 Metric spaces.
 -/
-import data.real.complete data.pnat
+import data.real.complete data.pnat data.list.sort data.fin
 open nat real eq.ops classical
 
 structure metric_space [class] (M : Type) : Type :=
@@ -161,6 +161,74 @@ proposition converges_to_seq_offset_succ_iff (X : ℕ → M) (y : M) :
   ((λ n, X (succ n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
 iff.intro converges_to_seq_of_converges_to_seq_offset_succ !converges_to_seq_offset_succ
 
+section
+open list
+definition r_trans : transitive (@le ℝ _) := λ a b c, !le.trans
+definition r_refl : reflexive (@le ℝ _) := λ a, !le.refl
+
+theorem dec_prf_eq (P : Prop) (H1 H2 : decidable P) : H1 = H2 :=
+  begin
+    induction H1,
+    induction H2,
+    reflexivity,
+    apply absurd a a_1,
+    induction H2,
+    apply absurd a_1 a,
+    reflexivity
+  end
+
+-- there's a very ugly part of this proof.
+
+proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x in ℕ) :
+            ∃ K : ℝ, ∀ n : ℕ, dist (X n) x ≤ K :=
+  begin
+    cases H zero_lt_one with N HN,
+    cases em (N = 0),
+    existsi 1,
+    intro n,
+    apply le_of_lt,
+    apply HN,
+    rewrite a,
+    apply zero_le,
+    let l := map (λ n : ℕ, -dist (X n) x) (upto N),
+    have Hnenil : l ≠ nil, from (map_ne_nil_of_ne_nil _ (upto_ne_nil_of_ne_zero a)),
+    existsi max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1,
+    intro n,
+    have Hsmn : ∀ m : ℕ, m < N → dist (X m) x ≤ max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1, begin
+      intro m Hm,
+      apply le.trans,
+      rotate 1,
+      apply le_max_left,
+      note Hall := min_lemma real.le_total r_trans r_refl Hnenil,
+      have Hmem : -dist (X m) x ∈ (map (λ (n : ℕ), -dist (X n) x) (upto N)), from mem_map _ (mem_upto_of_lt Hm),
+      note Hallm' := of_mem_of_all Hmem Hall,
+      apply le_neg_of_le_neg,
+      esimp, esimp at Hallm',
+      have Heqs : (λ (a b : real), classical.prop_decidable (@le.{1} real real.real_has_le a b))
+                   =
+                   (@decidable_le.{1} real
+                     (@decidable_linear_ordered_comm_group.to_decidable_linear_order.{1} real
+                        (@decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group.{1} real
+                           (@discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring.{1} real
+                             real.discrete_linear_ordered_field)))),
+      begin
+        apply funext, intro, apply funext, intro,
+        apply dec_prf_eq
+      end,
+      rewrite -Heqs,
+      exact Hallm'
+    end,
+    cases em (n < N) with Elt Ege,
+    apply Hsmn,
+    exact Elt,
+    apply le_of_lt,
+    apply lt_of_lt_of_le,
+    apply HN,
+    apply le_of_not_gt Ege,
+    apply le_max_right
+  end
+end
+
 /- cauchy sequences -/
 
 definition cauchy (X : ℕ → M) : Prop :=
@@ -282,6 +350,24 @@ theorem cnv_real_of_cnv_nat {X : ℕ → M} {c : M} (H : ∀ n : ℕ, dist (X n)
   end
 end
 
+theorem all_conv_seqs_of_converges_to_at {f : M → N} {c : M} {l : N} (Hconv : f ⟶ l at c) :
+        ∀ X : ℕ → M, ((∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c in ℕ)) → ((λ n : ℕ, f (X n)) ⟶ l in ℕ)) :=
+   begin
+     intros X HX,
+     rewrite [↑converges_to_at at Hconv, ↑converges_to_seq],
+     intros ε Hε,
+     cases Hconv Hε with δ Hδ,
+     cases Hδ with Hδ1 Hδ2,
+     cases HX 0 with _ HXlim,
+     cases HXlim Hδ1 with N1 HN1,
+     existsi N1,
+     intro n Hn,
+     apply Hδ2,
+     split,
+     apply and.left (HX _),
+     exact HN1 Hn
+   end
+
 theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N)
   (Hseq : ∀ X : ℕ → M, ((∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c in ℕ)) → ((λ n : ℕ, f (X n)) ⟶ l in ℕ)))
   : f ⟶ l at c :=
@@ -360,7 +446,7 @@ theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N)
 
 definition continuous (f : M → N) : Prop := ∀ x, continuous_at f x
 
-theorem converges_seq_of_comp [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N}
+theorem converges_seq_comp_of_converges_seq_of_cts [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N}
                                          (Hf : continuous f) :
         converges_seq (λ n, f (X n)) :=
   begin
diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean
index 8ea6b3f079..26eb5aa1da 100644
--- a/library/theories/analysis/real_limit.lean
+++ b/library/theories/analysis/real_limit.lean
@@ -263,6 +263,141 @@ proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) :
 have (λ n, X n * c) = (λ n, c * X n), from funext (take x, !mul.comm),
 by+ rewrite [this, mul.comm]; apply mul_left_converges_to_seq c HX
 
+protected lemma add_half_quarter {a : ℝ} (H : a > 0) : a / 2 + a / 4 < a :=
+  begin
+    replace (4 : ℝ) with (2 : ℝ) + 2,
+    have Hne : (2 + 2 : ℝ) ≠ 0, from ne_of_gt four_pos,
+    krewrite (div_add_div _ _ two_ne_zero Hne),
+    have Hnum : (2 + 2 + 2) / (2 * (2 + 2)) = (3 : ℝ) / 4, by norm_num,
+    rewrite [{2 * a}mul.comm, -left_distrib, mul_div_assoc, -mul_one a at {2}], krewrite Hnum,
+    apply mul_lt_mul_of_pos_left,
+    apply div_lt_of_mul_lt_of_pos,
+    apply four_pos,
+    rewrite one_mul,
+    replace (3 : ℝ) with (2 : ℝ) + 1,
+    replace (4 : ℝ) with (2 : ℝ) + 2,
+    apply add_lt_add_left,
+    apply two_gt_one,
+    exact H
+  end
+
+theorem converges_to_seq_squeeze (HX : X ⟶ x in ℕ) (HY : Y ⟶ x in ℕ) {Z : ℕ → ℝ} (HZX : ∀ n, X n ≤ Z n)
+        (HZY : ∀ n, Z n ≤ Y n) : Z ⟶ x in ℕ :=
+  begin
+    intros ε Hε,
+    have Hε4 : ε / 4 > 0, from div_pos_of_pos_of_pos Hε four_pos,
+    cases HX Hε4 with N1 HN1,
+    cases HY Hε4 with N2 HN2,
+    existsi max N1 N2,
+    intro n Hn,
+    have HXY : abs (Y n - X n) < ε / 2, begin
+      apply lt_of_le_of_lt,
+      apply abs_sub_le _ x,
+      have Hε24 : ε / 2 = ε / 4 + ε / 4, from eq.symm !add_quarters,
+      rewrite Hε24,
+      apply add_lt_add,
+      apply HN2,
+      apply ge.trans Hn !le_max_right,
+      rewrite abs_sub,
+      apply HN1,
+      apply ge.trans Hn !le_max_left
+    end,
+    have HZX : abs (Z n - X n) < ε / 2, begin
+      have HZXnp : Z n - X n ≥ 0, from sub_nonneg_of_le !HZX,
+      have HXYnp : Y n - X n ≥ 0, from sub_nonneg_of_le (le.trans !HZX !HZY),
+      rewrite [abs_of_nonneg HZXnp, abs_of_nonneg HXYnp at HXY],
+      note Hgt := lt_add_of_sub_lt_right HXY,
+      have Hlt : Z n < ε / 2 + X n, from calc
+        Z n ≤ Y n : HZY
+        ... < ε / 2 + X n : Hgt,
+      apply sub_lt_right_of_lt_add Hlt
+    end,
+    have H : abs (Z n - x) < ε, begin
+      apply lt_of_le_of_lt,
+      apply abs_sub_le _ (X n),
+      apply lt.trans,
+      apply add_lt_add,
+      apply HZX,
+      apply HN1,
+      apply ge.trans Hn !le_max_left,
+      apply add_half_quarter Hε
+    end,
+    exact H
+  end
+
+proposition converges_to_seq_of_abs_sub_converges_to_seq (Habs : (λ n, abs (X n - x)) ⟶ 0 in ℕ) :
+            X ⟶ x in ℕ :=
+  begin
+    intros ε Hε,
+    cases Habs Hε with N HN,
+    existsi N,
+    intro n Hn,
+    have Hn' : abs (abs (X n - x) - 0) < ε, from HN Hn,
+    rewrite [sub_zero at Hn', abs_abs at Hn'],
+    exact Hn'
+  end
+
+proposition abs_sub_converges_to_seq_of_converges_to_seq (HX : X ⟶ x in ℕ) :
+            (λ n, abs (X n - x)) ⟶ 0 in ℕ :=
+  begin
+    intros ε Hε,
+    cases HX Hε with N HN,
+    existsi N,
+    intro n Hn,
+    have Hn' : abs (abs (X n - x) - 0) < ε, by rewrite [sub_zero, abs_abs]; apply HN Hn,
+    exact Hn'
+  end
+
+proposition mul_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) :
+            (λ n, X n * Y n) ⟶ x * y in ℕ :=
+  begin
+    have Hbd : ∃ K : ℝ, ∀ n : ℕ, abs (X n) ≤ K, begin
+      cases bounded_of_converges_seq HX with K HK,
+      existsi K + abs x,
+      intro n,
+      note Habs := le.trans (abs_abs_sub_abs_le_abs_sub (X n) x) !HK,
+      apply le_add_of_sub_right_le,
+      apply le.trans,
+      apply le_abs_self,
+      assumption
+    end,
+    cases Hbd with K HK,
+    have Habsle : ∀ n, abs (X n * Y n - x * y) ≤ K * abs (Y n - y) + abs y * abs (X n - x), begin
+      intro,
+      have Heq : X n * Y n - x * y = (X n * Y n - X n * y) + (X n * y - x * y), by
+        rewrite [-sub_add_cancel (X n * Y n) (X n * y) at {1}, sub_eq_add_neg, *add.assoc],
+      apply le.trans,
+      rewrite Heq,
+      apply abs_add_le_abs_add_abs,
+      apply add_le_add,
+      rewrite [-mul_sub_left_distrib, abs_mul],
+      apply mul_le_mul_of_nonneg_right,
+      apply HK,
+      apply abs_nonneg,
+      rewrite [-mul_sub_right_distrib, abs_mul, mul.comm],
+      apply le.refl
+    end,
+    have Hdifflim : (λ n, abs (X n * Y n - x * y)) ⟶ 0 in ℕ, begin
+      apply converges_to_seq_squeeze,
+      rotate 2,
+      intro, apply abs_nonneg,
+      apply Habsle,
+      apply converges_to_seq_constant,
+      rewrite -{0}zero_add,
+      apply add_converges_to_seq,
+      rewrite -(mul_zero K),
+      apply mul_left_converges_to_seq,
+      apply abs_sub_converges_to_seq_of_converges_to_seq,
+      exact HY,
+      rewrite -(mul_zero (abs y)),
+      apply mul_left_converges_to_seq,
+      apply abs_sub_converges_to_seq_of_converges_to_seq,
+      exact HX
+    end,
+    apply converges_to_seq_of_abs_sub_converges_to_seq,
+    apply Hdifflim
+  end
+
 -- TODO: converges_to_seq_div, converges_to_seq_mul_left_iff, etc.
 
 proposition abs_converges_to_seq_zero (HX : X ⟶ 0 in ℕ) : (λ n, abs (X n)) ⟶ 0 in ℕ :=
@@ -280,6 +415,25 @@ iff.intro converges_to_seq_zero_of_abs_converges_to_seq_zero abs_converges_to_se
 
 end limit_operations
 
+/- properties of converges_to_at -/
+
+section limit_operations_continuous
+variables {f g : ℝ → ℝ}
+variables {a b x y : ℝ}
+
+theorem mul_converges_to_at (Hf : f ⟶ a at x) (Hg : g ⟶ b at x) : (λ z, f z * g z) ⟶ a * b at x :=
+  begin
+    apply converges_to_at_of_all_conv_seqs,
+    intro X HX,
+    apply mul_converges_to_seq,
+    note Hfc := all_conv_seqs_of_converges_to_at Hf,
+    apply Hfc _ HX,
+    note Hgb := all_conv_seqs_of_converges_to_at Hg,
+    apply Hgb _ HX
+  end
+
+end limit_operations_continuous
+
 /- monotone sequences -/
 
 section monotone_sequences
@@ -487,6 +641,17 @@ theorem continuous_offset_of_continuous {f : ℝ → ℝ} (Hcon : continuous f)
     assumption
   end
 
+theorem continuous_mul_of_continuous {f g : ℝ → ℝ} (Hconf : continuous f) (Hcong : continuous g) :
+        continuous (λ x, f x * g x) :=
+  begin
+    intro x,
+    apply continuous_at_of_converges_to_at,
+    apply mul_converges_to_at,
+    all_goals apply converges_to_at_of_continuous_at,
+    apply Hconf,
+    apply Hcong
+  end
+
 end continuous
 
 /-