diff --git a/leanpkg.toml b/leanpkg.toml
index e9d40e1..b3f2c42 100644
--- a/leanpkg.toml
+++ b/leanpkg.toml
@@ -5,4 +5,4 @@ lean_version = "leanprover-community/lean:3.7.2"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "ecdb13831d4671eb304c41e78adb5b280c2fc365"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "3d60e1344d5d3126c5a2adfe0da132fdebd6e60a"}
diff --git a/src/metric_space/metric_space_Lahfa.lean b/src/metric_space/metric_space_Lahfa.lean
new file mode 100644
index 0000000..825429a
--- /dev/null
+++ b/src/metric_space/metric_space_Lahfa.lean
@@ -0,0 +1,96 @@
+import data.set
+import data.set.finite
+import data.real.basic
+import data.finset
+import order.conditionally_complete_lattice
+
+noncomputable theory
+open_locale classical
+open set
+
+class metric_space (X : Type) :=
+(d : X → X → ℝ)
+(d_pos : ∀ x y, d x y ≥ 0)
+(presep : ∀ x y, x = y → d x y = 0)
+(sep : ∀ x y, d x y = 0 →  x = y)
+(sym : ∀ x y, d x y = d y x)
+(triangle : ∀ x y z, d x z ≤ d x y + d y z)
+
+variables {X:Type} [metric_space X]
+
+open metric_space
+
+instance real.metric_space : metric_space ℝ :=
+{ d                  := λx y, abs (x - y),
+  d_pos              := by simp [abs_nonneg],
+  presep             := begin simp, apply sub_eq_zero_of_eq end,
+  sep                := begin simp, apply eq_of_sub_eq_zero end,
+  sym                := assume x y, abs_sub _ _,
+  triangle           := assume x y z, abs_sub_le _ _ _ }
+
+theorem real.dist_eq (x y : ℝ) : d x y = abs (x - y) := rfl
+
+theorem real.dist_0_eq_abs (x : ℝ) : d x 0 = abs x :=
+by simp [real.dist_eq]
+
+def converge (x: ℕ → X) (l : X) :=
+  ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n))  < ε)
+
+lemma real.sup_sub_lt_eps {S: set ℝ}: ∀ ε > 0, ∃ x ∈ S, Sup S - x < ε := sorry
+lemma real.sup_dist_lt_eps {S: set ℝ}: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := begin
+  intros ε hε,
+  obtain ⟨ x, hx, hs_lt ⟩ := real.sup_sub_lt_eps ε hε,
+  use x,
+  split,
+  exact hx,
+  rw real.dist_eq,
+  apply abs_lt_of_lt_of_neg_lt,
+  exact hs_lt,
+  sorry,
+end
+
+lemma converge_of_dist_lt_one_div_succ {x: ℕ → ℝ} {l: ℝ}: (∀ n, d l (x n) ≤ 1 / (n + 1)) → converge x l := begin
+intro H,
+intros ε hε,
+obtain ⟨ N, hN ⟩ := exists_nat_one_div_lt hε,
+use N,
+intros n hn,
+calc d l (x n) ≤ 1 / (n + 1) : H n
+    ... ≤ 1 / (N + 1) : nat.one_div_le_one_div hn
+    ... < ε : hN
+end
+
+lemma sup_is_a_cv_seq (S: set ℝ):
+  S.nonempty → bdd_above S → ∃ (x: ℕ → ℝ), (∀ n, x n ∈ S) ∧ converge x (Sup S) := begin
+  intros hnn hbdd,
+  have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x < 1/(N + 1) := begin
+  intro N,
+  apply real.sup_dist_lt_eps,
+  apply nat.one_div_pos_of_nat,
+  end,
+  choose x hrange h using this,
+  use x,
+  split,
+  exact hrange,
+  exact converge_of_dist_lt_one_div_succ h, -- this line should work (?)
+  end
+
+#exit
+But, I have some issue regarding the types, here is the state at the last step:
+
+type mismatch at application
+  converge_of_dist_lt_one_div_succ h
+term
+  h
+has type
+  ∀ (N : ℕ), d (Sup S) (x N) < 1 / (↑N + 1)
+but is expected to have type
+  ∀ (n : ℕ), d (Sup S) (x n) ≤ 1 / (↑n + 1)
+state:
+S : set ℝ,
+hnn : set.nonempty S,
+hbdd : bdd_above S,
+x : ℕ → ℝ,
+hrange : ∀ (N : ℕ), x N ∈ S,
+h : ∀ (N : ℕ), d (Sup S) (x N) < 1 / (↑N + 1)
+⊢ converge x (Sup S)
diff --git a/src/metric_space/metric_space_tutorial.lean b/src/metric_space/metric_space_tutorial.lean
new file mode 100644
index 0000000..9aeedbf
--- /dev/null
+++ b/src/metric_space/metric_space_tutorial.lean
@@ -0,0 +1,256 @@
+--import data.set
+--import data.set.finite
+import data.real.basic
+--import data.finset
+--import order.conditionally_complete_lattice
+import topology.opens -- remove when finished checking types of things.
+-- note: we don't import topology.metric_space.basic, which is
+-- mathlib's version of metric spaces
+
+/-! -/
+--open_locale classical
+
+open set
+
+
+/-- A metric space is a set/type X equipped with a real-valued distance function
+    satisfying the usual axioms -/
+class metric_space (X : Type) :=
+(dist : X → X → ℝ)
+(dist_self : ∀ x : X, dist x x = 0)
+(eq_of_dist_eq_zero : ∀ {x y : X}, dist x y = 0 → x = y)
+(dist_comm : ∀ x y : X, dist x y = dist y x)
+(dist_triangle : ∀ x y z : X, dist x z ≤ dist x y + dist y z)
+
+-- Exercise: compare with the definition in all the maths books.
+-- Did we leave something out?
+
+-- theorems that we are about to prove about metric spaces go in the metric space namespace
+namespace metric_space
+
+-- let X be a metric space
+variables {X : Type} [metric_space X]
+
+/-! # Learning to use `linarith`
+
+We left out the axiom that ∀ x y : X, dist x y ≥ 0 in our metric space,
+because it can be deduced from the triangle inequality and symmetry!
+Let's prove it now, using `linarith`. The `linarith` tactic proves
+many "obvious" results involving inequalities as long as the expressions
+involved have degree 1. It looks at the hypotheses and tries to prove
+the goal. For example if `h : 0 ≤ a + a` is a hypothesis, and the goal
+is `⊢ 0 ≤ a`, then `linarith` will close the goal.
+
+Other useful tactics :
+
+`have h := dist_triangle x y x` will create a new hypothesis `h`.
+
+`push_neg` will move `¬` as far to the right as it can, and possibly
+remove it. For example if `h : ¬ (a ≤ b)` then `push_neg at h` will change `h` to `b < a`.
+
+`by_contra h` will create a hypothesis `h` saying that the goal is false, and
+will replace the goal with `false`. Note that `linarith` can even prove a goal `false` if
+the hypotheses are contradictory.
+
+Let's prove some basic things about distances using `linarith`.
+
+-/
+
+theorem dist_nonneg : ∀ (x y : X), 0 ≤ dist x y :=
+begin
+  --replace with sorry in tutorial
+  intros x y,
+  have h := dist_triangle x y x,
+  rw dist_self at h,
+  rw dist_comm y x at h,
+  linarith,
+end
+
+theorem dist_le_zero {x y : X} : dist x y ≤ 0 ↔ x = y :=
+begin
+  --replace with sorry in tutorial
+  split,
+  { intro h,
+    have h2 := dist_nonneg x y,
+    apply eq_of_dist_eq_zero,
+    linarith,
+  },
+  { intro h,
+    rw h,
+    rw dist_self,
+  }
+end
+
+theorem dist_pos {x y : X} : 0 < dist x y ↔ x ≠ y :=
+begin
+  --replace with sorry in tutorial
+  split,
+  { intro h,
+    intro hxy,
+    rw ←dist_le_zero at hxy,
+    linarith,
+  },
+  { intro h,
+    by_contra h2,
+    push_neg at h2,
+    rw dist_le_zero at h2,
+    contradiction,
+
+  }
+end
+
+/-! ### Open balls
+
+We define `ball x ε` to be the open ball centre `x` and radius `ε`. Note that we do not
+require `ε > 0`! That hypothesis shows up later in the theorems, not in the definition.
+
+
+-/
+
+variables {x y z : X} {ε ε₁ ε₂ : ℝ} {s : set X}
+
+/-- `ball x ε` is the set of all points `y` with `dist y x < ε` -/
+def ball (x : X) (ε : ℝ) : set X := {y | dist y x < ε}
+
+-- Let's tag this lemma with the `simp` tag, so the `simp` tactic will use it.
+@[simp] theorem mem_ball : y ∈ ball x ε ↔ dist y x < ε := iff.rfl -- true by definition
+
+-- Now we get this proof for free:
+theorem mem_ball_comm : x ∈ ball y ε ↔ y ∈ ball x ε :=
+begin
+  simp [dist_comm]
+end
+
+-- Let's tag `dist_self` with the `simp` tag too:
+
+attribute [simp] dist_self
+
+-- Can you find a proof of this? And then can you find a one-line proof using `simp`?
+theorem mem_ball_self (h : 0 < ε) : x ∈ ball x ε :=
+begin
+  --replace with sorry
+  rw mem_ball,
+  rw dist_self,
+  exact h,
+end
+
+/- Top tip: `rw mem_ball at hy ⊢` will rewrite `mem_ball` at both the hypothesis `hy` and the goal.
+  Get `⊢` in VS Code with `\|-`
+
+-/
+theorem ball_mono (h : ε₁ ≤ ε₂) : ball x ε₁ ⊆ ball x ε₂ :=
+begin
+  -- delete me
+  intros y hy,
+  rw mem_ball at hy ⊢,
+  linarith,
+end
+
+
+/-! # Open sets.
+
+A subset of a metric space is open if for every element `s` in the subset, there's some open
+ball `ball s ε`, with ε > 0, entirely contained with `S`.
+-/
+
+/-- A subset U of a metric space is open if every s ∈ U there's an open ball centre s within U -/
+def is_open (U : set X) := ∀ s ∈ U, ∃ (ε : ℝ) (hε : 0 < ε), ball s ε ⊆ U
+
+-- Note that `is_open` is a Proposition. Things like `is_open_Union` below are proofs.
+
+-- Let's start with two easy facts about open sets -- the empty set and the whole space is open.
+theorem is_open_empty : is_open (∅ : set X) :=
+begin
+  intro x,
+  intro hx,
+  cases hx,-- too hard for a beginner. Need to get a contradiction from `h : x ∈ ∅`
+end
+
+theorem is_open_univ : is_open (univ : set X) :=
+begin
+  intro x,
+  intro hx,
+  use 37,
+  split,
+    norm_num,
+  -- need subset_univ
+  simp,
+end
+
+-- An arbitrary union of open sets is open. The union is indexed over an auxiliary type ι
+
+-- TODO: I don't think this is any good, people need to know about set.subset.trans,
+-- set.subset.Union etc. Should do something on sets first?
+
+theorem is_open_Union (ι : Type) (f : ι → set X) (hf : ∀ (i : ι), is_open (f i)) :
+  is_open (⋃ (i : ι), f i) :=
+begin
+  intro x,
+  intro hx,
+  rcases hx with ⟨U, ⟨i, rfl⟩, hxU⟩,
+  have h := hf i x hxU,
+  rcases h with ⟨ε, hε, hxε⟩,
+  use ε,
+  split, use hε,
+  refine set.subset.trans hxε _,
+  apply set.subset_Union,
+end
+
+theorem is_open_inter {U V : set X}  (hU : is_open U) (hV : is_open V) : is_open (U ∩ V) := sorry
+
+
+
+
+/- A subset S of a metric space is closed if its complement is open -/
+def is_closed (S : set X) := is_open (-S)
+
+end metric_space
+
+#exit
+
+-- the lemmas from 274 to 300:
+theorem closed_ball_subset_closed_ball {α : Type u} [metric_space α] {ε₁ ε₂ : ℝ} {x : α} (h : ε₁ ≤ ε₂) :
+  closed_ball x ε₁ ⊆ closed_ball x ε₂ :=
+λ y (yx : _ ≤ ε₁), le_trans yx h
+
+theorem ball_disjoint (h : ε₁ + ε₂ ≤ dist x y) : ball x ε₁ ∩ ball y ε₂ = ∅ :=
+eq_empty_iff_forall_not_mem.2 $ λ z ⟨h₁, h₂⟩,
+not_lt_of_le (dist_triangle_left x y z)
+  (lt_of_lt_of_le (add_lt_add h₁ h₂) h)
+
+theorem ball_disjoint_same (h : ε ≤ dist x y / 2) : ball x ε ∩ ball y ε = ∅ :=
+ball_disjoint $ by rwa [← two_mul, ← le_div_iff' two_pos]
+
+theorem ball_subset (h : dist x y ≤ ε₂ - ε₁) : ball x ε₁ ⊆ ball y ε₂ :=
+λ z zx, by rw ← add_sub_cancel'_right ε₁ ε₂; exact
+lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h)
+
+theorem ball_half_subset (y) (h : y ∈ ball x (ε / 2)) : ball y (ε / 2) ⊆ ball x ε :=
+ball_subset $ by rw sub_self_div_two; exact le_of_lt h
+
+theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε :=
+⟨_, sub_pos.2 h, ball_subset $ by rw sub_sub_self⟩
+
+theorem ball_eq_empty_iff_nonpos : ε ≤ 0 ↔ ball x ε = ∅ :=
+(eq_empty_iff_forall_not_mem.trans
+⟨λ h, le_of_not_gt $ λ ε0, h _ $ mem_ball_self ε0,
+ λ ε0 y h, not_lt_of_le ε0 $ pos_of_mem_ball h⟩).symm
+
+@[simp] lemma ball_zero : ball x 0 = ∅ :=
+by rw [← metric.ball_eq_empty_iff_nonpos]
+
+--
+
+-- Do we want this?
+theorem eq_of_forall_dist_le {x y : α} (h : ∀ε, ε > 0 → dist x y ≤ ε) : x = y :=
+eq_of_dist_eq_zero (eq_of_le_of_forall_le_of_dense dist_nonneg h)
+
+/-- The triangle (polygon) inequality for sequences of points; `finset.range` version. -/
+lemma dist_le_range_sum_dist (f : ℕ → α) (n : ℕ) :
+  dist (f 0) (f n) ≤ (finset.range n).sum (λ i, dist (f i) (f (i + 1))) :=
+finset.Ico.zero_bot n ▸ dist_le_Ico_sum_dist f (nat.zero_le n)
+
+-- From mathlib
+https://github.com/leanprover-community/mathlib/blob/17632202cdf9682cea972e86437d32ac20c91b06/src/topology/basic.lean#L262-L319
+
+def closure (s : set α) : set α := ⋂₀ {t | is_closed t ∧ s ⊆ t}
diff --git a/src/metric_space/metricspace_Jason.lean b/src/metric_space/metricspace_Jason.lean
new file mode 100644
index 0000000..eb21ea5
--- /dev/null
+++ b/src/metric_space/metricspace_Jason.lean
@@ -0,0 +1,81 @@
+import tactic
+import topology.metric_space.basic
+variables {X : Type*} [metric_space X]
+variables {Y : Type*} [metric_space Y]
+
+/-- Jason KY effort -/
+/- Definition of an open ball -/
+def open_ball (x₀ : X) (r : ℝ) := {x : X | dist x₀ x < r}
+
+/- Definition of being open -/
+def is_open' (S : set X) := ∀ s ∈ S, ∃ (ε : ℝ) (hε : 0 < ε), open_ball s ε ⊆ S
+
+/- Definition of being closed -/
+def is_closed' (S : set X) := is_open' $ -S
+
+/- Definition of the set of limit points -/
+def limit_points (S : set X) :=
+    {x : X | ∀ (ε : ℝ) (hε : 0 < ε), ∃ (y ∈ S) (x ≠ y), y ∈ open_ball x ε}
+
+/- Definition of closure -/
+def closure' (S : set X) := ⋂ (T : set X) (h₀ : S ⊆ T) (h₁ : is_closed' T), T
+
+attribute [reducible] open_ball is_open' is_closed'
+limit_points
+
+/- Defining the structure of a closed set -/
+structure closed_set (X : Type*) [metric_space X] :=
+(carrier : set X)
+(is_closed : is_closed' carrier)
+
+instance : has_coe (closed_set X) (set X) := ⟨closed_set.carrier⟩
+instance : has_le (closed_set X) := ⟨λ α β, (α : set X) ⊆ (β : set X)⟩
+instance : has_lt (closed_set X) := ⟨λ α β, (α : set X) ⊂ (β : set X)⟩
+
+theorem ext' {S T : closed_set X} (h : (S : set X) = T) : S = T :=
+by cases S; cases T; congr'
+
+open set
+
+def Closure (S : set X) : closed_set X :=
+{ carrier := closure' S,
+  is_closed := sorry }
+
+/- The closure of a closed_set is itself -/
+lemma Closure_self (T : closed_set X) : T = Closure T.1 := sorry
+
+instance : partial_order (closed_set X) :=
+{.. partial_order.lift (coe : closed_set X → set X) (λ a b, ext') (by apply_instance)}
+
+/- The closure of a closed_set is itself -/
+lemma Closure_self' (T : closed_set X) : T = Closure T.1 := sorry
+
+/- A set is smaller than its closure -/
+theorem subset_closure' (S : set X) : S ⊆ closure' S :=
+set.subset_Inter $ λ _, set.subset_Inter $ λ h, set.subset_Inter $ λ _, h
+
+/- The closure of a smaller set is smaller than closure -/
+theorem closure_mono' {S T : set X} (h : S ⊆ T) : closure' S ⊆ closure' T := sorry
+
+/- Closed sets form a Galois insertion -/
+def gi : @galois_insertion (set X) (closed_set X) _ _ Closure closed_set.carrier :=
+{ choice := λ S h, Closure S,
+  gc := λ S T,
+    ⟨λ h, set.subset.trans (subset_closure' S) h, λ h, by rw Closure_self T; from closure_mono' h⟩,
+  le_l_u := λ S, subset_closure' S,
+  choice_eq := λ _ _, rfl }
+
+/- Closed sets form a complete lattice -/
+instance : complete_lattice (closed_set X) :=
+{ .. galois_insertion.lift_complete_lattice gi}
+
+--set_option pp.notation false
+example (A B : closed_set X) : A ⊔ B = A ⊓ B :=
+begin
+  show Closure (A.carrier ∪ B.carrier) = Closure (A.carrier ∩ B.carrier),
+  sorry
+end
+
+
+#print galois_insertion.lift_complete_lattice
+#print complete_lattice.sup
diff --git a/src/metric_space/metricspacetao.lean b/src/metric_space/metricspacetao.lean
new file mode 100644
index 0000000..e7912f4
--- /dev/null
+++ b/src/metric_space/metricspacetao.lean
@@ -0,0 +1,128 @@
+import data.real.basic
+import data.set
+import analysis.normed_space.basic
+
+/- Kevin Doran effort -/
+-- Q0. Notation for absolute. Should I reuse this from somewhere in Lean or mathlib?
+local notation `|`x`|` := abs x
+
+def is_adherent (x : ℝ) (X : set ℝ) : Prop :=
+∀ ε > 0, ∃y ∈ X, |x - y| ≤ ε
+
+infix `is_adherent_to` :55 := is_adherent
+
+def closure' (X : set ℝ) : set ℝ :=
+{x : ℝ | x is_adherent_to X }
+
+-- closure_mono term proof
+
+/-- If $$X\subseteq Y$$ then $$\overline{X}\subseteq\overline{Y}$$ -/
+theorem closure'_mono {X Y : set ℝ} (hXY : X ⊆ Y) : closure' X ⊆ closure' Y :=
+λ a haX ε hε, let ⟨x, haX', h⟩ := haX ε hε in ⟨x, hXY haX', h⟩
+
+-- closure_mono tactic proof
+example {X Y : set ℝ} (hXY : X ⊆ Y) : closure' X ⊆ closure' Y :=
+begin
+  -- Say a is in the closure of X. We want to show a is in the closure of Y.
+  -- So say ε > 0. We want to find y ∈ Y such that |a - y| ≤ ε.
+  intros a haX ε hε,
+  -- By definition of closure of X, there's x ∈ X with |a - x| ≤ ε.
+  rcases haX ε hε with ⟨x, haX', h⟩,
+  -- So let y be x.
+  use x,
+  -- Remark:
+  split,
+  { -- x is in Y because it's in X and X ⊆ Y
+    exact hXY haX', -- hXY is actually a function!
+  },
+  -- oh but now one of our assumptions is the conclusion
+  assumption
+end
+
+-- subset_closure term proof
+
+/-- For all subsets $$X$$ of $$\mathbb{R}$$, we have $$X\subseteq\overline{X}$$ -/
+lemma subset_closure' {X : set ℝ} : X ⊆ closure' X :=
+λ x hx ε hε, ⟨x, hx, le_of_lt (by rwa [sub_self, abs_zero])⟩
+
+-- tactic proof
+
+example {X : set ℝ} : X ⊆ closure' X :=
+begin
+  -- Say x ∈ X and ε > 0.
+  intros x hx ε hε,
+  -- We need to find y ∈ X with |x - y| ≤ ε. Just use x.
+  use x,
+  -- Remark: x ∈ X
+  split, exact hx,
+  -- Note also that |x - x| is obviously zero
+  simp,
+  -- and because ε > 0 we're done
+  exact le_of_lt hε
+  -- Note that that last bit would have been better if your definition of closure'
+  -- had used < and not ≤
+end
+
+-- closure_closure
+
+-- Note: for some reason this is not formalaised as `closure ∘ closure = closure`
+-- I don't know why we have this convention
+
+-- tactic mode proof
+
+/-- The closure of $$\overline{X}$$ is $$\overline{X}$$ again -/
+lemma closure'_closure' (X : set ℝ) : closure' (closure' X) = closure' X := --
+begin
+  -- We prove inclusions in both directions
+  ext a,
+  split,
+  --
+  { -- ⊆ : say $$a$$ is in the closure of $$\overline{X}$$.
+    intro ha,
+    -- We want to show it's in $$\overline{X}$$ so say ε > 0, and we want x with |x-a| ≤ ε
+    intros ε hε,
+    -- By definition of a, there's some elements $$b\in\overline{X}$$
+    -- with |a - b| ≤ ε/2
+    rcases ha (ε/2) (by linarith) with ⟨b, hb, hab⟩,
+    -- and by definition of b there's some x ∈ X with |b - x| ≤ ε/2
+    rcases hb (ε/2) (by linarith) with ⟨x, hx, hbx⟩,
+    -- Let's use this x
+    use x,
+    -- Note it's obviously in X
+    split, exact hx,
+    -- and now |a - x| = |(a - b) + (b - x)|
+    calc |a - x| = |(a - b) + (b - x)| : by ring
+                   -- ≤ ε/2 + ε/2 = ε
+    ...          ≤ |a - b| + |b - x|   : by apply abs_add
+    ...          ≤ ε : by linarith
+  },
+  { -- ⊇ : follows immediately from subset_closure'
+    intro h, apply subset_closure' h,
+  }
+end
+
+-- closure_squeeze term mode proof
+lemma closure'_squeeze {X Y : set ℝ} (h₁ : X ⊆ Y) (h₂ : Y ⊆ closure'(X)) :
+  closure'(X) = closure'(Y) :=
+set.subset.antisymm (closure'_mono h₁) $ by rw ←closure'_closure' X; apply closure'_mono h₂
+
+-- tactic mode proof
+example {X Y : set ℝ} (h₁ : X ⊆ Y) (h₂ : Y ⊆ closure'(X)) :
+  closure'(X) = closure'(Y) :=
+begin
+  -- We prove inclusions in both directions
+  apply set.subset.antisymm,
+  { -- ⊆ is just closure'_mono
+    apply closure'_mono h₁},
+  { -- ⊇ -- first use closure'_closure'
+    rw ←closure'_closure' X,
+    -- and then it follows from closure'_mono
+    apply closure'_mono h₂},
+end
+
+lemma closure_monotone : monotone closure' :=
+λ X Y H a ha ε hε, let ⟨p, hpx, hapε⟩ := ha ε hε in ⟨p, H hpx, hapε⟩
+
+lemma closure_inter_subset_inter_closure' (X Y : set ℝ) :
+closure' (X ∩ Y) ⊆ closure' X ∩ closure' Y :=
+(closure_monotone).map_inf_le _ _
diff --git a/src/metric_space/tactics1.md b/src/metric_space/tactics1.md
new file mode 100644
index 0000000..503e592
--- /dev/null
+++ b/src/metric_space/tactics1.md
@@ -0,0 +1,415 @@
+Tactics
+=======
+
+exact
+-----
+
+`exact H` : This tactic will close a goal equal to the type of `H`.
+
+Example 1:
+
+```
+H : x = y + 1
+⊢ x = y + 1
+```
+The `exact H` tactic will close that goal.
+
+Example 2:
+```
+H : a + r = b + r → a = b
+⊢ a + r = b + r → a = b
+```
+
+The tactic `exact H` will close that goal.
+
+Example 3:
+
+```
+⊢ succ a ≠ 0
+```
+
+The tactic `exact zero_ne_succ a` will close that goal, because `zero_ne_succ a` is a proof that `succ a ≠ 0`.
+
+assumption
+----------
+
+This tactic is a variant of `exact`, which closes any goal for which there is already a proof in our assumptions. For example if the assumptions and goal look like this:
+
+```
+H : x = y + 1
+⊢ x = y + 1
+```
+
+then the `assumption` tactic will close this goal.
+
+refl
+----
+
+The `refl` tactic will close any goal of the form `a = a`, and more generally any goal of the form `x R x` if `R` is a binary relation which is reflexive.
+
+induction
+----------
+
+`induction n with d hd`
+
+Does induction on `n`. Assumes that `n` is the kind of thing you can do induction on (for example `n : mynat` would be a great example).
+
+Running the tactic `induction a with d hd` changes the goal from
+```
+1 goal
+P : mynat → Prop,
+n : mynat
+⊢ P n
+```
+
+to
+
+```
+2 goals
+case mynat.zero
+P : mynat → Prop
+⊢ P 0
+case mynat.succ
+P : mynat → Prop,
+d : mynat,
+hd : P d
+⊢ P (succ d)
+```
+
+Example:
+
+`induction n with d Hd,`
+
+takes
+
+```
+1 goal
+n : mynat
+⊢ 0 + n = n
+```
+
+to
+
+```
+2 goals
+case mynat.zero
+⊢ 0 + 0 = 0
+case mynat.succ
+d : mynat,
+Hd : 0 + d = d
+⊢ 0 + succ d = succ d
+```
+
+cases
+-----
+
+A "weaker" variant of induction, where we do not get an inductive hypothesis; the `cases a with b` tactic simply changes a general `a : mynat` into the two cases `a = 0` and `a = succ b`.
+
+rw
+---
+
+Does a "rewrite". If `H : a = b` then `rw H` changes all `a`'s in the goal to `b`'s. Note that in contrast to core Lean, 
+the natural number game's `rw` does not try to close the goal with `refl`.
+If you want Lean 3.4.2's `rw`, use `rewrite`.
+
+Variant: if you want to change all `b`'s to `a`'s then `rw ←H` works (use `\l` to get the left arrow)
+
+Variant: if you want to change all `a`'s to `b`'s in hypothesis `H2` then `rw H at H2` works.
+
+The tactic also works with true/false statements; it will rewrite "iff"s. For example `le_def a b : a ≤ b ↔ ∃ (c : mynat), b = a + c`, so `rw le_def` will change `a ≤ b` to `∃ (c : mynat), b = a + c`.
+
+
+
+Example:
+```
+H : a = b + 3
+⊢ 0 + a = a + b
+```
+
+Then `rw H` changes the goal to
+
+```
+⊢ 0 + (b + 3) = b + 3 + b
+```
+
+Example:
+
+If the hypotheses are
+```
+h1 : a = b + 1
+h2 : 1 + a = 7
+```
+
+then `rw h1 at h2` changes `h2` to
+
+```
+h2 : 1 + (b + 1) = 7
+```
+
+Example: if the goal is
+```
+⊢ a ≤ b
+```
+
+then `rw le_def` will change the goal to
+
+```
+⊢ ∃ (c : mynat), b = a + c
+```
+
+Occasionally, it is necessary to do a slightly more targetted rewrite. For example if you have proved `add_comm x y : x + y = y + x`, if the goal is
+
+```
+⊢ a + b = c + d
+```
+
+and you want to change it into
+
+```
+⊢ a + b = d + c
+```
+
+you can type `rw add_comm c`. Just typing `rw add_comm` will rewrite `a + b` to `b + a`.
+
+
+symmetry
+--------
+
+The `symmetry` tactic will change a goal of the form `a = b` to the goal `b = a`. It will also change a goal of the form `a ≠ b` to a goal of the form `b ≠ a`.
+
+`symmetry at H` will change `H : a = b` to `H : b = a`.
+
+
+split
+-----
+
+The `split` tactic will change a goal of the form `P ∧ Q` into two goals `P` and `Q`. It will also change a goal of the form `P ↔ Q` into two goals `P` and `Q`.
+
+Note that when two goals are created, it is considered best practice to deal with each goal separately in `{ }` brackets. For example if the assumptions and goal look like this:
+
+```
+P Q : Prop,
+hpq : P → Q,
+hqp : Q → P
+⊢ P ↔ Q
+```
+
+then a proof might look like this:
+
+```
+  split,
+  {
+    exact hpq
+  },
+  {
+    exact hqp
+  }
+```
+
+intro
+-----
+
+The `intro` tactic can be used when the goal looks like `P → Q` or like `∀ x, f x = g x`.
+
+In the `P → Q` case, `intro HP` turns
+
+```
+⊢ P → Q
+```
+
+to
+
+```
+HP : P
+⊢ Q
+```
+
+and in the `∀ x, f x = g x` case, `intro a` turns
+```
+⊢ ∀ (x : ℕ), f x = g x
+```
+
+to
+
+```
+a : ℕ
+⊢ f a = g a
+```
+
+A variant: the `intros` tactic will introduce more than one variable at once. For example if the state is
+
+```
+⊢ ∀ (x y : ℕ), f x y = g x y
+```
+
+then `intros a b` turns it into
+
+```
+a b : ℕ
+⊢ f a b = g a b
+```
+
+have
+----
+
+If you want to make a new assumption, you can do this with the `have` tactic. For example `have H : 3 + 0 = 3 := add_zero 3` will insert the hypothesis `H : 3 + 0 = 3` into the list of assumptions.
+
+An alternative syntax is `have H : a + b = c,` which then simply adds a new goal `⊢ a + b = c`.
+
+revert
+------
+
+The `revert` tactic does the opposite of the `intro` tactic. For example if the state is
+
+```
+a : ℕ
+⊢ f a = g a
+```
+
+then `revert a` will transform it to
+
+
+```
+⊢ ∀ (a : ℕ), f a = g a
+```
+
+apply
+-----
+
+If the assumptions and goal look like this:
+
+```
+H : P → Q
+⊢ Q
+```
+
+then the tactic `apply H` will change the goal to `⊢ P`.
+
+As a more clever application, `succ_inj` is a proof of
+`∀ (m n : ℕ), succ m = succ n → m = n`. If the goal is
+
+```
+⊢ a = b
+```
+
+then `apply succ_inj` will transform it to
+
+```
+⊢ succ a = succ b
+```
+
+exfalso
+-------
+
+The `exfalso` tactic changes any goal at all to `false`. This is often used when the assumptions are contradictory (e.g. during a proof by contradiction).
+
+Example of usage: if the assumptions and goal are this:
+
+```
+hP : P,
+hnP : P → false
+⊢ Q
+```
+
+then a proof could be
+
+```
+  exfalso,
+  apply hnP,
+  exact hP
+```
+
+left
+----
+
+The `left` tactic changes a goal of the form
+
+```
+⊢ P ∨ Q
+```
+
+to
+
+```
+⊢ P
+```
+
+right
+-----
+
+The `right` tactic changes a goal of the form
+
+```
+⊢ P ∨ Q
+```
+
+to
+
+```
+⊢ Q
+```
+
+congr'
+------
+
+The `congr'` tactic changes a goal of the form
+
+```
+⊢ f a = f b
+```
+
+to a goal of the form
+
+```
+⊢ a = b
+```
+
+Note that if `f` is not injective then this tactic can change a goal which is true into one which is false.
+
+Example of usage: if the goal is
+
+```
+⊢ succ a = succ b
+```
+
+then `congr'` changes it to
+
+```
+⊢ a = b
+```
+
+use
+---
+
+The `use` goal works ong oals of the form
+
+```
+⊢ ∃ (c : mynat), f c
+```
+
+For example, if the goal is
+
+```
+⊢ ∃ (c : mynat), c + 2 = 4
+```
+
+then `use 2` will change the goal into
+
+```
+⊢ 2 + 2 = 4
+```
+
+****
+
+Tricks
+------
+
+`rw [h1, h2, h3]` is the same as
+
+```
+rw h1,
+rw h2,
+rw h3
+```
+
+and `rwa h` is the same as `rw h, try {refl}, try {assumption}`.
diff --git a/src/metric_space/tactics_cheat_sheet.md b/src/metric_space/tactics_cheat_sheet.md
new file mode 100644
index 0000000..ecdc504
--- /dev/null
+++ b/src/metric_space/tactics_cheat_sheet.md
@@ -0,0 +1,34 @@
+# Basic tactic cheat sheet
+
+| Term you want to use | If a hypothesis `h` | If the goal      |
+| ----------|:-------------------:|:----------------:|
+| P → Q     |   `apply h`         | `intro hP`       |
+| P ∧ Q     |   `cases h`         | `split`          |
+| P ∨ Q     |   `cases h`         | `left` or `right`|
+| P = P     |   (useless)         | `refl`           |
+| P = Q     |   `rw h`            |                  |
+| P ↔ Q     | `rw h` or `cases h` | `split`          |
+| false     |  `cases h`          |                  |
+| ∃ x, P x  |  `cases h with x hx`| `use a`          |
+
+
+## Other
+
+`have h : (some true/false statement)` : use if you want to create a new hypothesis `h` and you know the proof. Lean will create a new goal.
+
+`by_cases h : P` does a case split on whether `P` is true
+or false. If Lean complains that it doesn't know that your
+proposition is decidable, try the `classical` tactic
+before running `by_cases`, or write `open_locale classical`
+before you start your proof. 
+
+If you think that a goal should be provable by pure logic,
+given what you have, try `cc`, `tauto!`, `finish` or `simp`.
+These tactics all do subtly different things, but it's
+worth trying them all if you're stuck.
+
+`exfalso` changes the goal to `false`. Can be useful if
+your hypotheses are enough to prove a contradiction, and
+one of them is `h : ¬ P` (which is notation for `h : P → false`).
+After `exfalso` you can `apply P` and reduce your goal to `P`. 
+
diff --git a/src/metric_space/tutorial1_sets.lean b/src/metric_space/tutorial1_sets.lean
new file mode 100644
index 0000000..28faed8
--- /dev/null
+++ b/src/metric_space/tutorial1_sets.lean
@@ -0,0 +1,99 @@
+/- This file is intended for beginner Lean users who know about tactics
+  such as `intro`, `cases`, `exact`, `left`, `right`
+
+-/
+
+import data.set.basic
+
+/-!
+
+# Sets in Lean
+
+In set theory it's convenient to allow all kinds of sets.
+For example, a group can be formalised as an ordered quadruple
+(G,*,1,⁻¹) satisfying some axioms, and there are several tricks
+to make ordered quadruples out of sets.
+
+In Lean, this heavy lifting is done by the theory of inductive types,
+and we have no need for exotic ordered quadruples. However one certainly
+needs a theory of sets -- one wants to take the intersection of two subgroups
+of a group, or arbitrary unions of open sets in a metric space.
+
+In particular one wants to work with *subsets* of a given set or type. Lean
+has such functionality, and we explore it here, learning how to prove
+basic statements such as S ⊆ S ∪ T, or ∅ ⊆ S, for S and T subsets of a fixed type X. 
+
+## Introduction
+
+Let `X` be a fixed type. This will be our "universe", and all sets in this
+introduction will be subsets of `X`. Recall that because `X` is a type, it has
+terms rather than elements, and we write `x : X` to mean that `x` is a term of type `X`.
+
+The type of subsets of `X` is not called `subset X` but `set X`. So `S : set X` means
+that `S` is a subset of `X`. If `x : X` then we can ask if `x ∈ S`, which is a true/false
+statement. Hence any subset `S` of `X` gives rise to a function `X → Prop` (recall that
+`Prop` is the universe of all true/false statements) sending `x : X` to the statement
+`x ∈ S`. Conversely, given a function `f : X → Prop` we can form a subset of `X`
+consisting of the `x : X` such that `f x` is true. The notation for this in Lean
+is `{x : X | f x}`. Thus we have a correspondence between subsets `S : set X` and
+functions `X → Prop`, and in fact internally a subset `S` of `X` is stored as a
+function `S : X → Prop`, and `x ∈ S` is just notation for the true/false statement `S x`. 
+
+For example if `X = ℝ` and `f : X → Prop` sends the term `x : X` to the statement
+`x^2 = 4`, then the corresponding subset `S : set X` is the set `{x : X | x^2 = 4}`,
+or in other words the subset `{2, -2}` of `ℝ`.
+
+## Notation
+
+Say `X` is a fixed type, and `S T : set X` are subsets.
+
+`S ⊆ T` is defined to mean `∀ x : X, x ∈ S → x ∈ T`
+`S ⊂ T` is defined to mean `S ⊆ T ∧ ¬ (T ⊆ S)`. 
+`S ∩ T` is defined to mean the set `{x : X | x ∈ S ∧ x ∈ T}`, and in particular
+  `x ∈ S ∩ T` is by definition equal to the statement `x ∈ S ∧ x ∈ T`. 
+`S ∪ T` is the set `{x : X | x ∈ S ∨ x ∈ T}`. 
+`∅ : set X` is the empty set. The corresponding function X → Prop sends `x : X` to
+  the proposition `false`, a proposition with no proof. 
+`univ : set X` is the whole type `X` considered as a set. Note that it does not
+  make sense to say `univ = X` because they have different types: the type of `univ`
+  is `set X` and the type of `X` is `Type`. The underlying function sends `x : X`
+  to the proposition `true`, a proposition which can be proved with the tactic `trivial`.
+
+-/
+
+-- Let's prove some theorems about sets in Lean.
+
+namespace tutorial
+
+variables {X : Type} {S T U : set X}
+
+example : S ∩ T ⊆ S :=
+begin
+  -- recall that (S ∩ T) ⊆ S is defined to mean ∀ x : X, x ∈ (S ∩ T) → x ∈ S,
+  -- so we can start with `intro x`
+  intro x,
+  -- Assume x ∈ S ∩ T
+  intro hxST,
+  -- the hypothesis hxST is defined to mean `x ∈ S ∧ x ∈ T`, so we can
+  -- do `cases` on `hxST` to get to these two simpler proofs.
+  cases hxST with hxS hxT,
+  -- but our goal is exactly hxS
+  exact hxS
+end
+
+-- Exercise.
+-- recall x ∈ S ∪ T *means* x ∈ S ∨ x ∈ T.
+example : S ⊆ S ∪ T :=
+begin
+  sorry
+end
+
+
+#exit
+
+P → Q
+P ∧ Q
+P ∨ Q
+P ↔ Q
+¬ P
+∃ x : P x
\ No newline at end of file