diff --git a/src/analysis/calculus/times_cont_diff.lean b/src/analysis/calculus/times_cont_diff.lean
index 42cde032a3ff1..55b10a510db8c 100644
--- a/src/analysis/calculus/times_cont_diff.lean
+++ b/src/analysis/calculus/times_cont_diff.lean
@@ -2429,6 +2429,9 @@ lemma times_cont_diff_at_inv {x : 𝕜'} (hx : x ≠ 0) {n} :
   times_cont_diff_at 𝕜 n has_inv.inv x :=
 by simpa only [inverse_eq_has_inv] using times_cont_diff_at_ring_inverse 𝕜 (units.mk0 x hx)
 
+lemma times_cont_diff_on_inv {n} : times_cont_diff_on 𝕜 n (has_inv.inv : 𝕜' → 𝕜') {0}ᶜ :=
+λ x hx, (times_cont_diff_at_inv 𝕜 hx).times_cont_diff_within_at
+
 variable {𝕜}
 
 -- TODO: the next few lemmas don't need `𝕜` or `𝕜'` to be complete
@@ -2683,7 +2686,6 @@ begin
     exact with_top.coe_le_coe.2 (nat.le_succ n) }
 end
 
-
 /-- A function is `C^∞` on an open domain if and only if it is differentiable
 there, and its derivative (formulated with `deriv`) is `C^∞`. -/
 theorem times_cont_diff_on_top_iff_deriv_of_open (hs : is_open s₂) :
diff --git a/src/analysis/special_functions/exp_log.lean b/src/analysis/special_functions/exp_log.lean
index 2ea61436da3b3..fbcf08f2ee574 100644
--- a/src/analysis/special_functions/exp_log.lean
+++ b/src/analysis/special_functions/exp_log.lean
@@ -282,31 +282,89 @@ namespace real
 
 variables {x y z : ℝ}
 
-lemma exists_exp_eq_of_pos {x : ℝ} (hx : 0 < x) : ∃ y, exp y = x :=
-have ∀ {z:ℝ}, 1 ≤ z → z ∈ set.range exp,
-  from λ z hz, intermediate_value_univ 0 (z - 1) continuous_exp
-    ⟨by simpa, by simpa using add_one_le_exp_of_nonneg (sub_nonneg.2 hz)⟩,
-match le_total x 1 with
-| (or.inl hx1) := let ⟨y, hy⟩ := this (one_le_inv hx hx1) in
-  ⟨-y, by rw [exp_neg, hy, inv_inv']⟩
-| (or.inr hx1) := this hx1
+/-- The real exponential function tends to `+∞` at `+∞`. -/
+lemma tendsto_exp_at_top : tendsto exp at_top at_top :=
+begin
+  have A : tendsto (λx:ℝ, x + 1) at_top at_top :=
+    tendsto_at_top_add_const_right at_top 1 tendsto_id,
+  have B : ∀ᶠ x in at_top, x + 1 ≤ exp x :=
+    eventually_at_top.2 ⟨0, λx hx, add_one_le_exp_of_nonneg hx⟩,
+  exact tendsto_at_top_mono' at_top B A
 end
 
+/-- The real exponential function tends to `0` at `-∞` or, equivalently, `exp(-x)` tends to `0`
+at `+∞` -/
+lemma tendsto_exp_neg_at_top_nhds_0 : tendsto (λx, exp (-x)) at_top (𝓝 0) :=
+(tendsto_inv_at_top_zero.comp tendsto_exp_at_top).congr (λx, (exp_neg x).symm)
+
+/-- The real exponential function tends to `1` at `0`. -/
+lemma tendsto_exp_nhds_0_nhds_1 : tendsto exp (𝓝 0) (𝓝 1) :=
+by { convert continuous_exp.tendsto 0, simp }
+
+lemma tendsto_exp_at_bot : tendsto exp at_bot (𝓝 0) :=
+(tendsto_exp_neg_at_top_nhds_0.comp tendsto_neg_at_bot_at_top).congr $
+  λ x, congr_arg exp $ neg_neg x
+
+lemma tendsto_exp_at_bot_nhds_within : tendsto exp at_bot (𝓝[set.Ioi 0] 0) :=
+tendsto_inf.2 ⟨tendsto_exp_at_bot, tendsto_principal.2 $ eventually_of_forall exp_pos⟩
+
+lemma range_exp : set.range exp = set.Ioi 0 :=
+set.ext $ λ y, ⟨λ ⟨x, hx⟩, hx ▸ exp_pos x,
+  λ hy, mem_range_of_exists_le_of_exists_ge continuous_exp
+    (tendsto_exp_at_bot.eventually (ge_mem_nhds hy)).exists
+    (tendsto_exp_at_top.eventually (eventually_ge_at_top y)).exists⟩
+
+/-- `real.exp` as an order isomorphism between `ℝ` and `(0, +∞)`. -/
+def exp_order_iso : ℝ ≃o set.Ioi (0 : ℝ) :=
+(exp_strict_mono.order_iso _).trans $ order_iso.set_congr _ _ range_exp
+
+@[simp] lemma coe_exp_order_iso_apply (x : ℝ) : (exp_order_iso x : ℝ) = exp x := rfl
+
+@[simp] lemma coe_comp_exp_order_iso : coe ∘ exp_order_iso = exp := rfl
+
+@[simp] lemma map_exp_at_top : map exp at_top = at_top :=
+by rw [← coe_comp_exp_order_iso, ← filter.map_map, order_iso.map_at_top,
+  map_coe_Ioi_at_top]
+
+@[simp] lemma comap_exp_at_top : comap exp at_top = at_top :=
+by rw [← map_exp_at_top, comap_map exp_injective, map_exp_at_top]
+
+@[simp] lemma tendsto_exp_comp_at_top {α : Type*} {l : filter α} {f : α → ℝ} :
+  tendsto (λ x, exp (f x)) l at_top ↔ tendsto f l at_top :=
+by rw [← tendsto_comap_iff, comap_exp_at_top]
+
+lemma tendsto_comp_exp_at_top {α : Type*} {l : filter α} {f : ℝ → α} :
+  tendsto (λ x, f (exp x)) at_top l ↔ tendsto f at_top l :=
+by rw [← tendsto_map'_iff, map_exp_at_top]
+
+@[simp] lemma map_exp_at_bot : map exp at_bot = 𝓝[set.Ioi 0] 0 :=
+by rw [← coe_comp_exp_order_iso, ← filter.map_map, order_iso.map_at_bot,
+  ← map_coe_Ioi_at_bot]
+
+lemma comap_exp_nhds_within_Ioi_zero : comap exp (𝓝[set.Ioi 0] 0) = at_bot :=
+by rw [← map_exp_at_bot, comap_map exp_injective]
+
+lemma tendsto_comp_exp_at_bot {α : Type*} {l : filter α} {f : ℝ → α} :
+  tendsto (λ x, f (exp x)) at_bot l ↔ tendsto f (𝓝[set.Ioi 0] 0) l :=
+by rw [← map_exp_at_bot, tendsto_map'_iff]
+
 /-- The real logarithm function, equal to the inverse of the exponential for `x > 0`,
 to `log |x|` for `x < 0`, and to `0` for `0`. We use this unconventional extension to
 `(-∞, 0]` as it gives the formula `log (x * y) = log x + log y` for all nonzero `x` and `y`, and
 the derivative of `log` is `1/x` away from `0`. -/
 @[pp_nodot] noncomputable def log (x : ℝ) : ℝ :=
-if hx : x ≠ 0 then classical.some (exists_exp_eq_of_pos (abs_pos.mpr hx)) else 0
+if hx : x = 0 then 0 else exp_order_iso.symm ⟨abs x, abs_pos.2 hx⟩
+
+lemma log_of_ne_zero (hx : x ≠ 0) : log x = exp_order_iso.symm ⟨abs x, abs_pos.2 hx⟩ := dif_neg hx
+
+lemma log_of_pos (hx : 0 < x) : log x = exp_order_iso.symm ⟨x, hx⟩ :=
+by { rw [log_of_ne_zero hx.ne'], congr, exact abs_of_pos hx }
 
 lemma exp_log_eq_abs (hx : x ≠ 0) : exp (log x) = abs x :=
-by { rw [log, dif_pos hx], exact classical.some_spec (exists_exp_eq_of_pos ((abs_pos.mpr hx))) }
+by rw [log_of_ne_zero hx, ← coe_exp_order_iso_apply, order_iso.apply_symm_apply, subtype.coe_mk]
 
 lemma exp_log (hx : 0 < x) : exp (log x) = x :=
-by { rw exp_log_eq_abs (ne_of_gt hx), exact abs_of_pos hx }
-
-lemma range_exp : set.range exp = {x | 0 < x} :=
-set.ext $ λ x, ⟨by { rintro ⟨x, rfl⟩, exact exp_pos x }, λ hx, ⟨log x, exp_log hx⟩⟩
+by { rw exp_log_eq_abs hx.ne', exact abs_of_pos hx }
 
 lemma exp_log_of_neg (hx : x < 0) : exp (log x) = -x :=
 by { rw exp_log_eq_abs (ne_of_lt hx), exact abs_of_neg hx }
@@ -314,6 +372,9 @@ by { rw exp_log_eq_abs (ne_of_lt hx), exact abs_of_neg hx }
 @[simp] lemma log_exp (x : ℝ) : log (exp x) = x :=
 exp_injective $ exp_log (exp_pos x)
 
+lemma surj_on_log : set.surj_on log (set.Ioi 0) set.univ :=
+λ x _, ⟨exp x, exp_pos x, log_exp x⟩
+
 lemma log_surjective : function.surjective log :=
 λ x, ⟨exp x, log_exp x⟩
 
@@ -330,14 +391,15 @@ exp_injective $ by rw [exp_log zero_lt_one, exp_zero]
 begin
   by_cases h : x = 0,
   { simp [h] },
-  { apply exp_injective,
-    rw [exp_log_eq_abs h, exp_log_eq_abs, abs_abs],
-    simp [h] }
+  { rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs] }
 end
 
 @[simp] lemma log_neg_eq_log (x : ℝ) : log (-x) = log x :=
 by rw [← log_abs x, ← log_abs (-x), abs_neg]
 
+lemma surj_on_log' : set.surj_on log (set.Iio 0) set.univ :=
+λ x _, ⟨-exp x, neg_lt_zero.2 $ exp_pos x, by rw [log_neg_eq_log, log_exp]⟩
+
 lemma log_mul (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y :=
 exp_injective $
 by rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]
@@ -345,13 +407,11 @@ by rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_e
 @[simp] lemma log_inv (x : ℝ) : log (x⁻¹) = -log x :=
 begin
   by_cases hx : x = 0, { simp [hx] },
-  apply eq_neg_of_add_eq_zero,
-  rw [← log_mul (inv_ne_zero hx) hx, inv_mul_cancel hx, log_one]
+  rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
 end
 
 lemma log_le_log (h : 0 < x) (h₁ : 0 < y) : real.log x ≤ real.log y ↔ x ≤ y :=
-⟨λ h₂, by rwa [←real.exp_le_exp, real.exp_log h, real.exp_log h₁] at h₂, λ h₂,
-(real.exp_le_exp).1 $ by rwa [real.exp_log h₁, real.exp_log h]⟩
+by rw [← exp_le_exp, exp_log h, exp_log h₁]
 
 lemma log_lt_log (hx : 0 < x) : x < y → log x < log y :=
 by { intro h, rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)] }
@@ -389,107 +449,142 @@ end
 lemma log_nonpos (hx : 0 ≤ x) (h'x : x ≤ 1) : log x ≤ 0 :=
 (log_nonpos_iff' hx).2 h'x
 
-section prove_log_is_continuous
+lemma strict_mono_incr_on_log : strict_mono_incr_on log (set.Ioi 0) :=
+λ x hx y hy hxy, log_lt_log hx hxy
 
-lemma tendsto_log_one_zero : tendsto log (𝓝 1) (𝓝 0) :=
+lemma strict_mono_decr_on_log : strict_mono_decr_on log (set.Iio 0) :=
 begin
-  rw tendsto_nhds_nhds, assume ε ε0,
-  let δ := min (exp ε - 1) (1 - exp (-ε)),
-  have : 0 < δ,
-    refine lt_min (sub_pos_of_lt (by rwa one_lt_exp_iff)) (sub_pos_of_lt _),
-      by { rw exp_lt_one_iff, linarith },
-  use [δ, this], assume x h,
-  cases le_total 1 x with hx hx,
-  { have h : x < exp ε,
-      rw [dist_eq, abs_of_nonneg (sub_nonneg_of_le hx)] at h,
-      linarith [(min_le_left _ _ : δ ≤ exp ε - 1)],
-    calc abs (log x - 0) = abs (log x) : by simp
-      ... = log x : abs_of_nonneg $ log_nonneg hx
-      ... < ε : by { rwa [← exp_lt_exp, exp_log], linarith }},
-  { have h : exp (-ε) < x,
-      rw [dist_eq, abs_of_nonpos (sub_nonpos_of_le hx)] at h,
-      linarith [(min_le_right _ _ : δ ≤ 1 - exp (-ε))],
-    have : 0 < x := lt_trans (exp_pos _) h,
-    calc abs (log x - 0) = abs (log x) : by simp
-      ... = -log x : abs_of_nonpos $ log_nonpos (le_of_lt this) hx
-      ... < ε : by { rw [neg_lt, ← exp_lt_exp, exp_log], assumption' } }
+  rintros x (hx : x < 0) y (hy : y < 0) hxy,
+  rw [← log_abs y, ← log_abs x],
+  refine log_lt_log (abs_pos.2 hy.ne) _,
+  rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]
 end
 
-lemma continuous_log' : continuous (λx : {x:ℝ // 0 < x}, log x) :=
-continuous_iff_continuous_at.2 $ λ x,
+/-- The real logarithm function tends to `+∞` at `+∞`. -/
+lemma tendsto_log_at_top : tendsto log at_top at_top :=
+tendsto_comp_exp_at_top.1 $ by simpa only [log_exp] using tendsto_id
+
+lemma tendsto_log_nhds_within_zero : tendsto log (𝓝[{0}ᶜ] 0) at_bot :=
 begin
-  rw continuous_at,
-  let f₁ := λ h:{h:ℝ // 0 < h}, log (x.1 * h.1),
-  let f₂ := λ y:{y:ℝ // 0 < y}, subtype.mk (x.1 ⁻¹ * y.1) (mul_pos (inv_pos.2 x.2) y.2),
-  have H1 : tendsto f₁ (𝓝 ⟨1, zero_lt_one⟩) (𝓝 (log (x.1*1))),
-    have : f₁ = λ h:{h:ℝ // 0 < h}, log x.1 + log h.1,
-      ext h, rw ← log_mul (ne_of_gt x.2) (ne_of_gt h.2),
-    simp only [this, log_mul (ne_of_gt x.2) one_ne_zero, log_one],
-    exact tendsto_const_nhds.add (tendsto.comp tendsto_log_one_zero continuous_at_subtype_coe),
-  have H2 : tendsto f₂ (𝓝 x) (𝓝 ⟨x.1⁻¹ * x.1, mul_pos (inv_pos.2 x.2) x.2⟩),
-    rw tendsto_subtype_rng, exact tendsto_const_nhds.mul continuous_at_subtype_coe,
-  suffices h : tendsto (f₁ ∘ f₂) (𝓝 x) (𝓝 (log x.1)),
-  begin
-    convert h, ext y,
-    have : x.val * (x.val⁻¹ * y.val) = y.val,
-      rw [← mul_assoc, mul_inv_cancel (ne_of_gt x.2), one_mul],
-    show log (y.val) = log (x.val * (x.val⁻¹ * y.val)), rw this
-  end,
-  exact tendsto.comp (by rwa mul_one at H1)
-    (by { simp only [inv_mul_cancel (ne_of_gt x.2)] at H2, assumption })
+  rw [← (show _ = log, from funext log_abs)],
+  refine tendsto.comp (_ : tendsto log (𝓝[set.Ioi 0] (abs 0)) at_bot)
+    ((continuous_abs.tendsto 0).inf (tendsto_principal_principal.2 $ λ a, abs_pos.2)),
+  rw [abs_zero, ← tendsto_comp_exp_at_bot],
+  simpa using tendsto_id
 end
 
-lemma continuous_at_log (hx : 0 < x) : continuous_at log x :=
-continuous_within_at.continuous_at (continuous_on_iff_continuous_restrict.2 continuous_log' _ hx)
-  (mem_nhds_sets (is_open_lt' _) hx)
+lemma continuous_on_log : continuous_on log {0}ᶜ :=
+begin
+  rw [continuous_on_iff_continuous_restrict, set.restrict],
+  conv in (log _) { rw [log_of_ne_zero (show (x : ℝ) ≠ 0, from x.2)] },
+  exact exp_order_iso.symm.continuous.comp (continuous_subtype_mk _ continuous_subtype_coe.norm)
+end
 
-/--
-Three forms of the continuity of `real.log` are provided.
-For the other two forms, see `real.continuous_log'` and `real.continuous_at_log`
--/
-lemma continuous_log {α : Type*} [topological_space α] {f : α → ℝ} (h : ∀a, 0 < f a)
-  (hf : continuous f) : continuous (λa, log (f a)) :=
-show continuous ((log ∘ @subtype.val ℝ (λr, 0 < r)) ∘ λa, ⟨f a, h a⟩),
-  from continuous_log'.comp (continuous_subtype_mk _ hf)
+lemma continuous_log' : continuous (λ x : {x : ℝ // 0 < x}, log x) :=
+continuous_on_iff_continuous_restrict.1 $ continuous_on_log.mono $ λ x hx, ne_of_gt hx
+
+lemma continuous_at_log (hx : x ≠ 0) : continuous_at log x :=
+(continuous_on_log x hx).continuous_at $ mem_nhds_sets is_open_compl_singleton hx
 
-end prove_log_is_continuous
+@[simp] lemma continuous_at_log_iff : continuous_at log x ↔ x ≠ 0 :=
+begin
+  refine ⟨_, continuous_at_log⟩,
+  rintros h rfl,
+  exact not_tendsto_nhds_of_tendsto_at_bot tendsto_log_nhds_within_zero _
+    (h.tendsto.mono_left inf_le_left)
+end
 
 lemma has_deriv_at_log_of_pos (hx : 0 < x) : has_deriv_at log x⁻¹ x :=
 have has_deriv_at log (exp $ log x)⁻¹ x,
-from (has_deriv_at_exp $ log x).of_local_left_inverse (continuous_at_log hx)
-  (ne_of_gt $ exp_pos _) $ eventually.mono (mem_nhds_sets is_open_Ioi hx) @exp_log,
+from (has_deriv_at_exp $ log x).of_local_left_inverse (continuous_at_log hx.ne')
+  (ne_of_gt $ exp_pos _) $ eventually.mono (lt_mem_nhds hx) @exp_log,
 by rwa [exp_log hx] at this
 
 lemma has_deriv_at_log (hx : x ≠ 0) : has_deriv_at log x⁻¹ x :=
 begin
-  by_cases h : 0 < x, { exact has_deriv_at_log_of_pos h },
-  push_neg at h,
-  convert ((has_deriv_at_log_of_pos (neg_pos.mpr (lt_of_le_of_ne h hx)))
-    .comp x (has_deriv_at_id x).neg),
-  { ext y, exact (log_neg_eq_log y).symm },
-  { field_simp [hx] }
+  cases hx.lt_or_lt with hx hx,
+  { convert (has_deriv_at_log_of_pos (neg_pos.mpr hx)).comp x (has_deriv_at_neg x),
+    { ext y, exact (log_neg_eq_log y).symm },
+    { field_simp [hx.ne] } },
+  { exact has_deriv_at_log_of_pos hx }
 end
 
+lemma differentiable_at_log (hx : x ≠ 0) : differentiable_at ℝ log x :=
+(has_deriv_at_log hx).differentiable_at
+
+lemma differentiable_on_log : differentiable_on ℝ log {0}ᶜ :=
+λ x hx, (differentiable_at_log hx).differentiable_within_at
+
+@[simp] lemma differentiable_at_log_iff : differentiable_at ℝ log x ↔ x ≠ 0 :=
+⟨λ h, continuous_at_log_iff.1 h.continuous_at, differentiable_at_log⟩
+
+lemma deriv_log (x : ℝ) : deriv log x = x⁻¹ :=
+if hx : x = 0 then
+  by rw [deriv_zero_of_not_differentiable_at (mt differentiable_at_log_iff.1 (not_not.2 hx)), hx,
+    inv_zero]
+else (has_deriv_at_log hx).deriv
+
+@[simp] lemma deriv_log' : deriv log = has_inv.inv := funext deriv_log
+
 lemma measurable_log : measurable log :=
 measurable_of_measurable_on_compl_singleton 0 $ continuous.measurable $
-  continuous_iff_continuous_at.2 $ λ x, (real.has_deriv_at_log x.2).continuous_at.comp
-    continuous_at_subtype_coe
+  continuous_on_iff_continuous_restrict.1 continuous_on_log
+
+lemma times_cont_diff_on_log {n : with_top ℕ} : times_cont_diff_on ℝ n log {0}ᶜ :=
+begin
+  suffices : times_cont_diff_on ℝ ⊤ log {0}ᶜ, from this.of_le le_top,
+  refine (times_cont_diff_on_top_iff_deriv_of_open is_open_compl_singleton).2 _,
+  simp [differentiable_on_log, times_cont_diff_on_inv]
+end
+
+lemma times_cont_diff_at_log (hx : x ≠ 0) {n : with_top ℕ} : times_cont_diff_at ℝ n log x :=
+(times_cont_diff_on_log x hx).times_cont_diff_at $ mem_nhds_sets is_open_compl_singleton hx
 
 end real
 
 section log_differentiable
 open real
 
+section continuity
+
+variables {α : Type*}
+
+lemma filter.tendsto.log {f : α → ℝ} {l : filter α} {x : ℝ} (h : tendsto f l (𝓝 x)) (hx : x ≠ 0) :
+  tendsto (λ x, log (f x)) l (𝓝 (log x)) :=
+(continuous_at_log hx).tendsto.comp h
+
+variables [topological_space α] {f : α → ℝ} {s : set α} {a : α}
+
+lemma continuous.log (hf : continuous f) (h₀ : ∀ x, f x ≠ 0) : continuous (λ x, log (f x)) :=
+continuous_on_log.comp_continuous hf h₀
+
+lemma continuous_at.log (hf : continuous_at f a) (h₀ : f a ≠ 0) :
+  continuous_at (λ x, log (f x)) a :=
+hf.log h₀
+
+lemma continuous_within_at.log (hf : continuous_within_at f s a) (h₀ : f a ≠ 0) :
+  continuous_within_at (λ x, log (f x)) s a :=
+hf.log h₀
+
+lemma continuous_on.log (hf : continuous_on f s) (h₀ : ∀ x ∈ s, f x ≠ 0) :
+  continuous_on (λ x, log (f x)) s :=
+λ x hx, (hf x hx).log (h₀ x hx)
+
+end continuity
+
+section deriv
+
 variables {f : ℝ → ℝ} {x f' : ℝ} {s : set ℝ}
 
-lemma measurable.log (hf : measurable f) : measurable (λ x, log (f x)) :=
+lemma measurable.log {α : Type*} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
+  measurable (λ x, log (f x)) :=
 measurable_log.comp hf
 
 lemma has_deriv_within_at.log (hf : has_deriv_within_at f f' s x) (hx : f x ≠ 0) :
   has_deriv_within_at (λ y, log (f y)) (f' / (f x)) s x :=
 begin
-  convert (has_deriv_at_log hx).comp_has_deriv_within_at x hf,
-  field_simp
+  rw div_eq_inv_mul,
+  exact (has_deriv_at_log hx).comp_has_deriv_within_at x hf
 end
 
 lemma has_deriv_at.log (hf : has_deriv_at f f' x) (hx : f x ≠ 0) :
@@ -499,13 +594,37 @@ begin
   exact hf.log hx
 end
 
+lemma deriv_within.log (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0)
+  (hxs : unique_diff_within_at ℝ s x) :
+  deriv_within (λx, log (f x)) s x = (deriv_within f s x) / (f x) :=
+(hf.has_deriv_within_at.log hx).deriv_within hxs
+
+@[simp] lemma deriv.log (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :
+  deriv (λx, log (f x)) x = (deriv f x) / (f x) :=
+(hf.has_deriv_at.log hx).deriv
+
+end deriv
+
+section fderiv
+
+variables {E : Type*} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {f' : E →L[ℝ] ℝ}
+  {s : set E}
+
+lemma has_fderiv_within_at.log (hf : has_fderiv_within_at f f' s x) (hx : f x ≠ 0) :
+  has_fderiv_within_at (λ x, log (f x)) ((f x)⁻¹ • f') s x :=
+(has_deriv_at_log hx).comp_has_fderiv_within_at x hf
+
+lemma has_fderiv_at.log (hf : has_fderiv_at f f' x) (hx : f x ≠ 0) :
+  has_fderiv_at (λ x, log (f x)) ((f x)⁻¹ • f') x :=
+(has_deriv_at_log hx).comp_has_fderiv_at x hf
+
 lemma differentiable_within_at.log (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) :
   differentiable_within_at ℝ (λx, log (f x)) s x :=
-(hf.has_deriv_within_at.log hx).differentiable_within_at
+(hf.has_fderiv_within_at.log hx).differentiable_within_at
 
 @[simp] lemma differentiable_at.log (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :
   differentiable_at ℝ (λx, log (f x)) x :=
-(hf.has_deriv_at.log hx).differentiable_at
+(hf.has_fderiv_at.log hx).differentiable_at
 
 lemma differentiable_on.log (hf : differentiable_on ℝ f s) (hx : ∀ x ∈ s, f x ≠ 0) :
   differentiable_on ℝ (λx, log (f x)) s :=
@@ -515,38 +634,21 @@ lemma differentiable_on.log (hf : differentiable_on ℝ f s) (hx : ∀ x ∈ s,
   differentiable ℝ (λx, log (f x)) :=
 λx, (hf x).log (hx x)
 
-lemma deriv_within_log' (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0)
+lemma fderiv_within.log (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0)
   (hxs : unique_diff_within_at ℝ s x) :
-  deriv_within (λx, log (f x)) s x = (deriv_within f s x) / (f x) :=
-(hf.has_deriv_within_at.log hx).deriv_within hxs
+  fderiv_within ℝ (λx, log (f x)) s x = (f x)⁻¹ • fderiv_within ℝ f s x :=
+(hf.has_fderiv_within_at.log hx).fderiv_within hxs
 
-@[simp] lemma deriv_log' (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :
-  deriv (λx, log (f x)) x = (deriv f x) / (f x) :=
-(hf.has_deriv_at.log hx).deriv
+@[simp] lemma fderiv.log (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :
+  fderiv ℝ (λx, log (f x)) x = (f x)⁻¹ • fderiv ℝ f x :=
+(hf.has_fderiv_at.log hx).fderiv
+
+end fderiv
 
 end log_differentiable
 
 namespace real
 
-/-- The real exponential function tends to `+∞` at `+∞`. -/
-lemma tendsto_exp_at_top : tendsto exp at_top at_top :=
-begin
-  have A : tendsto (λx:ℝ, x + 1) at_top at_top :=
-    tendsto_at_top_add_const_right at_top 1 tendsto_id,
-  have B : ∀ᶠ x in at_top, x + 1 ≤ exp x :=
-    eventually_at_top.2 ⟨0, λx hx, add_one_le_exp_of_nonneg hx⟩,
-  exact tendsto_at_top_mono' at_top B A
-end
-
-/-- The real exponential function tends to `0` at `-∞` or, equivalently, `exp(-x)` tends to `0`
-at `+∞` -/
-lemma tendsto_exp_neg_at_top_nhds_0 : tendsto (λx, exp (-x)) at_top (𝓝 0) :=
-(tendsto_inv_at_top_zero.comp (tendsto_exp_at_top)).congr (λx, (exp_neg x).symm)
-
-/-- The real exponential function tends to `1` at `0`. -/
-lemma tendsto_exp_nhds_0_nhds_1 : tendsto exp (𝓝 0) (𝓝 1) :=
-by { convert continuous_exp.tendsto 0, simp }
-
 /-- The function `exp(x)/x^n` tends to `+∞` at `+∞`, for any natural number `n` -/
 lemma tendsto_exp_div_pow_at_top (n : ℕ) : tendsto (λx, exp x / x^n) at_top at_top :=
 begin
@@ -618,17 +720,6 @@ begin
     { exact neg_zero.symm } },
 end
 
-/-- The real logarithm function tends to `+∞` at `+∞`. -/
-lemma tendsto_log_at_top : tendsto log at_top at_top :=
-begin
-  rw tendsto_at_top_at_top,
-  intro b,
-  use exp b,
-  intros a hab,
-  rw [← exp_le_exp, exp_log_eq_abs (ne_of_gt $ lt_of_lt_of_le (exp_pos b) hab)],
-  exact le_trans hab (le_abs_self a)
-end
-
 open_locale big_operators
 
 /-- A crude lemma estimating the difference between `log (1-x)` and its Taylor series at `0`,
diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean
index 9f098e9f8c8bf..231622a7decc4 100644
--- a/src/data/complex/exponential.lean
+++ b/src/data/complex/exponential.lean
@@ -1097,12 +1097,14 @@ lemma exp_strict_mono : strict_mono exp :=
 
 @[mono] lemma exp_monotone : ∀ {x y : ℝ}, x ≤ y → exp x ≤ exp y := exp_strict_mono.monotone
 
-lemma exp_lt_exp {x y : ℝ} : exp x < exp y ↔ x < y := exp_strict_mono.lt_iff_lt
+@[simp] lemma exp_lt_exp {x y : ℝ} : exp x < exp y ↔ x < y := exp_strict_mono.lt_iff_lt
 
-lemma exp_le_exp {x y : ℝ} : exp x ≤ exp y ↔ x ≤ y := exp_strict_mono.le_iff_le
+@[simp] lemma exp_le_exp {x y : ℝ} : exp x ≤ exp y ↔ x ≤ y := exp_strict_mono.le_iff_le
 
 lemma exp_injective : function.injective exp := exp_strict_mono.injective
 
+@[simp] lemma exp_eq_exp {x y : ℝ} : exp x = exp y ↔ x = y := exp_injective.eq_iff
+
 @[simp] lemma exp_eq_one_iff : exp x = 1 ↔ x = 0 :=
 by rw [← exp_zero, exp_injective.eq_iff]
 
diff --git a/src/data/set/function.lean b/src/data/set/function.lean
index bd19969b1164e..2ea9dd502bb82 100644
--- a/src/data/set/function.lean
+++ b/src/data/set/function.lean
@@ -646,6 +646,11 @@ lemma strict_mono.comp_strict_mono_incr_on [preorder α] [preorder β] [preorder
   strict_mono_incr_on (g ∘ f) s :=
 λ x hx y hy hxy, hg $ hf hx hy hxy
 
+lemma strict_mono.cod_restrict [preorder α] [preorder β] {f : α → β} (hf : strict_mono f)
+  {s : set β} (hs : ∀ x, f x ∈ s) :
+  strict_mono (set.cod_restrict f s hs) :=
+hf
+
 namespace function
 
 open set
diff --git a/src/order/rel_iso.lean b/src/order/rel_iso.lean
index 856b22cd96895..0b0405e2ee4d3 100644
--- a/src/order/rel_iso.lean
+++ b/src/order/rel_iso.lean
@@ -551,14 +551,38 @@ have gf : ∀ (a : α), a = g (f a) := by { intro, rw [←cmp_eq_eq_iff, h, cmp_
   right_inv := by { intro, rw [←cmp_eq_eq_iff, ←h, cmp_self_eq_eq] },
   map_rel_iff' := by { intros, apply le_iff_le_of_cmp_eq_cmp, convert h _ _, apply gf } }
 
-/-- A strictly monotone surjective function from a linear order is an order isomorphism. -/
-noncomputable def of_strict_mono_surjective {α β} [linear_order α] [preorder β] (f : α → β)
-  (h_mono : strict_mono f) (h_surj : surjective f) : α ≃o β :=
-{ to_equiv := equiv.of_bijective f ⟨h_mono.injective, h_surj⟩,
-  .. order_embedding.of_strict_mono f h_mono }
+/-- Order isomorphism between two equal sets. -/
+def set_congr (s t : set α) (h : s = t) : s ≃o t :=
+{ to_equiv := equiv.set_congr h,
+  map_rel_iff' := λ x y, iff.rfl }
+
+/-- Order isomorphism between `univ : set α` and `α`. -/
+def set.univ : (set.univ : set α) ≃o α :=
+{ to_equiv := equiv.set.univ α,
+  map_rel_iff' := λ x y, iff.rfl }
 
 end order_iso
 
+/-- If a function `f` is strictly monotone on a set `s`, then it defines an order isomorphism
+between `s` and its image. -/
+protected noncomputable def strict_mono_incr_on.order_iso {α β} [linear_order α] [preorder β]
+  (f : α → β) (s : set α) (hf : strict_mono_incr_on f s) :
+  s ≃o f '' s :=
+{ to_equiv := hf.inj_on.bij_on_image.equiv _,
+  map_rel_iff' := λ x y, iff.symm $ hf.le_iff_le x.2 y.2 }
+
+/-- A strictly monotone function from a linear order is an order isomorphism between its domain and
+its range. -/
+protected noncomputable def strict_mono.order_iso {α β} [linear_order α] [preorder β] (f : α → β)
+  (h_mono : strict_mono f) : α ≃o set.range f :=
+{ to_equiv := equiv.set.range f h_mono.injective,
+  map_rel_iff' := λ a b, h_mono.le_iff_le.symm }
+
+/-- A strictly monotone surjective function from a linear order is an order isomorphism. -/
+noncomputable def strict_mono.order_iso_of_surjective {α β} [linear_order α] [preorder β]
+  (f : α → β) (h_mono : strict_mono f) (h_surj : surjective f) : α ≃o β :=
+(h_mono.order_iso f).trans $ (order_iso.set_congr _ _ h_surj.range_eq).trans order_iso.set.univ
+
 /-- A subset `p : set α` embeds into `α` -/
 def set_coe_embedding {α : Type*} (p : set α) : p ↪ α := ⟨subtype.val, @subtype.eq _ _⟩
 
diff --git a/src/topology/algebra/ordered.lean b/src/topology/algebra/ordered.lean
index 1667358d6ac32..8a9d9ef3760c9 100644
--- a/src/topology/algebra/ordered.lean
+++ b/src/topology/algebra/ordered.lean
@@ -212,19 +212,19 @@ lemma is_closed.is_closed_le [topological_space β] {f g : β → α} {s : set 
 omit t
 
 lemma nhds_within_Ici_ne_bot {a b : α} (H₂ : a ≤ b) :
-  𝓝[Ici a] b ≠ ⊥ :=
+  ne_bot (𝓝[Ici a] b) :=
 nhds_within_ne_bot_of_mem H₂
 
-lemma nhds_within_Ici_self_ne_bot (a : α) :
-  𝓝[Ici a] a ≠ ⊥ :=
+@[instance] lemma nhds_within_Ici_self_ne_bot (a : α) :
+  ne_bot (𝓝[Ici a] a) :=
 nhds_within_Ici_ne_bot (le_refl a)
 
 lemma nhds_within_Iic_ne_bot {a b : α} (H : a ≤ b) :
-  𝓝[Iic b] a ≠ ⊥ :=
+  ne_bot (𝓝[Iic b] a) :=
 nhds_within_ne_bot_of_mem H
 
-lemma nhds_within_Iic_self_ne_bot (a : α) :
-  𝓝[Iic a] a ≠ ⊥ :=
+@[instance] lemma nhds_within_Iic_self_ne_bot (a : α) :
+  ne_bot (𝓝[Iic a] a) :=
 nhds_within_Iic_ne_bot (le_refl a)
 
 end preorder
@@ -281,10 +281,12 @@ is_open_Iio.interior_eq
 @[simp] lemma interior_Ioo : interior (Ioo a b) = Ioo a b :=
 is_open_Ioo.interior_eq
 
+variables [topological_space γ]
+
 /-- Intermediate value theorem for two functions: if `f` and `g` are two continuous functions
 on a preconnected space and `f a ≤ g a` and `g b ≤ f b`, then for some `x` we have `f x = g x`. -/
-lemma intermediate_value_univ₂ {γ : Type*} [topological_space γ] [preconnected_space γ] {a b : γ}
-  {f g : γ → α} (hf : continuous f) (hg : continuous g) (ha : f a ≤ g a) (hb : g b ≤ f b) :
+lemma intermediate_value_univ₂ [preconnected_space γ] {a b : γ} {f g : γ → α} (hf : continuous f)
+  (hg : continuous g) (ha : f a ≤ g a) (hb : g b ≤ f b) :
   ∃ x, f x = g x :=
 begin
   obtain ⟨x, h, hfg, hgf⟩ : (univ ∩ {x | f x ≤ g x ∧ g x ≤ f x}).nonempty,
@@ -297,31 +299,29 @@ end
 /-- Intermediate value theorem for two functions: if `f` and `g` are two functions continuous
 on a preconnected set `s` and for some `a b ∈ s` we have `f a ≤ g a` and `g b ≤ f b`,
 then for some `x ∈ s` we have `f x = g x`. -/
-lemma is_preconnected.intermediate_value₂ {γ : Type*} [topological_space γ] {s : set γ}
-  (hs : is_preconnected s) {a b : γ} (ha : a ∈ s) (hb : b ∈ s) {f g : γ → α}
+lemma is_preconnected.intermediate_value₂ {s : set γ} (hs : is_preconnected s)
+  {a b : γ} (ha : a ∈ s) (hb : b ∈ s) {f g : γ → α}
   (hf : continuous_on f s) (hg : continuous_on g s) (ha' : f a ≤ g a) (hb' : g b ≤ f b) :
   ∃ x ∈ s, f x = g x :=
-let ⟨x, hx⟩ := @intermediate_value_univ₂ α _ _ _ s _ (subtype.preconnected_space hs) ⟨a, ha⟩ ⟨b, hb⟩
+let ⟨x, hx⟩ := @intermediate_value_univ₂ α s _ _ _ _ (subtype.preconnected_space hs) ⟨a, ha⟩ ⟨b, hb⟩
   _ _ (continuous_on_iff_continuous_restrict.1 hf) (continuous_on_iff_continuous_restrict.1 hg)
   ha' hb'
 in ⟨x, x.2, hx⟩
 
 /-- Intermediate Value Theorem for continuous functions on connected sets. -/
-lemma is_preconnected.intermediate_value {γ : Type*} [topological_space γ] {s : set γ}
-  (hs : is_preconnected s) {a b : γ} (ha : a ∈ s) (hb : b ∈ s) {f : γ → α}
-  (hf : continuous_on f s) :
+lemma is_preconnected.intermediate_value {s : set γ} (hs : is_preconnected s)
+  {a b : γ} (ha : a ∈ s) (hb : b ∈ s) {f : γ → α} (hf : continuous_on f s) :
   Icc (f a) (f b) ⊆ f '' s :=
 λ x hx, mem_image_iff_bex.2 $ hs.intermediate_value₂ ha hb hf continuous_on_const hx.1 hx.2
 
 /-- Intermediate Value Theorem for continuous functions on connected spaces. -/
-lemma intermediate_value_univ {γ : Type*} [topological_space γ] [preconnected_space γ]
-  (a b : γ) {f : γ → α} (hf : continuous f) :
+lemma intermediate_value_univ [preconnected_space γ] (a b : γ) {f : γ → α} (hf : continuous f) :
   Icc (f a) (f b) ⊆ range f :=
 λ x hx, intermediate_value_univ₂ hf continuous_const hx.1 hx.2
 
 /-- Intermediate Value Theorem for continuous functions on connected spaces. -/
-lemma mem_range_of_exists_le_of_exists_ge {γ : Type*} [topological_space γ] [preconnected_space γ]
-  {c : α} {f : γ → α} (hf : continuous f) (h₁ : ∃ a, f a ≤ c) (h₂ : ∃ b, c ≤ f b) :
+lemma mem_range_of_exists_le_of_exists_ge [preconnected_space γ] {c : α} {f : γ → α}
+  (hf : continuous f) (h₁ : ∃ a, f a ≤ c) (h₂ : ∃ b, c ≤ f b) :
   c ∈ range f :=
 let ⟨a, ha⟩ := h₁, ⟨b, hb⟩ := h₂ in intermediate_value_univ a b hf ⟨ha, hb⟩
 
@@ -3173,8 +3173,7 @@ noncomputable def homeomorph_of_strict_mono_continuous
   (f : α → β) (h_mono : strict_mono f) (h_cont : continuous f) (h_top : tendsto f at_top at_top)
   (h_bot : tendsto f at_bot at_bot) :
   homeomorph α β :=
-(order_iso.of_strict_mono_surjective f h_mono
-  (surjective_of_continuous h_cont h_top h_bot)).to_homeomorph
+(h_mono.order_iso_of_surjective f (surjective_of_continuous h_cont h_top h_bot)).to_homeomorph
 
 @[simp] lemma coe_homeomorph_of_strict_mono_continuous
   (f : α → β) (h_mono : strict_mono f) (h_cont : continuous f) (h_top : tendsto f at_top at_top)
@@ -3196,10 +3195,8 @@ noncomputable def homeomorph_of_strict_mono_continuous_Ioo
   (h_top : tendsto f (𝓝[Iio b] b) at_top)
   (h_bot : tendsto f (𝓝[Ioi a] a) at_bot) :
   homeomorph (Ioo a b) β :=
-@homeomorph_of_strict_mono_continuous _ _
-(@ord_connected_subset_conditionally_complete_linear_order α (Ioo a b) _
-  ⟨classical.choice (nonempty_Ioo_subtype h)⟩ _)
-_ _ _ _ _ _
+by haveI : inhabited (Ioo a b) := inhabited_of_nonempty (nonempty_Ioo_subtype h); exact
+homeomorph_of_strict_mono_continuous
 (restrict f (Ioo a b))
 (λ x y, h_mono x.2.1 y.2.2)
 (continuous_on_iff_continuous_restrict.mp h_cont)
diff --git a/src/topology/separation.lean b/src/topology/separation.lean
index dfdf33a7145c6..777576326f47d 100644
--- a/src/topology/separation.lean
+++ b/src/topology/separation.lean
@@ -65,8 +65,11 @@ class t1_space (α : Type u) [topological_space α] : Prop :=
 lemma is_closed_singleton [t1_space α] {x : α} : is_closed ({x} : set α) :=
 t1_space.t1 x
 
+lemma is_open_compl_singleton [t1_space α] {x : α} : is_open ({x}ᶜ : set α) :=
+is_closed_singleton
+
 lemma is_open_ne [t1_space α] {x : α} : is_open {y | y ≠ x} :=
-compl_singleton_eq x ▸ is_open_compl_iff.2 (t1_space.t1 x)
+is_open_compl_singleton
 
 instance subtype.t1_space {α : Type u} [topological_space α] [t1_space α] {p : α → Prop} :
   t1_space (subtype p) :=