diff --git a/archive/100-theorems-list/73_ascending_descending_sequences.lean b/archive/100-theorems-list/73_ascending_descending_sequences.lean
index 35d8df77cd006..e909d44087044 100644
--- a/archive/100-theorems-list/73_ascending_descending_sequences.lean
+++ b/archive/100-theorems-list/73_ascending_descending_sequences.lean
@@ -91,7 +91,8 @@ begin
       rw nat.lt_iff_add_one_le,
       apply le_max',
       rw mem_image at this ⊢,
-      -- In particular we take the subsequence `t` of length `a_i` which ends at `i`, by definition of `a_i`
+      -- In particular we take the subsequence `t` of length `a_i` which ends at `i`, by definition
+      -- of `a_i`
       rcases this with ⟨t, ht₁, ht₂⟩,
       rw mem_filter at ht₁,
       -- Ensure `t` ends at `i`.
@@ -107,9 +108,10 @@ begin
         { convert max_insert,
           rw [ht₁.2.1, option.lift_or_get_some_some, max_eq_left, with_top.some_eq_coe],
           apply le_of_lt ‹i < j› },
-        -- To show it's increasing (i.e., `f` is monotone increasing on `t.insert j`), we do cases on
-        -- what the possibilities could be - either in `t` or equals `j`.
-        simp only [strict_mono_incr_on, strict_mono_decr_on, coe_insert, set.mem_insert_iff, mem_coe],
+        -- To show it's increasing (i.e., `f` is monotone increasing on `t.insert j`), we do cases
+        -- on what the possibilities could be - either in `t` or equals `j`.
+        simp only [strict_mono_incr_on, strict_mono_decr_on, coe_insert, set.mem_insert_iff,
+          mem_coe],
         -- Most of the cases are just bashes.
         rintros x ⟨rfl | _⟩ y ⟨rfl | _⟩ _,
         { apply (irrefl _ ‹j < j›).elim },
@@ -138,8 +140,8 @@ begin
     simp only [mem_image, exists_prop, mem_range, mem_univ, mem_product, true_and, prod.mk.inj_iff],
     rintros ⟨i, rfl, rfl⟩,
     specialize q i,
-    -- Show `1 ≤ a_i` and `1 ≤ b_i`, which is easy from the fact that `{i}` is a increasing and decreasing
-    -- subsequence which we did right near the top.
+    -- Show `1 ≤ a_i` and `1 ≤ b_i`, which is easy from the fact that `{i}` is a increasing and
+    -- decreasing subsequence which we did right near the top.
     have z : 1 ≤ (ab i).1 ∧ 1 ≤ (ab i).2,
     { split;
       { apply le_max',
diff --git a/src/analysis/calculus/times_cont_diff.lean b/src/analysis/calculus/times_cont_diff.lean
index 6f28a7b661a54..05a74bd51699f 100644
--- a/src/analysis/calculus/times_cont_diff.lean
+++ b/src/analysis/calculus/times_cont_diff.lean
@@ -522,7 +522,7 @@ begin
       exact nhds_within_mono _ (subset_insert x u) hv },
     { rw has_ftaylor_series_up_to_on_succ_iff_right,
       refine ⟨λ y hy, rfl, λ y hy, _, _⟩,
-      { change has_fderiv_within_at (λ (z : E), (continuous_multilinear_curry_fin0 𝕜 E F).symm (f z))
+      { change has_fderiv_within_at (λ z, (continuous_multilinear_curry_fin0 𝕜 E F).symm (f z))
           ((formal_multilinear_series.unshift (p' y) (f y) 1).curry_left) (v ∩ u) y,
         rw continuous_linear_equiv.comp_has_fderiv_within_at_iff',
         convert (f'_eq_deriv y hy.2).mono (inter_subset_right v u),
diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean
index d5a418ecfa63a..ed0d159202683 100644
--- a/src/category_theory/types.lean
+++ b/src/category_theory/types.lean
@@ -86,7 +86,8 @@ namespace functor_to_types
 variables {C : Type u} [category.{v} C] (F G H : C ⥤ Type w) {X Y Z : C}
 variables (σ : F ⟶ G) (τ : G ⟶ H)
 
-@[simp] lemma map_comp_apply (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) : (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) :=
+@[simp] lemma map_comp_apply (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) :
+  (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) :=
 by simp [types_comp]
 
 @[simp] lemma map_id_apply (a : F.obj X) : (F.map (𝟙 X)) a = a :=
@@ -99,7 +100,9 @@ congr_fun (σ.naturality f) x
 
 variables {D : Type u'} [𝒟 : category.{u'} D] (I J : D ⥤ C) (ρ : I ⟶ J) {W : D}
 
-@[simp] lemma hcomp (x : (I ⋙ F).obj W) : (ρ ◫ σ).app W x = (G.map (ρ.app W)) (σ.app (I.obj W) x) := rfl
+@[simp] lemma hcomp (x : (I ⋙ F).obj W) :
+  (ρ ◫ σ).app W x = (G.map (ρ.app W)) (σ.app (I.obj W) x) :=
+rfl
 
 @[simp] lemma map_inv_map_hom_apply (f : X ≅ Y) (x : F.obj X) : F.map f.inv (F.map f.hom x) = x :=
 congr_fun (F.map_iso f).hom_inv_id x
@@ -281,15 +284,22 @@ end category_theory
 -- We prove `equiv_iso_iso` and then use that to sneakily construct `equiv_equiv_iso`.
 -- (In this order the proofs are handled by `obviously`.)
 
-/-- equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms of types -/
+/-- Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms
+of types. -/
 @[simps] def equiv_iso_iso {X Y : Type u} : (X ≃ Y) ≅ (X ≅ Y) :=
 { hom := λ e, e.to_iso,
   inv := λ i, i.to_equiv, }
 
-/-- equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms of types -/
--- We leave `X` and `Y` as explicit arguments here, because the coercions from `equiv` to a function won't fire without them.
+/-- Equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms
+of types. -/
+-- We leave `X` and `Y` as explicit arguments here, because the coercions from `equiv` to a function
+-- won't fire without them.
+-- TODO: is it still true?
 def equiv_equiv_iso (X Y : Type u) : (X ≃ Y) ≃ (X ≅ Y) :=
 (equiv_iso_iso).to_equiv
 
-@[simp] lemma equiv_equiv_iso_hom {X Y : Type u} (e : X ≃ Y) : (equiv_equiv_iso X Y) e = e.to_iso := rfl
-@[simp] lemma equiv_equiv_iso_inv {X Y : Type u} (e : X ≅ Y) : (equiv_equiv_iso X Y).symm e = e.to_equiv := rfl
+@[simp] lemma equiv_equiv_iso_hom {X Y : Type u} (e : X ≃ Y) :
+  (equiv_equiv_iso X Y) e = e.to_iso := rfl
+
+@[simp] lemma equiv_equiv_iso_inv {X Y : Type u} (e : X ≅ Y) :
+  (equiv_equiv_iso X Y).symm e = e.to_equiv := rfl
diff --git a/src/computability/tm_computable.lean b/src/computability/tm_computable.lean
index 1bec3d8af86db..a499db7266238 100644
--- a/src/computability/tm_computable.lean
+++ b/src/computability/tm_computable.lean
@@ -92,9 +92,10 @@ structure evals_to {σ : Type*} (f : σ → option σ) (a : σ) (b : option σ)
 (steps : ℕ)
 (evals_in_steps : ((flip bind f)^[steps] a) = b)
 
-/-- A "proof" of the fact that f eventually reaches b in at most m steps when repeatedly evaluated on a,
-remembering the number of steps it takes. -/
-structure evals_to_in_time {σ : Type*} (f : σ → option σ) (a : σ) (b : option σ) (m : ℕ) extends evals_to f a b :=
+/-- A "proof" of the fact that `f` eventually reaches `b` in at most `m` steps when repeatedly
+evaluated on `a`, remembering the number of steps it takes. -/
+structure evals_to_in_time {σ : Type*} (f : σ → option σ) (a : σ) (b : option σ) (m : ℕ)
+  extends evals_to f a b :=
 (steps_le_m : steps ≤ m)
 
 /-- Reflexivity of `evals_to` in 0 steps. -/
@@ -107,7 +108,8 @@ structure evals_to_in_time {σ : Type*} (f : σ → option σ) (a : σ) (b : opt
  by rw [function.iterate_add_apply,h₁.evals_in_steps,h₂.evals_in_steps]⟩
 
 /-- Reflexivity of `evals_to_in_time` in 0 steps. -/
-@[refl] def evals_to_in_time.refl {σ : Type*} (f : σ → option σ) (a : σ) : evals_to_in_time f a a 0 :=
+@[refl] def evals_to_in_time.refl {σ : Type*} (f : σ → option σ) (a : σ) :
+  evals_to_in_time f a a 0 :=
 ⟨evals_to.refl f a, le_refl 0⟩
 
 /-- Transitivity of `evals_to_in_time` in the sum of the numbers of steps. -/
@@ -121,12 +123,14 @@ def tm2_outputs (tm : fin_tm2) (l : list (tm.Γ tm.k₀)) (l' : option (list (tm
 evals_to tm.step (init_list tm l) ((option.map (halt_list tm)) l')
 
 /-- A proof of tm outputting l' when given l in at most m steps. -/
-def tm2_outputs_in_time (tm : fin_tm2) (l : list (tm.Γ tm.k₀)) (l' : option (list (tm.Γ tm.k₁))) (m : ℕ) :=
+def tm2_outputs_in_time (tm : fin_tm2) (l : list (tm.Γ tm.k₀))
+  (l' : option (list (tm.Γ tm.k₁))) (m : ℕ) :=
 evals_to_in_time tm.step (init_list tm l) ((option.map (halt_list tm)) l') m
 
 /-- The forgetful map, forgetting the upper bound on the number of steps. -/
 def tm2_outputs_in_time.to_tm2_outputs {tm : fin_tm2} {l : list (tm.Γ tm.k₀)}
-{l' : option (list (tm.Γ tm.k₁))} {m : ℕ} (h : tm2_outputs_in_time tm l l' m) : tm2_outputs tm l l' :=
+{l' : option (list (tm.Γ tm.k₁))} {m : ℕ} (h : tm2_outputs_in_time tm l l' m) :
+  tm2_outputs tm l l' :=
 h.to_evals_to
 
 /-- A Turing machine with input alphabet equivalent to Γ₀ and output alphabet equivalent to Γ₁. -/
@@ -142,15 +146,18 @@ structure tm2_computable {α β : Type} (ea : fin_encoding α) (eb : fin_encodin
   (option.some ((list.map output_alphabet.inv_fun) (eb.encode (f a)))) )
 
 /-- A Turing machine + a time function + a proof it outputs f in at most time(len(input)) steps. -/
-structure tm2_computable_in_time {α β : Type} (ea : fin_encoding α) (eb : fin_encoding β) (f : α → β)
+structure tm2_computable_in_time {α β : Type} (ea : fin_encoding α) (eb : fin_encoding β)
+  (f : α → β)
   extends tm2_computable_aux ea.Γ eb.Γ :=
 ( time: ℕ → ℕ )
 ( outputs_fun : ∀ a, tm2_outputs_in_time tm (list.map input_alphabet.inv_fun (ea.encode a))
   (option.some ((list.map output_alphabet.inv_fun) (eb.encode (f a))))
   (time (ea.encode a).length) )
 
-/-- A Turing machine + a polynomial time function + a proof it outputs f in at most time(len(input)) steps. -/
-structure tm2_computable_in_poly_time {α β : Type} (ea : fin_encoding α) (eb : fin_encoding β) (f : α → β)
+/-- A Turing machine + a polynomial time function + a proof it outputs f in at most time(len(input))
+steps. -/
+structure tm2_computable_in_poly_time {α β : Type} (ea : fin_encoding α) (eb : fin_encoding β)
+  (f : α → β)
   extends tm2_computable_aux ea.Γ eb.Γ :=
 ( time: polynomial ℕ )
 ( outputs_fun : ∀ a, tm2_outputs_in_time tm (list.map input_alphabet.inv_fun (ea.encode a))
@@ -158,13 +165,15 @@ structure tm2_computable_in_poly_time {α β : Type} (ea : fin_encoding α) (eb
   (time.eval (ea.encode a).length) )
 
 /-- A forgetful map, forgetting the time bound on the number of steps. -/
-def tm2_computable_in_time.to_tm2_computable {α β : Type} {ea : fin_encoding α} {eb : fin_encoding β}
-{f : α → β} (h : tm2_computable_in_time ea eb f) : tm2_computable ea eb f :=
+def tm2_computable_in_time.to_tm2_computable {α β : Type} {ea : fin_encoding α}
+  {eb : fin_encoding β} {f : α → β} (h : tm2_computable_in_time ea eb f) :
+  tm2_computable ea eb f :=
 ⟨h.to_tm2_computable_aux, λ a, tm2_outputs_in_time.to_tm2_outputs (h.outputs_fun a)⟩
 
 /-- A forgetful map, forgetting that the time function is polynomial. -/
 def tm2_computable_in_poly_time.to_tm2_computable_in_time {α β : Type} {ea : fin_encoding α}
-{eb : fin_encoding β} {f : α → β} (h : tm2_computable_in_poly_time ea eb f) : tm2_computable_in_time ea eb f :=
+  {eb : fin_encoding β} {f : α → β} (h : tm2_computable_in_poly_time ea eb f) :
+  tm2_computable_in_time ea eb f :=
 ⟨h.to_tm2_computable_aux, λ n, h.time.eval n, h.outputs_fun⟩
 
 open turing.TM2.stmt
@@ -188,7 +197,8 @@ instance inhabited_fin_tm2 : inhabited fin_tm2 :=
 noncomputable theory
 
 /-- A proof that the identity map on α is computable in polytime. -/
-def id_computable_in_poly_time {α : Type} (ea : fin_encoding α) : @tm2_computable_in_poly_time α α ea ea id :=
+def id_computable_in_poly_time {α : Type} (ea : fin_encoding α) :
+  @tm2_computable_in_poly_time α α ea ea id :=
 { tm := id_computer ea,
   input_alphabet := equiv.cast rfl,
   output_alphabet := equiv.cast rfl,
@@ -201,33 +211,36 @@ instance inhabited_tm2_computable_in_poly_time : inhabited (tm2_computable_in_po
 (default (fin_encoding bool)) (default (fin_encoding bool)) id) :=
 ⟨id_computable_in_poly_time computability.inhabited_fin_encoding.default⟩
 
-instance inhabited_tm2_outputs_in_time : inhabited (tm2_outputs_in_time (id_computer fin_encoding_bool_bool)
-(list.map (equiv.cast rfl).inv_fun [ff]) (some (list.map (equiv.cast rfl).inv_fun [ff])) _)
- :=
+instance inhabited_tm2_outputs_in_time :
+  inhabited (tm2_outputs_in_time (id_computer fin_encoding_bool_bool)
+    (list.map (equiv.cast rfl).inv_fun [ff]) (some (list.map (equiv.cast rfl).inv_fun [ff])) _) :=
 ⟨(id_computable_in_poly_time fin_encoding_bool_bool).outputs_fun ff⟩
 
 instance inhabited_tm2_outputs : inhabited (tm2_outputs (id_computer fin_encoding_bool_bool)
 (list.map (equiv.cast rfl).inv_fun [ff]) (some (list.map (equiv.cast rfl).inv_fun [ff]))) :=
 ⟨tm2_outputs_in_time.to_tm2_outputs turing.inhabited_tm2_outputs_in_time.default⟩
 
-instance inhabited_evals_to_in_time : inhabited (evals_to_in_time (λ _ : unit, some ⟨⟩) ⟨⟩ (some ⟨⟩) 0)
-:= ⟨evals_to_in_time.refl _ _⟩
+instance inhabited_evals_to_in_time :
+  inhabited (evals_to_in_time (λ _ : unit, some ⟨⟩) ⟨⟩ (some ⟨⟩) 0) :=
+⟨evals_to_in_time.refl _ _⟩
 
-instance inhabited_tm2_evals_to : inhabited (evals_to (λ _ : unit, some ⟨⟩) ⟨⟩ (some ⟨⟩))
-:= ⟨evals_to.refl _ _⟩
+instance inhabited_tm2_evals_to : inhabited (evals_to (λ _ : unit, some ⟨⟩) ⟨⟩ (some ⟨⟩)) :=
+⟨evals_to.refl _ _⟩
 
 /-- A proof that the identity map on α is computable in time. -/
 def id_computable_in_time {α : Type} (ea : fin_encoding α) : @tm2_computable_in_time α α ea ea id :=
 tm2_computable_in_poly_time.to_tm2_computable_in_time $ id_computable_in_poly_time ea
 
-instance inhabited_tm2_computable_in_time : inhabited (tm2_computable_in_time fin_encoding_bool_bool fin_encoding_bool_bool id) :=
+instance inhabited_tm2_computable_in_time :
+  inhabited (tm2_computable_in_time fin_encoding_bool_bool fin_encoding_bool_bool id) :=
 ⟨id_computable_in_time computability.inhabited_fin_encoding.default⟩
 
 /-- A proof that the identity map on α is computable. -/
 def id_computable {α : Type} (ea : fin_encoding α) : @tm2_computable α α ea ea id :=
 tm2_computable_in_time.to_tm2_computable $ id_computable_in_time ea
 
-instance inhabited_tm2_computable : inhabited (tm2_computable fin_encoding_bool_bool fin_encoding_bool_bool id) :=
+instance inhabited_tm2_computable :
+  inhabited (tm2_computable fin_encoding_bool_bool fin_encoding_bool_bool id) :=
 ⟨id_computable computability.inhabited_fin_encoding.default⟩
 
 instance inhabited_tm2_computable_aux : inhabited (tm2_computable_aux bool bool) :=
diff --git a/src/data/fintype/card.lean b/src/data/fintype/card.lean
index ec5cf5d9f482a..aea2637a40ca5 100644
--- a/src/data/fintype/card.lean
+++ b/src/data/fintype/card.lean
@@ -126,7 +126,8 @@ end
 
 /-- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
 is the sum of `f x`, for some `x : fin (n + 1)` plus the remaining product -/
-theorem fin.sum_univ_succ_above [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) (x : fin (n + 1)) :
+theorem fin.sum_univ_succ_above [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β)
+  (x : fin (n + 1)) :
   ∑ i, f i = f x + ∑ i : fin n, f (x.succ_above i) :=
 by apply @fin.prod_univ_succ_above (multiplicative β)
 
@@ -196,7 +197,8 @@ by rw fintype.of_equiv_card; simp
 @[simp, to_additive]
 lemma finset.prod_attach_univ [fintype α] [comm_monoid β] (f : {a : α // a ∈ @univ α _} → β) :
   ∏ x in univ.attach, f x = ∏ x, f ⟨x, (mem_univ _)⟩ :=
-prod_bij (λ x _, x.1) (λ _ _, mem_univ _) (λ _ _ , by simp) (by simp) (λ b _, ⟨⟨b, mem_univ _⟩, by simp⟩)
+prod_bij (λ x _, x.1) (λ _ _, mem_univ _) (λ _ _ , by simp) (by simp)
+  (λ b _, ⟨⟨b, mem_univ _⟩, by simp⟩)
 
 /-- Taking a product over `univ.pi t` is the same as taking the product over `fintype.pi_finset t`.
   `univ.pi t` and `fintype.pi_finset t` are essentially the same `finset`, but differ
diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index 4cb2d49725d1f..92706a397bd83 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -1688,7 +1688,8 @@ lemma reverse_take {α} {xs : list α} (n : ℕ)
   (h : n ≤ xs.length) :
   xs.reverse.take n = (xs.drop (xs.length - n)).reverse :=
 begin
-  induction xs generalizing n; simp only [reverse_cons, drop, reverse_nil, nat.zero_sub, length, take_nil],
+  induction xs generalizing n;
+    simp only [reverse_cons, drop, reverse_nil, nat.zero_sub, length, take_nil],
   cases decidable.lt_or_eq_of_le h with h' h',
   { replace h' := le_of_succ_le_succ h',
     rwa [take_append_of_le_length, xs_ih _ h'],
@@ -1696,7 +1697,8 @@ begin
     { rwa [succ_eq_add_one, nat.sub_add_comm] },
     { rwa length_reverse } },
   { subst h', rw [length, nat.sub_self, drop],
-    rw [show xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length, from _, take_length, reverse_cons],
+    suffices : xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length,
+      by rw [this, take_length, reverse_cons],
     rw [length_append, length_reverse], refl }
 end
 
diff --git a/src/data/list/nodup.lean b/src/data/list/nodup.lean
index b5c433ee453a0..ec6d0989c2cac 100644
--- a/src/data/list/nodup.lean
+++ b/src/data/list/nodup.lean
@@ -9,7 +9,8 @@ import data.list.forall2
 /-!
 # Lists with no duplicates
 
-`list.nodup` is defined in `data/list/defs`. In this file we prove various properties of this predicate.
+`list.nodup` is defined in `data/list/defs`. In this file we prove various properties of this
+predicate.
 -/
 
 universes u v
diff --git a/src/data/list/pairwise.lean b/src/data/list/pairwise.lean
index c1fb71140444f..52f09c5d10914 100644
--- a/src/data/list/pairwise.lean
+++ b/src/data/list/pairwise.lean
@@ -248,7 +248,8 @@ theorem pairwise_sublists' {R} : ∀ {l : list α}, pairwise R l →
 | _ pairwise.nil := pairwise_singleton _ _
 | _ (@pairwise.cons _ _ a l H₁ H₂) :=
   begin
-    simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp_distrib, and_imp],
+    simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map,
+      exists_imp_distrib, and_imp],
     have IH := pairwise_sublists' H₂,
     refine ⟨IH, IH.imp (λ l₁ l₂, lex.cons), _⟩,
     intros l₁ sl₁ x l₂ sl₂ e, subst e,
@@ -273,7 +274,8 @@ variable [decidable_rel R]
 @[simp] theorem pw_filter_cons_of_neg {a : α} {l : list α} (h : ¬ ∀ b ∈ pw_filter R l, R a b) :
   pw_filter R (a::l) = pw_filter R l := if_neg h
 
-theorem pw_filter_map (f : β → α) : Π (l : list β), pw_filter R (map f l) = map f (pw_filter (λ x y, R (f x) (f y)) l)
+theorem pw_filter_map (f : β → α) :
+  Π (l : list β), pw_filter R (map f l) = map f (pw_filter (λ x y, R (f x) (f y)) l)
 | [] := rfl
 | (x :: xs) :=
   if h : ∀ b ∈ pw_filter R (map f xs), R (f x) b
diff --git a/src/data/list/perm.lean b/src/data/list/perm.lean
index b534af076646b..54167f16979e9 100644
--- a/src/data/list/perm.lean
+++ b/src/data/list/perm.lean
@@ -756,7 +756,8 @@ by { dsimp [(∩), list.inter], congr, funext a, rw [p.mem_iff] }
 theorem perm.inter {l₁ l₂ t₁ t₂ : list α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ∩ t₁ ~ l₂ ∩ t₂ :=
 p₂.inter_left l₂ ▸ p₁.inter_right t₁
 
-theorem perm.inter_append {l t₁ t₂ : list α} (h : disjoint t₁ t₂) : l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂ :=
+theorem perm.inter_append {l t₁ t₂ : list α} (h : disjoint t₁ t₂) :
+  l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂ :=
 begin
   induction l,
   case list.nil
diff --git a/src/data/list/range.lean b/src/data/list/range.lean
index 99ba2b4537d6a..9943c72f0ed93 100644
--- a/src/data/list/range.lean
+++ b/src/data/list/range.lean
@@ -141,7 +141,8 @@ by simp only [range_eq_range', range'_concat, zero_add]
 
 theorem iota_eq_reverse_range' : ∀ n : ℕ, iota n = reverse (range' 1 n)
 | 0     := rfl
-| (n+1) := by simp only [iota, range'_concat, iota_eq_reverse_range' n, reverse_append, add_comm]; refl
+| (n+1) := by simp only [iota, range'_concat, iota_eq_reverse_range' n,
+             reverse_append, add_comm]; refl
 
 @[simp] theorem length_iota (n : ℕ) : length (iota n) = n :=
 by simp only [iota_eq_reverse_range', length_reverse, length_range']
diff --git a/src/data/list/sections.lean b/src/data/list/sections.lean
index ad6dc99d1e54d..74326e1a4bb2a 100644
--- a/src/data/list/sections.lean
+++ b/src/data/list/sections.lean
@@ -29,7 +29,8 @@ end
 theorem mem_sections_length {L : list (list α)} {f} (h : f ∈ sections L) : length f = length L :=
 forall₂_length_eq (mem_sections.1 h)
 
-lemma rel_sections {r : α → β → Prop} : (forall₂ (forall₂ r) ⇒ forall₂ (forall₂ r)) sections sections
+lemma rel_sections {r : α → β → Prop} :
+  (forall₂ (forall₂ r) ⇒ forall₂ (forall₂ r)) sections sections
 | _ _ forall₂.nil := forall₂.cons forall₂.nil forall₂.nil
 | _ _ (forall₂.cons h₀ h₁) :=
   rel_bind (rel_sections h₁) (assume _ _ hl, rel_map (assume _ _ ha, forall₂.cons ha hl) h₀)
diff --git a/src/data/list/sigma.lean b/src/data/list/sigma.lean
index 2083a8c245397..a8cd0ad82d715 100644
--- a/src/data/list/sigma.lean
+++ b/src/data/list/sigma.lean
@@ -472,7 +472,8 @@ else if ha₁ : a₁ ∈ l.keys then
 else
   by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]
 
-lemma sizeof_kerase {α} {β : α → Type*} [decidable_eq α] [has_sizeof (sigma β)] (x : α) (xs : list (sigma β)) :
+lemma sizeof_kerase {α} {β : α → Type*} [decidable_eq α] [has_sizeof (sigma β)] (x : α)
+  (xs : list (sigma β)) :
   sizeof (list.kerase x xs) ≤ sizeof xs :=
 begin
   unfold_wf,
@@ -556,7 +557,8 @@ begin
   { rw [erase_dupkeys_cons,lookup_kinsert_ne h,l_ih,lookup_cons_ne], exact h },
 end
 
-lemma sizeof_erase_dupkeys {α} {β : α → Type*} [decidable_eq α] [has_sizeof (sigma β)] (xs : list (sigma β)) :
+lemma sizeof_erase_dupkeys {α} {β : α → Type*} [decidable_eq α] [has_sizeof (sigma β)]
+  (xs : list (sigma β)) :
   sizeof (list.erase_dupkeys xs) ≤ sizeof xs :=
 begin
   unfold_wf,
diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean
index 356a20ac83bef..bf77dbefbf6c3 100644
--- a/src/data/matrix/basic.lean
+++ b/src/data/matrix/basic.lean
@@ -335,10 +335,12 @@ diagonal_dot_product _ _ _
   (d : n → α) (M : matrix m n α) (i j) : (M ⬝ diagonal d) i j = M i j * d j :=
 by { rw ← diagonal_transpose, apply dot_product_diagonal }
 
-@[simp] protected theorem one_mul [decidable_eq m] (M : matrix m n α) : (1 : matrix m m α) ⬝ M = M :=
+@[simp] protected theorem one_mul [decidable_eq m] (M : matrix m n α) :
+  (1 : matrix m m α) ⬝ M = M :=
 by ext i j; rw [← diagonal_one, diagonal_mul, one_mul]
 
-@[simp] protected theorem mul_one [decidable_eq n] (M : matrix m n α) : M ⬝ (1 : matrix n n α) = M :=
+@[simp] protected theorem mul_one [decidable_eq n] (M : matrix m n α) :
+  M ⬝ (1 : matrix n n α) = M :=
 by ext i j; rw [← diagonal_one, mul_diagonal, mul_one]
 
 instance [decidable_eq n] : monoid (matrix n n α) :=
@@ -497,7 +499,8 @@ instance [semiring α] : has_scalar α (matrix m n α) := pi.has_scalar
 instance {β : Type w} [semiring α] [add_comm_monoid β] [semimodule α β] :
   semimodule α (matrix m n β) := pi.semimodule _ _ _
 
-@[simp] lemma smul_apply [semiring α] (a : α) (A : matrix m n α) (i : m) (j : n) : (a • A) i j = a * A i j := rfl
+@[simp] lemma smul_apply [semiring α] (a : α) (A : matrix m n α) (i : m) (j : n) :
+  (a • A) i j = a * A i j := rfl
 
 section semiring
 variables [semiring α]
@@ -866,9 +869,11 @@ Simplification lemmas for `matrix.row` and `matrix.col`.
 open_locale matrix
 
 @[simp] lemma col_add [semiring α] (v w : m → α) : col (v + w) = col v + col w := by { ext, refl }
-@[simp] lemma col_smul [semiring α] (x : α) (v : m → α) : col (x • v) = x • col v := by { ext, refl }
+@[simp] lemma col_smul [semiring α] (x : α) (v : m → α) : col (x • v) = x • col v :=
+by { ext, refl }
 @[simp] lemma row_add [semiring α] (v w : m → α) : row (v + w) = row v + row w := by { ext, refl }
-@[simp] lemma row_smul [semiring α] (x : α) (v : m → α) : row (x • v) = x • row v := by { ext, refl }
+@[simp] lemma row_smul [semiring α] (x : α) (v : m → α) : row (x • v) = x • row v :=
+by { ext, refl }
 
 @[simp] lemma col_apply (v : m → α) (i j) : matrix.col v i j = v i := rfl
 @[simp] lemma row_apply (v : m → α) (i j) : matrix.row v i j = v j := rfl
@@ -921,7 +926,8 @@ begin
   { rwa [update_row_ne h, if_neg h] }
 end
 
-lemma update_column_apply [decidable_eq m] {j' : m} : update_column M j c i j' = if j' = j then c i else M i j' :=
+lemma update_column_apply [decidable_eq m] {j' : m} :
+  update_column M j c i j' = if j' = j then c i else M i j' :=
 begin
   by_cases j' = j,
   { rw [h, update_column_self, if_pos rfl] },
diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean
index 524bcd71b6f4f..5c6fa01b53389 100644
--- a/src/data/mv_polynomial/basic.lean
+++ b/src/data/mv_polynomial/basic.lean
@@ -103,7 +103,8 @@ instance : has_scalar R (mv_polynomial σ R) := add_monoid_algebra.has_scalar
 instance : semimodule R (mv_polynomial σ R) := add_monoid_algebra.semimodule
 instance : algebra R (mv_polynomial σ R) := add_monoid_algebra.algebra
 
-/-- the coercion turning an `mv_polynomial` into the function which reports the coefficient of a given monomial -/
+/-- The coercion turning an `mv_polynomial` into the function which reports the coefficient
+of a given monomial. -/
 def coeff_coe_to_fun : has_coe_to_fun (mv_polynomial σ R) :=
 finsupp.has_coe_to_fun
 
@@ -166,7 +167,8 @@ instance infinite_of_infinite (σ : Type*) (R : Type*) [comm_semiring R] [infini
   infinite (mv_polynomial σ R) :=
 infinite.of_injective C (C_injective _ _)
 
-instance infinite_of_nonempty (σ : Type*) (R : Type*) [nonempty σ] [comm_semiring R] [nontrivial R] :
+instance infinite_of_nonempty (σ : Type*) (R : Type*) [nonempty σ] [comm_semiring R]
+  [nontrivial R] :
   infinite (mv_polynomial σ R) :=
 infinite.of_injective (λ i : ℕ, monomial (single (classical.arbitrary σ) i) 1)
 begin
@@ -516,8 +518,8 @@ end constant_coeff
 
 section as_sum
 
-@[simp]
-lemma support_sum_monomial_coeff (p : mv_polynomial σ R) : ∑ v in p.support, monomial v (coeff v p) = p :=
+@[simp] lemma support_sum_monomial_coeff (p : mv_polynomial σ R) :
+  ∑ v in p.support, monomial v (coeff v p) = p :=
 finsupp.sum_single p
 
 lemma as_sum (p : mv_polynomial σ R) : p = ∑ v in p.support, monomial v (coeff v p) :=
@@ -822,7 +824,7 @@ eval₂_map f g φ p
 coeff_map f φ 0
 
 lemma constant_coeff_comp_map (f : R →+* S₁) :
-  (constant_coeff : mv_polynomial σ S₁ →+* S₁).comp (mv_polynomial.map f) = f.comp (constant_coeff) :=
+  (constant_coeff : mv_polynomial σ S₁ →+* S₁).comp (mv_polynomial.map f) = f.comp constant_coeff :=
 by { ext; simp }
 
 lemma support_map_subset (p : mv_polynomial σ R) : (map f p).support ⊆ p.support :=
diff --git a/src/data/mv_polynomial/monad.lean b/src/data/mv_polynomial/monad.lean
index aa55345fa1bc2..c0cb532b70256 100644
--- a/src/data/mv_polynomial/monad.lean
+++ b/src/data/mv_polynomial/monad.lean
@@ -194,7 +194,8 @@ lemma bind₂_comp_bind₂ (f : R →+* mv_polynomial σ S) (g : S →+* mv_poly
   (bind₂ g).comp (bind₂ f) = bind₂ ((bind₂ g).comp f) :=
 by { ext1; simp }
 
-lemma bind₂_bind₂ (f : R →+* mv_polynomial σ S) (g : S →+* mv_polynomial σ T) (φ : mv_polynomial σ R) :
+lemma bind₂_bind₂ (f : R →+* mv_polynomial σ S) (g : S →+* mv_polynomial σ T)
+  (φ : mv_polynomial σ R) :
   (bind₂ g) (bind₂ f φ) = bind₂ ((bind₂ g).comp f) φ :=
 ring_hom.congr_fun (bind₂_comp_bind₂ f g) φ
 
@@ -244,7 +245,8 @@ lemma eval₂_hom_comp_C (f : R →+* S) (g : σ → S) :
   (eval₂_hom f g).comp C = f :=
 by { ext1 r, exact eval₂_C f g r }
 
-lemma eval₂_hom_bind₁ (f : R →+* S) (g : τ → S) (h : σ → mv_polynomial τ R) (φ : mv_polynomial σ R) :
+lemma eval₂_hom_bind₁ (f : R →+* S) (g : τ → S) (h : σ → mv_polynomial τ R)
+  (φ : mv_polynomial σ R) :
   eval₂_hom f g (bind₁ h φ) = eval₂_hom f (λ i, eval₂_hom f g (h i)) φ :=
 by rw [hom_bind₁, eval₂_hom_comp_C]
 
@@ -260,7 +262,8 @@ lemma eval₂_hom_comp_bind₂ (f : S →+* T) (g : σ → T) (h : R →+* mv_po
   (eval₂_hom f g).comp (bind₂ h) = eval₂_hom ((eval₂_hom f g).comp h) g :=
 by { ext1; simp }
 
-lemma eval₂_hom_bind₂ (f : S →+* T) (g : σ → T) (h : R →+* mv_polynomial σ S) (φ : mv_polynomial σ R) :
+lemma eval₂_hom_bind₂ (f : S →+* T) (g : σ → T) (h : R →+* mv_polynomial σ S)
+  (φ : mv_polynomial σ R) :
   eval₂_hom f g (bind₂ h φ) = eval₂_hom ((eval₂_hom f g).comp h) g φ :=
 ring_hom.congr_fun (eval₂_hom_comp_bind₂ f g h) φ
 
diff --git a/src/geometry/manifold/mfderiv.lean b/src/geometry/manifold/mfderiv.lean
index 8c4990d07ae5e..72f358f936450 100644
--- a/src/geometry/manifold/mfderiv.lean
+++ b/src/geometry/manifold/mfderiv.lean
@@ -59,10 +59,10 @@ of `f` in these charts.
 
 Due to the fact that we are working in a model with corners, with an additional embedding `I` of the
 model space `H` in the model vector space `E`, the charts taking values in `E` are not the original
-charts of the manifold, but those ones composed with `I`, called extended charts. We
-define `written_in_ext_chart I I' x f` for the function `f` written in the preferred extended charts.
-Then the manifold derivative of `f`, at `x`, is just the usual derivative of
-`written_in_ext_chart I I' x f`, at the point `(ext_chart_at I x) x`.
+charts of the manifold, but those ones composed with `I`, called extended charts. We define
+`written_in_ext_chart I I' x f` for the function `f` written in the preferred extended charts.  Then
+the manifold derivative of `f`, at `x`, is just the usual derivative of `written_in_ext_chart I I' x
+f`, at the point `(ext_chart_at I x) x`.
 
 There is a subtelty with respect to continuity: if the function is not continuous, then the image
 of a small open set around `x` will not be contained in the source of the preferred chart around
@@ -210,14 +210,16 @@ has_fderiv_within_at (written_in_ext_chart_at I I' x f : E → E') f' (range I)
 /-- Let `f` be a function between two smooth manifolds. Then `mfderiv_within I I' f s x` is the
 derivative of `f` at `x` within `s`, as a continuous linear map from the tangent space at `x` to the
 tangent space at `f x`. -/
-def mfderiv_within (f : M → M') (s : set M) (x : M) : tangent_space I x →L[𝕜] tangent_space I' (f x) :=
+def mfderiv_within (f : M → M') (s : set M) (x : M) :
+  tangent_space I x →L[𝕜] tangent_space I' (f x) :=
 if h : mdifferentiable_within_at I I' f s x then
 (fderiv_within 𝕜 (written_in_ext_chart_at I I' x f) ((ext_chart_at I x).symm ⁻¹' s ∩ range I)
   ((ext_chart_at I x) x) : _)
 else 0
 
 /-- Let `f` be a function between two smooth manifolds. Then `mfderiv I I' f x` is the derivative of
-`f` at `x`, as a continuous linear map from the tangent space at `x` to the tangent space at `f x`. -/
+`f` at `x`, as a continuous linear map from the tangent space at `x` to the tangent space at
+`f x`. -/
 def mfderiv (f : M → M') (x : M) : tangent_space I x →L[𝕜] tangent_space I' (f x) :=
 if h : mdifferentiable_at I I' f x then
 (fderiv_within 𝕜 (written_in_ext_chart_at I I' x f : E → E') (range I)
@@ -294,7 +296,8 @@ begin
   rwa univ_inter at this
 end
 
-lemma unique_mdiff_on.inter (hs : unique_mdiff_on I s) (ht : is_open t) : unique_mdiff_on I (s ∩ t) :=
+lemma unique_mdiff_on.inter (hs : unique_mdiff_on I s) (ht : is_open t) :
+  unique_mdiff_on I (s ∩ t) :=
 λx hx, unique_mdiff_within_at.inter (hs _ hx.1) (mem_nhds_sets ht hx.2)
 
 lemma is_open.unique_mdiff_on (hs : is_open s) : unique_mdiff_on I s :=
@@ -313,11 +316,13 @@ variables [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_co
 
 /-- `unique_mdiff_within_at` achieves its goal: it implies the uniqueness of the derivative. -/
 theorem unique_mdiff_within_at.eq (U : unique_mdiff_within_at I s x)
-  (h : has_mfderiv_within_at I I' f s x f') (h₁ : has_mfderiv_within_at I I' f s x f₁') : f' = f₁' :=
+  (h : has_mfderiv_within_at I I' f s x f') (h₁ : has_mfderiv_within_at I I' f s x f₁') :
+  f' = f₁' :=
 U.eq h.2 h₁.2
 
 theorem unique_mdiff_on.eq (U : unique_mdiff_on I s) (hx : x ∈ s)
-  (h : has_mfderiv_within_at I I' f s x f') (h₁ : has_mfderiv_within_at I I' f s x f₁') : f' = f₁' :=
+  (h : has_mfderiv_within_at I I' f s x f') (h₁ : has_mfderiv_within_at I I' f s x f₁') :
+  f' = f₁' :=
 unique_mdiff_within_at.eq (U _ hx) h h₁
 
 
@@ -406,7 +411,8 @@ lemma has_mfderiv_within_at.nhds_within (h : has_mfderiv_within_at I I' f s x f'
   (ht : s ∈ 𝓝[t] x) : has_mfderiv_within_at I I' f t x f' :=
 (has_mfderiv_within_at_inter' ht).1 (h.mono (inter_subset_right _ _))
 
-lemma has_mfderiv_within_at.has_mfderiv_at (h : has_mfderiv_within_at I I' f s x f') (hs : s ∈ 𝓝 x) :
+lemma has_mfderiv_within_at.has_mfderiv_at (h : has_mfderiv_within_at I I' f s x f')
+  (hs : s ∈ 𝓝 x) :
   has_mfderiv_at I I' f x f' :=
 by rwa [← univ_inter s, has_mfderiv_within_at_inter hs, has_mfderiv_within_at_univ] at h
 
@@ -511,7 +517,8 @@ lemma mdifferentiable.mdifferentiable_on
 (mdifferentiable_on_univ.2 h).mono (subset_univ _)
 
 lemma mdifferentiable_on_of_locally_mdifferentiable_on
-  (h : ∀x∈s, ∃u, is_open u ∧ x ∈ u ∧ mdifferentiable_on I I' f (s ∩ u)) : mdifferentiable_on I I' f s :=
+  (h : ∀x∈s, ∃u, is_open u ∧ x ∈ u ∧ mdifferentiable_on I I' f (s ∩ u)) :
+  mdifferentiable_on I I' f s :=
 begin
   assume x xs,
   rcases h x xs with ⟨t, t_open, xt, ht⟩,
@@ -644,12 +651,14 @@ end
 variables {I I'}
 
 lemma mdifferentiable_within_at.congr_mono (h : mdifferentiable_within_at I I' f s x)
-  (ht : ∀x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) : mdifferentiable_within_at I I' f₁ t x :=
+  (ht : ∀x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) :
+  mdifferentiable_within_at I I' f₁ t x :=
 (has_mfderiv_within_at.congr_mono h.has_mfderiv_within_at ht hx h₁).mdifferentiable_within_at
 
 lemma mdifferentiable_within_at.congr (h : mdifferentiable_within_at I I' f s x)
   (ht : ∀x ∈ s, f₁ x = f x) (hx : f₁ x = f x) : mdifferentiable_within_at I I' f₁ s x :=
-(has_mfderiv_within_at.congr_mono h.has_mfderiv_within_at ht hx (subset.refl _)).mdifferentiable_within_at
+(has_mfderiv_within_at.congr_mono h.has_mfderiv_within_at ht hx
+  (subset.refl _)).mdifferentiable_within_at
 
 lemma mdifferentiable_on.congr_mono (h : mdifferentiable_on I I' f s) (h' : ∀x ∈ t, f₁ x = f x)
   (h₁ : t ⊆ s) : mdifferentiable_on I I' f₁ t :=
@@ -710,7 +719,8 @@ lemma written_in_ext_chart_comp (h : continuous_within_at f s x) :
 begin
   apply @filter.mem_sets_of_superset _ _
     ((f ∘ (ext_chart_at I x).symm)⁻¹' (ext_chart_at I' (f x)).source) _
-    (ext_chart_preimage_mem_nhds_within I x (h.preimage_mem_nhds_within (ext_chart_at_source_mem_nhds _ _))),
+    (ext_chart_preimage_mem_nhds_within I x
+      (h.preimage_mem_nhds_within (ext_chart_at_source_mem_nhds _ _))),
   mfld_set_tac,
 end
 
@@ -783,7 +793,8 @@ lemma mdifferentiable_at.comp
 lemma mfderiv_within_comp
   (hg : mdifferentiable_within_at I' I'' g u (f x)) (hf : mdifferentiable_within_at I I' f s x)
   (h : s ⊆ f ⁻¹' u) (hxs : unique_mdiff_within_at I s x) :
-  mfderiv_within I I'' (g ∘ f) s x = (mfderiv_within I' I'' g u (f x)).comp (mfderiv_within I I' f s x) :=
+  mfderiv_within I I'' (g ∘ f) s x =
+    (mfderiv_within I' I'' g u (f x)).comp (mfderiv_within I I' f s x) :=
 begin
   apply has_mfderiv_within_at.mfderiv_within _ hxs,
   exact has_mfderiv_within_at.comp x hg.has_mfderiv_within_at hf.has_mfderiv_within_at h
@@ -1136,7 +1147,8 @@ theorem mfderiv_within_eq_fderiv_within :
   mfderiv_within (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') f s x
   = fderiv_within 𝕜 f s x :=
 begin
-  by_cases h : mdifferentiable_within_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') f s x,
+  by_cases h :
+    mdifferentiable_within_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') f s x,
   { simp only [mfderiv_within, h, dif_pos] with mfld_simps },
   { simp only [mfderiv_within, h, dif_neg, not_false_iff],
     rw [mdifferentiable_within_at_iff_differentiable_within_at,
@@ -1287,7 +1299,8 @@ begin
   have z_source : z ∈ e.source, by simp only [hx.1] with mfld_simps,
   have zx : e z = x, by simp only [z, hx.1] with mfld_simps,
   let F := ext_chart_at I z,
-  -- the unique derivative property at `z` is expressed through its preferred chart, that we call `F`.
+  -- the unique derivative property at `z` is expressed through its preferred chart,
+  -- that we call `F`.
   have B : unique_diff_within_at 𝕜
     (F.symm ⁻¹' (s ∩ (e.source ∩ e ⁻¹' ((ext_chart_at I' x).source))) ∩ F.target) (F z),
   { have : unique_mdiff_within_at I s z := hs _ hx.2,
@@ -1321,7 +1334,8 @@ begin
   -- The derivative `G'` is onto, as it is the derivative of a local diffeomorphism, the composition
   -- of the two charts and of `e`.
   have C : dense_range (G' : E → E'),
-  { have : G' = mfderiv I I' ((chart_at H z).symm ≫ₕ e ≫ₕ (chart_at H' x)) ((chart_at H z : M → H) z),
+  { have : G' = mfderiv I I' ((chart_at H z).symm ≫ₕ e ≫ₕ (chart_at H' x))
+      ((chart_at H z : M → H) z),
       by { rw (Diff.mdifferentiable_at Mmem).mfderiv, refl },
     rw this,
     exact (Diff.mfderiv_surjective Mmem).dense_range },
diff --git a/src/geometry/manifold/smooth_manifold_with_corners.lean b/src/geometry/manifold/smooth_manifold_with_corners.lean
index 3ad68f5b481d1..a2d41e8ba2a32 100644
--- a/src/geometry/manifold/smooth_manifold_with_corners.lean
+++ b/src/geometry/manifold/smooth_manifold_with_corners.lean
@@ -167,7 +167,8 @@ instance : has_coe_to_fun (model_with_corners 𝕜 E H) := ⟨_, λ e, e.to_fun
 protected def model_with_corners.symm : local_equiv E H := I.to_local_equiv.symm
 
 /- Register a few lemmas to make sure that `simp` puts expressions in normal form -/
-@[simp, mfld_simps] lemma model_with_corners.to_local_equiv_coe : (I.to_local_equiv : H → E) = I := rfl
+@[simp, mfld_simps] lemma model_with_corners.to_local_equiv_coe : (I.to_local_equiv : H → E) = I :=
+rfl
 
 @[simp, mfld_simps] lemma model_with_corners.mk_coe (e : local_equiv H E) (a b c d) :
   ((model_with_corners.mk e a b c d : model_with_corners 𝕜 E H) : H → E) = (e : H → E) := rfl
diff --git a/src/group_theory/archimedean.lean b/src/group_theory/archimedean.lean
index bb7e00ab2b0e3..047e0e961aaac 100644
--- a/src/group_theory/archimedean.lean
+++ b/src/group_theory/archimedean.lean
@@ -40,7 +40,8 @@ begin
   obtain ⟨⟨a_in, a_pos⟩, a_min⟩ := ha,
   refine le_antisymm _ (H.closure_le.mpr $ by simp [a_in]),
   intros g g_in,
-  obtain ⟨k, nonneg, lt⟩ : ∃ k, 0 ≤ g - k •ℤ a ∧ g - k •ℤ a < a := exists_int_smul_near_of_pos' a_pos g,
+  obtain ⟨k, nonneg, lt⟩ : ∃ k, 0 ≤ g - k •ℤ a ∧ g - k •ℤ a < a :=
+    exists_int_smul_near_of_pos' a_pos g,
   have h_zero : g - k •ℤ a = 0,
   { by_contra h,
     have h : a ≤ g - k •ℤ a,
diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean
index 0b9dc22b4db88..4fc6768478138 100644
--- a/src/group_theory/coset.lean
+++ b/src/group_theory/coset.lean
@@ -256,7 +256,8 @@ calc α ≃ Σ L : quotient s, {x : α // (x : quotient s) = L} :
   equiv.sigma_congr_right (λ L,
     begin
       rw ← eq_class_eq_left_coset,
-      show _root_.subtype (λ x : α, quotient.mk' x = L) ≃ _root_.subtype (λ x : α, quotient.mk' x = quotient.mk' _),
+      show _root_.subtype (λ x : α, quotient.mk' x = L) ≃
+        _root_.subtype (λ x : α, quotient.mk' x = quotient.mk' _),
       simp [-quotient.eq'],
     end)
     ... ≃ Σ L : quotient s, s :
diff --git a/src/topology/algebra/continuous_functions.lean b/src/topology/algebra/continuous_functions.lean
index bd8bbeedfb817..f34ccf6863545 100644
--- a/src/topology/algebra/continuous_functions.lean
+++ b/src/topology/algebra/continuous_functions.lean
@@ -84,8 +84,8 @@ end subtype
 section continuous_map
 
 @[to_additive]
-instance continuous_map_semigroup {α : Type*} {β : Type*} [topological_space α] [topological_space β]
-  [semigroup β] [has_continuous_mul β] : semigroup C(α, β) :=
+instance continuous_map_semigroup {α : Type*} {β : Type*} [topological_space α]
+  [topological_space β] [semigroup β] [has_continuous_mul β] : semigroup C(α, β) :=
 { mul_assoc := λ a b c, by ext; exact mul_assoc _ _ _,
   ..continuous_map.has_mul}
 
@@ -114,8 +114,8 @@ instance continuous_map_group {α : Type*} {β : Type*} [topological_space α] [
   ..continuous_map_monoid }
 
 @[to_additive]
-instance continuous_map_comm_group {α : Type*} {β : Type*} [topological_space α] [topological_space β]
-  [comm_group β] [topological_group β] : comm_group C(α, β) :=
+instance continuous_map_comm_group {α : Type*} {β : Type*} [topological_space α]
+  [topological_space β] [comm_group β] [topological_group β] : comm_group C(α, β) :=
 { ..continuous_map_group,
   ..continuous_map_comm_monoid }
 
@@ -241,8 +241,8 @@ section algebra_structure
 ### Algebra structure
 
 In this section we show that continuous functions valued in a topological algebra `A` over a ring
-`R` inherit the structure of an algebra. Note that the hypothesis that `A` is a topological algebra is
-obtained by requiring that `A` be both a `topological_semimodule` and a `topological_semiring`
+`R` inherit the structure of an algebra. Note that the hypothesis that `A` is a topological algebra
+is obtained by requiring that `A` be both a `topological_semimodule` and a `topological_semiring`
 (by now we require `topological_ring`: see TODO below).-/
 
 section subtype
diff --git a/src/topology/algebra/floor_ring.lean b/src/topology/algebra/floor_ring.lean
index 575ecfa641586..e0c19eb26fe2d 100644
--- a/src/topology/algebra/floor_ring.lean
+++ b/src/topology/algebra/floor_ring.lean
@@ -180,11 +180,12 @@ begin
     { simp only [continuous_within_at, fract_coe, nhds_within_prod_eq,
                   nhds_within_univ, id.def, comp_app, prod.map_mk],
       refine (h _ ⟨true.intro, by exact_mod_cast left_mem_Icc.mpr zero_le_one⟩).tendsto.comp _,
-      rw [nhds_within_prod_eq, nhds_within_univ, nhds_within_Icc_eq_nhds_within_Ici (@zero_lt_one α _ _)],
+      rw [nhds_within_prod_eq, nhds_within_univ,
+        nhds_within_Icc_eq_nhds_within_Ici (@zero_lt_one α _ _)],
       exact tendsto_id.prod_map (tendsto_fract_right _) } },
   { have : t ∈ Ioo (floor t : α) ((floor t : α) + 1),
       from ⟨lt_of_le_of_ne (floor_le t) (ne.symm ht), lt_floor_add_one _⟩,
-    refine (h ((prod.map _ fract) _) ⟨trivial, ⟨fract_nonneg _, (fract_lt_one _).le⟩⟩).tendsto.comp _,
+    apply (h ((prod.map _ fract) _) ⟨trivial, ⟨fract_nonneg _, (fract_lt_one _).le⟩⟩).tendsto.comp,
     simp only [nhds_prod_eq, nhds_within_prod_eq, nhds_within_univ, id.def, prod.map_mk],
     exact continuous_at_id.tendsto.prod_map
             (tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _
diff --git a/src/topology/algebra/group_completion.lean b/src/topology/algebra/group_completion.lean
index 2f85188f42ef0..0beb68d02376e 100644
--- a/src/topology/algebra/group_completion.lean
+++ b/src/topology/algebra/group_completion.lean
@@ -80,23 +80,26 @@ instance is_add_group_hom_coe : is_add_group_hom (coe : α → completion α) :=
 
 variables {β : Type v} [uniform_space β] [add_group β] [uniform_add_group β]
 
-lemma is_add_group_hom_extension  [complete_space β] [separated_space β]
-  {f : α → β} [is_add_group_hom f] (hf : continuous f) : is_add_group_hom (completion.extension f) :=
+lemma is_add_group_hom_extension  [complete_space β] [separated_space β] {f : α → β}
+  [is_add_group_hom f] (hf : continuous f) : is_add_group_hom (completion.extension f) :=
 have hf : uniform_continuous f, from uniform_continuous_of_continuous hf,
 { map_add := assume a b, completion.induction_on₂ a b
   (is_closed_eq
     (continuous_extension.comp continuous_add)
     ((continuous_extension.comp continuous_fst).add (continuous_extension.comp continuous_snd)))
-  (assume a b, by rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, is_add_hom.map_add f]) }
+  (λ a b, by rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf,
+    is_add_hom.map_add f]) }
 
 lemma is_add_group_hom_map
   {f : α → β} [is_add_group_hom f] (hf : continuous f) : is_add_group_hom (completion.map f) :=
 @is_add_group_hom_extension _ _ _ _ _ _ _ _ _ _ _ (is_add_group_hom.comp _ _)
   ((continuous_coe _).comp hf)
 
-instance {α : Type u} [uniform_space α] [add_comm_group α] [uniform_add_group α] : add_comm_group (completion α) :=
+instance {α : Type u} [uniform_space α] [add_comm_group α] [uniform_add_group α] :
+  add_comm_group (completion α) :=
 { add_comm  := assume a b, completion.induction_on₂ a b
-    (is_closed_eq (continuous_map₂ continuous_fst continuous_snd) (continuous_map₂ continuous_snd continuous_fst))
+    (is_closed_eq (continuous_map₂ continuous_fst continuous_snd)
+      (continuous_map₂ continuous_snd continuous_fst))
     (assume x y, by { change ↑x + ↑y = ↑y + ↑x, rw [← coe_add, ← coe_add, add_comm]}),
   .. completion.add_group }
 end uniform_add_group
diff --git a/src/topology/algebra/ordered.lean b/src/topology/algebra/ordered.lean
index f4a75a6b59286..2e3e2b0dadde8 100644
--- a/src/topology/algebra/ordered.lean
+++ b/src/topology/algebra/ordered.lean
@@ -38,8 +38,9 @@ We prove many basic properties of such topologies.
 
 ## Main statements
 
-This file contains the proofs of the following facts. For exact requirements (`order_closed_topology`
-vs `order_topology`, `preorder` vs `partial_order` vs `linear_order` etc) see their statements.
+This file contains the proofs of the following facts. For exact requirements
+(`order_closed_topology` vs `order_topology`, `preorder` vs `partial_order` vs `linear_order` etc)
+see their statements.
 
 ### Open / closed sets
 
@@ -427,11 +428,11 @@ by simpa only [dual_Ioc] using @nhds_within_Ioc_eq_nhds_within_Ioi (order_dual 
   𝓝[Ioo a b] b = 𝓝[Iio b] b :=
 by simpa only [dual_Ioo] using @nhds_within_Ioo_eq_nhds_within_Ioi (order_dual α) _ _ _ _ _ h
 
-@[simp] lemma continuous_within_at_Ico_iff_Iio [topological_space β] {a b : α} {f : α → β} (h : a < b) :
+@[simp] lemma continuous_within_at_Ico_iff_Iio {a b : α} {f : α → γ} (h : a < b) :
   continuous_within_at f (Ico a b) b ↔ continuous_within_at f (Iio b) b :=
 by simp only [continuous_within_at, nhds_within_Ico_eq_nhds_within_Iio h]
 
-@[simp] lemma continuous_within_at_Ioo_iff_Iio [topological_space β] {a b : α} {f : α → β} (h : a < b) :
+@[simp] lemma continuous_within_at_Ioo_iff_Iio {a b : α} {f : α → γ} (h : a < b) :
   continuous_within_at f (Ioo a b) b ↔ continuous_within_at f (Iio b) b :=
 by simp only [continuous_within_at, nhds_within_Ioo_eq_nhds_within_Iio h]
 
@@ -1779,7 +1780,8 @@ begin
     { rw h, exact mem_closure_of_is_glb (is_glb_Ioo hab) hab' },
     by_cases h' : x = b,
     { rw h', refine mem_closure_of_is_lub (is_lub_Ioo hab) hab' },
-    exact subset_closure ⟨lt_of_le_of_ne hx.1 (ne.symm h), by simpa [h'] using lt_or_eq_of_le hx.2⟩ }
+    exact subset_closure ⟨lt_of_le_of_ne hx.1 (ne.symm h),
+      by simpa [h'] using lt_or_eq_of_le hx.2⟩ }
 end
 
 /-- The closure of the interval `(a, b]` is the closed interval `[a, b]`. -/
diff --git a/src/topology/algebra/uniform_group.lean b/src/topology/algebra/uniform_group.lean
index 1219b0c23724a..0630dddd8a5ab 100644
--- a/src/topology/algebra/uniform_group.lean
+++ b/src/topology/algebra/uniform_group.lean
@@ -100,12 +100,14 @@ begin
   rw [nhds_eq_comap_uniformity, filter.comap_comap],
   refine le_antisymm (filter.map_le_iff_le_comap.1 _) _,
   { assume s hs,
-    rcases mem_uniformity_of_uniform_continuous_invariant uniform_continuous_sub hs with ⟨t, ht, hts⟩,
+    rcases mem_uniformity_of_uniform_continuous_invariant uniform_continuous_sub hs
+      with ⟨t, ht, hts⟩,
     refine mem_map.2 (mem_sets_of_superset ht _),
     rintros ⟨a, b⟩,
     simpa [subset_def] using hts a b a },
   { assume s hs,
-    rcases mem_uniformity_of_uniform_continuous_invariant uniform_continuous_add hs with ⟨t, ht, hts⟩,
+    rcases mem_uniformity_of_uniform_continuous_invariant uniform_continuous_add hs
+      with ⟨t, ht, hts⟩,
     refine ⟨_, ht, _⟩,
     rintros ⟨a, b⟩, simpa [subset_def] using hts 0 (b - a) a }
 end
@@ -168,7 +170,8 @@ def topological_add_group.to_uniform_space : uniform_space G :=
       have H : (λp:G×G, p.2 - p.1) ⁻¹' V ∈ comap (λp:G×G, p.2 - p.1) (𝓝 (0 : G)),
         by existsi [V, V_nhds] ; refl,
       existsi H,
-      have comp_rel_sub : comp_rel ((λp:G×G, p.2 - p.1) ⁻¹' V) ((λp:G×G, p.2 - p.1) ⁻¹' V) ⊆ (λp:G×G, p.2 - p.1) ⁻¹' U,
+      have comp_rel_sub :
+        comp_rel ((λp:G×G, p.2 - p.1) ⁻¹' V) ((λp, p.2 - p.1) ⁻¹' V) ⊆ (λp:G×G, p.2 - p.1) ⁻¹' U,
       begin
         intros p p_comp_rel,
         rcases p_comp_rel with ⟨z, ⟨Hz1, Hz2⟩⟩,
@@ -212,12 +215,13 @@ begin
 end
 end
 
-lemma to_uniform_space_eq {α : Type*} [u : uniform_space α] [add_comm_group α] [uniform_add_group α]:
-  topological_add_group.to_uniform_space α = u :=
+lemma to_uniform_space_eq {G : Type*} [u : uniform_space G] [add_comm_group G]
+  [uniform_add_group G] :
+  topological_add_group.to_uniform_space G = u :=
 begin
   ext : 1,
-  show @uniformity α (topological_add_group.to_uniform_space α) = 𝓤 α,
-  rw [uniformity_eq_comap_nhds_zero' α, uniformity_eq_comap_nhds_zero α]
+  show @uniformity G (topological_add_group.to_uniform_space G) = 𝓤 G,
+  rw [uniformity_eq_comap_nhds_zero' G, uniformity_eq_comap_nhds_zero G]
 end
 
 end topological_add_comm_group
@@ -342,7 +346,8 @@ variables [topological_space α] [add_comm_group α] [topological_add_group α]
 variables [topological_space β] [add_comm_group β] [topological_add_group β]
 variables [topological_space γ] [add_comm_group γ] [topological_add_group γ]
 variables [topological_space δ] [add_comm_group δ] [topological_add_group δ]
-variables [uniform_space G] [add_comm_group G] [uniform_add_group G] [separated_space G] [complete_space G]
+variables [uniform_space G] [add_comm_group G] [uniform_add_group G] [separated_space G]
+  [complete_space G]
 variables {e : β → α} [is_add_group_hom e] (de : dense_inducing e)
 variables {f : δ → γ} [is_add_group_hom f] (df : dense_inducing f)
 variables {φ : β × δ → G} (hφ : continuous φ) [bilin : is_Z_bilin φ]
@@ -359,7 +364,8 @@ begin
   let ee := λ u : β × β, (e u.1, e u.2),
 
   have lim1 : tendsto (λ a : β × β, (a.2 - a.1, y₁)) (comap e Nx ×ᶠ comap e Nx) (𝓝 (0, y₁)),
-  { have := tendsto.prod_mk (tendsto_sub_comap_self de x₀) (tendsto_const_nhds : tendsto (λ (p : β × β), y₁) (comap ee $ 𝓝 (x₀, x₀)) (𝓝 y₁)),
+  { have := tendsto.prod_mk (tendsto_sub_comap_self de x₀)
+      (tendsto_const_nhds : tendsto (λ (p : β × β), y₁) (comap ee $ 𝓝 (x₀, x₀)) (𝓝 y₁)),
     rw [nhds_prod_eq, prod_comap_comap_eq, ←nhds_prod_eq],
     exact (this : _) },
 
@@ -418,7 +424,8 @@ begin
             V₁ ∩ V₂, inter_mem_sets V₁_nhd V₂_nhd],
 
   rintros x x' ⟨xU₁, xU₂⟩ ⟨x'U₁, x'U₂⟩ y y' ⟨yV₁, yV₂⟩ ⟨y'V₁, y'V₂⟩,
-  have key_formula : φ(x', y') - φ(x, y) = φ(x' - x, y₁) + φ(x' - x, y' - y₁) + φ(x₁, y' - y) + φ(x - x₁, y' - y),
+  have key_formula : φ(x', y') - φ(x, y) =
+    φ(x' - x, y₁) + φ(x' - x, y' - y₁) + φ(x₁, y' - y) + φ(x - x₁, y' - y),
   { repeat { rw is_Z_bilin.sub_left φ },
     repeat { rw is_Z_bilin.sub_right φ },
     apply eq_of_sub_eq_zero,
diff --git a/src/topology/bounded_continuous_function.lean b/src/topology/bounded_continuous_function.lean
index 56280ec0bd22c..363d177615608 100644
--- a/src/topology/bounded_continuous_function.lean
+++ b/src/topology/bounded_continuous_function.lean
@@ -59,16 +59,17 @@ lemma dist_set_exists : ∃ C, 0 ≤ C ∧ ∀ x : α, dist (f x) (g x) ≤ C :=
 begin
   refine if h : nonempty α then _ else ⟨0, le_refl _, λ x, h.elim ⟨x⟩⟩,
   cases h with x,
-  rcases f.2 with ⟨_, Cf, hCf⟩, /- hCf : ∀ (x y : α), dist (f.val x) (f.val y) ≤ Cf -/
-  rcases g.2 with ⟨_, Cg, hCg⟩, /- hCg : ∀ (x y : α), dist (g.val x) (g.val y) ≤ Cg -/
+  rcases f.2.2 with ⟨Cf, hCf : ∀ x y, dist (f x) (f y) ≤ Cf⟩,
+  rcases g.2.2 with ⟨Cg, hCg : ∀ x y, dist (g x) (g y) ≤ Cg⟩,
   let C := max 0 (dist (f x) (g x) + (Cf + Cg)),
-  exact ⟨C, le_max_left _ _, λ y, calc
-    dist (f y) (g y) ≤ dist (f x) (g x) + (dist (f x) (f y) + dist (g x) (g y)) : dist_triangle4_left _ _ _ _
-                ... ≤ dist (f x) (g x) + (Cf + Cg) : add_le_add_left (add_le_add (hCf _ _) (hCg _ _)) _
-                ... ≤ C : le_max_right _ _⟩
+  refine ⟨C, le_max_left _ _, λ y, _⟩,
+  calc dist (f y) (g y) ≤ dist (f x) (g x) + (dist (f x) (f y) + dist (g x) (g y)) :
+    dist_triangle4_left _ _ _ _
+                    ... ≤ dist (f x) (g x) + (Cf + Cg) : by mono*
+                    ... ≤ C : le_max_right _ _
 end
 
-/-- The pointwise distance is controlled by the distance between functions, by definition -/
+/-- The pointwise distance is controlled by the distance between functions, by definition. -/
 lemma dist_coe_le_dist (x : α) : dist (f x) (g x) ≤ dist f g :=
 le_cInf dist_set_exists $ λb hb, hb.2 x
 
@@ -160,9 +161,10 @@ begin
     exact this.continuous (λN, (f N).2.1) },
   { /- Check that `F` is bounded -/
     rcases (f 0).2.2 with ⟨C, hC⟩,
-    exact ⟨C + (b 0 + b 0), λ x y, calc
-      dist (F x) (F y) ≤ dist (f 0 x) (f 0 y) + (dist (f 0 x) (F x) + dist (f 0 y) (F y)) : dist_triangle4_left _ _ _ _
-         ... ≤ C + (b 0 + b 0) : add_le_add (hC x y) (add_le_add (fF_bdd x 0) (fF_bdd y 0))⟩ },
+    refine ⟨C + (b 0 + b 0), λ x y, _⟩,
+    calc dist (F x) (F y) ≤ dist (f 0 x) (f 0 y) + (dist (f 0 x) (F x) + dist (f 0 y) (F y)) :
+      dist_triangle4_left _ _ _ _
+                      ... ≤ C + (b 0 + b 0) : by mono* },
   { /- Check that `F` is close to `f N` in distance terms -/
     refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero (λ _, dist_nonneg) _ b_lim),
     exact λ N, (dist_le (b0 _)).2 (λx, fF_bdd x N) }
@@ -321,7 +323,8 @@ arzela_ascoli₂ s hs (closure A) is_closed_closure
       refine bex.imp_right (λ U U_set hU y z hy hz f hf, _) (H x (ε/2) (half_pos ε0)),
       rcases metric.mem_closure_iff.1 hf (ε/2/2) (half_pos (half_pos ε0)) with ⟨g, gA, dist_fg⟩,
       replace dist_fg := λ x, lt_of_le_of_lt (dist_coe_le_dist x) dist_fg,
-      calc dist (f y) (f z) ≤ dist (f y) (g y) + dist (f z) (g z) + dist (g y) (g z) : dist_triangle4_right _ _ _ _
+      calc dist (f y) (f z) ≤ dist (f y) (g y) + dist (f z) (g z) + dist (g y) (g z) :
+        dist_triangle4_right _ _ _ _
           ... < ε/2/2 + ε/2/2 + ε/2 :
             add_lt_add (add_lt_add (dist_fg y) (dist_fg z)) (hU y z hy hz g gA)
           ... = ε : by rw [add_halves, add_halves]
diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
index f28a49dd791e1..fb74a51e79daa 100644
--- a/src/topology/constructions.lean
+++ b/src/topology/constructions.lean
@@ -212,7 +212,7 @@ have hf : continuous_at f (x, y).fst, from hf,
 have hg : continuous_at g (x, y).snd, from hg,
 hf.prod_map hg
 
-lemma prod_generate_from_generate_from_eq {α : Type*} {β : Type*} {s : set (set α)} {t : set (set β)}
+lemma prod_generate_from_generate_from_eq {α β : Type*} {s : set (set α)} {t : set (set β)}
   (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
   @prod.topological_space α β (generate_from s) (generate_from t) =
   generate_from {g | ∃u∈s, ∃v∈t, g = set.prod u v} :=
diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean
index 2d9ae3c2a3970..3aa825fdde92c 100644
--- a/src/topology/continuous_on.lean
+++ b/src/topology/continuous_on.lean
@@ -313,7 +313,8 @@ tendsto f (𝓝[s] x) (𝓝 (f x))
 /-- If a function is continuous within `s` at `x`, then it tends to `f x` within `s` by definition.
 We register this fact for use with the dot notation, especially to use `tendsto.comp` as
 `continuous_within_at.comp` will have a different meaning. -/
-lemma continuous_within_at.tendsto {f : α → β} {s : set α} {x : α} (h : continuous_within_at f s x) :
+lemma continuous_within_at.tendsto {f : α → β} {s : set α} {x : α}
+  (h : continuous_within_at f s x) :
   tendsto f (𝓝[s] x) (𝓝 (f x)) := h
 
 /-- A function between topological spaces is continuous on a subset `s`
@@ -328,7 +329,8 @@ theorem continuous_within_at_univ (f : α → β) (x : α) :
   continuous_within_at f set.univ x ↔ continuous_at f x :=
 by rw [continuous_at, continuous_within_at, nhds_within_univ]
 
-theorem continuous_within_at_iff_continuous_at_restrict (f : α → β) {x : α} {s : set α} (h : x ∈ s) :
+theorem continuous_within_at_iff_continuous_at_restrict (f : α → β) {x : α} {s : set α}
+  (h : x ∈ s) :
   continuous_within_at f s x ↔ continuous_at (s.restrict f) ⟨x, h⟩ :=
 tendsto_nhds_within_iff_subtype h f _
 
diff --git a/src/topology/dense_embedding.lean b/src/topology/dense_embedding.lean
index 062831193ad40..aa079d29f3b99 100644
--- a/src/topology/dense_embedding.lean
+++ b/src/topology/dense_embedding.lean
@@ -94,8 +94,8 @@ variables [topological_space δ] {f : γ → α} {g : γ → δ} {h : δ → β}
 g↓     ↓e
  δ -h→ β
 -/
-lemma tendsto_comap_nhds_nhds  {d : δ} {a : α} (di : dense_inducing i) (H : tendsto h (𝓝 d) (𝓝 (i a)))
-  (comm : h ∘ g = i ∘ f) : tendsto f (comap g (𝓝 d)) (𝓝 a) :=
+lemma tendsto_comap_nhds_nhds  {d : δ} {a : α} (di : dense_inducing i)
+  (H : tendsto h (𝓝 d) (𝓝 (i a))) (comm : h ∘ g = i ∘ f) : tendsto f (comap g (𝓝 d)) (𝓝 a) :=
 begin
   have lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d := map_comap_le,
   replace lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d) := map_mono lim1,
@@ -227,8 +227,9 @@ lemma to_embedding : embedding e :=
 protected lemma separable_space [separable_space α] : separable_space β :=
 de.to_dense_inducing.separable_space
 
-/-- The product of two dense embeddings is a dense embedding -/
-protected lemma prod {e₁ : α → β} {e₂ : γ → δ} (de₁ : dense_embedding e₁) (de₂ : dense_embedding e₂) :
+/-- The product of two dense embeddings is a dense embedding. -/
+protected lemma prod {e₁ : α → β} {e₂ : γ → δ} (de₁ : dense_embedding e₁)
+  (de₂ : dense_embedding e₂) :
   dense_embedding (λ(p : α × γ), (e₁ p.1, e₂ p.2)) :=
 { inj := assume ⟨x₁, x₂⟩ ⟨y₁, y₂⟩,
     by simp; exact assume h₁ h₂, ⟨de₁.inj h₁, de₂.inj h₂⟩,
@@ -273,7 +274,8 @@ have ∀q:β×β, p q.1 q.2,
 assume b₁ b₂, this ⟨b₁, b₂⟩
 
 lemma is_closed_property3 [topological_space β] {e : α → β} {p : β → β → β → Prop}
-  (he : dense_range e) (hp : is_closed {q:β×β×β | p q.1 q.2.1 q.2.2}) (h : ∀a₁ a₂ a₃, p (e a₁) (e a₂) (e a₃)) :
+  (he : dense_range e) (hp : is_closed {q:β×β×β | p q.1 q.2.1 q.2.2})
+  (h : ∀a₁ a₂ a₃, p (e a₁) (e a₂) (e a₃)) :
   ∀b₁ b₂ b₃, p b₁ b₂ b₃ :=
 have ∀q:β×β×β, p q.1 q.2.1 q.2.2,
   from is_closed_property (he.prod_map $ he.prod_map he) hp $ λ _, h _ _ _,
@@ -291,7 +293,8 @@ lemma dense_range.induction_on₂ [topological_space β] {e : α → β} {p : β
 
 @[elab_as_eliminator]
 lemma dense_range.induction_on₃ [topological_space β] {e : α → β} {p : β → β → β → Prop}
-  (he : dense_range e) (hp : is_closed {q:β×β×β | p q.1 q.2.1 q.2.2}) (h : ∀a₁ a₂ a₃, p (e a₁) (e a₂) (e a₃))
+  (he : dense_range e) (hp : is_closed {q:β×β×β | p q.1 q.2.1 q.2.2})
+  (h : ∀a₁ a₂ a₃, p (e a₁) (e a₂) (e a₃))
   (b₁ b₂ b₃ : β) : p b₁ b₂ b₃ := is_closed_property3 he hp h _ _ _
 
 section
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
index fce1f4256d3b9..1147a164db10a 100644
--- a/src/topology/metric_space/basic.lean
+++ b/src/topology/metric_space/basic.lean
@@ -104,17 +104,16 @@ by rw dist_comm y; apply dist_triangle
 
 lemma dist_triangle4 (x y z w : α) :
   dist x w ≤ dist x y + dist y z + dist z w :=
-calc
-  dist x w ≤ dist x z + dist z w : dist_triangle x z w
-       ... ≤ (dist x y + dist y z) + dist z w : add_le_add_right (metric_space.dist_triangle x y z) _
+calc dist x w ≤ dist x z + dist z w : dist_triangle x z w
+          ... ≤ (dist x y + dist y z) + dist z w : add_le_add_right (dist_triangle x y z) _
 
 lemma dist_triangle4_left (x₁ y₁ x₂ y₂ : α) :
   dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂) :=
-by rw [add_left_comm, dist_comm x₁, ← add_assoc]; apply dist_triangle4
+by { rw [add_left_comm, dist_comm x₁, ← add_assoc], apply dist_triangle4 }
 
 lemma dist_triangle4_right (x₁ y₁ x₂ y₂ : α) :
   dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂ :=
-by rw [add_right_comm, dist_comm y₁]; apply dist_triangle4
+by { rw [add_right_comm, dist_comm y₁], apply dist_triangle4 }
 
 /-- The triangle (polygon) inequality for sequences of points; `finset.Ico` version. -/
 lemma dist_le_Ico_sum_dist (f : ℕ → α) {m n} (h : m ≤ n) :
@@ -329,7 +328,7 @@ by simp [dist_comm]
 theorem ball_subset_ball (h : ε₁ ≤ ε₂) : ball x ε₁ ⊆ ball x ε₂ :=
 λ y (yx : _ < ε₁), lt_of_lt_of_le yx h
 
-theorem closed_ball_subset_closed_ball {α : Type u} [metric_space α] {ε₁ ε₂ : ℝ} {x : α} (h : ε₁ ≤ ε₂) :
+theorem closed_ball_subset_closed_ball (h : ε₁ ≤ ε₂) :
   closed_ball x ε₁ ⊆ closed_ball x ε₂ :=
 λ y (yx : _ ≤ ε₁), le_trans yx h
 
@@ -447,7 +446,8 @@ lemma uniform_continuous_on_iff [metric_space β] {f : α → β} {s : set α} :
   uniform_continuous_on f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x y ∈ s, dist x y < δ → dist (f x) (f y) < ε :=
 begin
   dsimp [uniform_continuous_on],
-  rw (metric.uniformity_basis_dist.inf_principal (s.prod s)).tendsto_iff metric.uniformity_basis_dist,
+  rw (metric.uniformity_basis_dist.inf_principal (s.prod s)).tendsto_iff
+    metric.uniformity_basis_dist,
   simp only [and_imp, exists_prop, prod.forall, mem_inter_eq, gt_iff_lt, mem_set_of_eq, mem_prod],
   finish,
 end
@@ -785,7 +785,8 @@ def emetric_space.to_metric_space_of_dist {α : Type u} [e : emetric_space α]
   metric_space α :=
 let m : metric_space α :=
 { dist := dist,
-  eq_of_dist_eq_zero := λx y hxy, by simpa [h, ennreal.to_real_eq_zero_iff, edist_ne_top x y] using hxy,
+  eq_of_dist_eq_zero := λx y hxy,
+    by simpa [h, ennreal.to_real_eq_zero_iff, edist_ne_top x y] using hxy,
   dist_self          := λx, by simp [h],
   dist_comm          := λx y, by simp [h, emetric_space.edist_comm],
   dist_triangle      := λx y z, begin
@@ -812,7 +813,8 @@ converging. This is often applied for `B N = 2^{-N}`, i.e., with a very fast con
 `0`, which makes it possible to use arguments of converging series, while this is impossible
 to do in general for arbitrary Cauchy sequences. -/
 theorem metric.complete_of_convergent_controlled_sequences (B : ℕ → real) (hB : ∀n, 0 < B n)
-  (H : ∀u : ℕ → α, (∀N n m : ℕ, N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃x, tendsto u at_top (𝓝 x)) :
+  (H : ∀u : ℕ → α, (∀N n m : ℕ, N ≤ n → N ≤ m → dist (u n) (u m) < B N) →
+    ∃x, tendsto u at_top (𝓝 x)) :
   complete_space α :=
 begin
   -- this follows from the same criterion in emetric spaces. We just need to translate
@@ -1332,8 +1334,8 @@ instance complete_of_proper [proper_space α] : complete_space α :=
   rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩,
   have : t ⊆ closed_ball x 1 := by intros y yt; simp [dist_comm]; apply le_of_lt (ht x y xt yt),
   have : closed_ball x 1 ∈ f := f.sets_of_superset t_fset this,
-  rcases (compact_iff_totally_bounded_complete.1 (proper_space.compact_ball x 1)).2 f hf (le_principal_iff.2 this)
-    with ⟨y, _, hy⟩,
+  rcases (compact_iff_totally_bounded_complete.1 (proper_space.compact_ball x 1)).2 f hf
+    (le_principal_iff.2 this) with ⟨y, _, hy⟩,
   exact ⟨y, hy⟩
 end⟩
 
@@ -1695,7 +1697,8 @@ end
 /-- The diameter of a union is controlled by the sum of the diameters, and the distance between
 any two points in each of the sets. This lemma is true without any side condition, since it is
 obviously true if `s ∪ t` is unbounded. -/
-lemma diam_union {t : set α} (xs : x ∈ s) (yt : y ∈ t) : diam (s ∪ t) ≤ diam s + dist x y + diam t :=
+lemma diam_union {t : set α} (xs : x ∈ s) (yt : y ∈ t) :
+  diam (s ∪ t) ≤ diam s + dist x y + diam t :=
 begin
   classical, by_cases H : bounded (s ∪ t),
   { have hs : bounded s, from H.subset (subset_union_left _ _),
diff --git a/src/topology/opens.lean b/src/topology/opens.lean
index 88a06d91ff88d..3ddcbb93f1cf5 100644
--- a/src/topology/opens.lean
+++ b/src/topology/opens.lean
@@ -146,7 +146,8 @@ lemma is_basis_iff_nbhd {B : set (opens α)} :
 begin
   split; intro h,
   { rintros ⟨sU, hU⟩ x hx,
-    rcases (mem_nhds_of_is_topological_basis h).mp (mem_nhds_sets hU hx) with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩,
+    rcases (mem_nhds_of_is_topological_basis h).mp (mem_nhds_sets hU hx)
+      with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩,
     refine ⟨V, H₁, _⟩,
     cases V, dsimp at H₂, subst H₂, exact hsV },
   { refine is_topological_basis_of_open_of_nhds _ _,
diff --git a/src/topology/order.lean b/src/topology/order.lean
index f372b42cb1f2f..6e5cb01877c3b 100644
--- a/src/topology/order.lean
+++ b/src/topology/order.lean
@@ -93,7 +93,8 @@ protected def mk_of_nhds (n : α → filter α) : topological_space α :=
 { is_open        := λs, ∀a∈s, s ∈ n a,
   is_open_univ   := assume x h, univ_mem_sets,
   is_open_inter  := assume s t hs ht x ⟨hxs, hxt⟩, inter_mem_sets (hs x hxs) (ht x hxt),
-  is_open_sUnion := assume s hs a ⟨x, hx, hxa⟩, mem_sets_of_superset (hs x hx _ hxa) (set.subset_sUnion_of_mem hx) }
+  is_open_sUnion := assume s hs a ⟨x, hx, hxa⟩,
+    mem_sets_of_superset (hs x hx _ hxa) (set.subset_sUnion_of_mem hx) }
 
 lemma nhds_mk_of_nhds (n : α → filter α) (a : α)
   (h₀ : pure ≤ n) (h₁ : ∀{a s}, s ∈ n a → ∃ t ∈ n a, t ⊆ s ∧ ∀a' ∈ t, s ∈ n a') :
@@ -293,7 +294,8 @@ lemma continuous.coinduced_le (h : @continuous α β t t' f) :
   t.coinduced f ≤ t' :=
 λ s hs, (continuous_def.1 h s hs : _)
 
-lemma coinduced_le_iff_le_induced {f : α → β} {tα : topological_space α} {tβ : topological_space β} :
+lemma coinduced_le_iff_le_induced {f : α → β} {tα : topological_space α}
+  {tβ : topological_space β} :
   tα.coinduced f ≤ tβ ↔ tα ≤ tβ.induced f :=
 iff.intro
   (assume h s ⟨t, ht, hst⟩, hst ▸ h _ ht)
@@ -406,7 +408,8 @@ protected def topological_space.nhds_adjoint (a : α) (f : filter α) : topologi
 { is_open        := λs, a ∈ s → s ∈ f,
   is_open_univ   := assume s, univ_mem_sets,
   is_open_inter  := assume s t hs ht ⟨has, hat⟩, inter_mem_sets (hs has) (ht hat),
-  is_open_sUnion := assume k hk ⟨u, hu, hau⟩, mem_sets_of_superset (hk u hu hau) (subset_sUnion_of_mem hu) }
+  is_open_sUnion := assume k hk ⟨u, hu, hau⟩, mem_sets_of_superset (hk u hu hau)
+    (subset_sUnion_of_mem hu) }
 
 lemma gc_nhds (a : α) :
   galois_connection  (topological_space.nhds_adjoint a) (λt, @nhds α t a) :=
diff --git a/src/topology/path_connected.lean b/src/topology/path_connected.lean
index 3c84c30f44946..080b0418a3763 100644
--- a/src/topology/path_connected.lean
+++ b/src/topology/path_connected.lean
@@ -425,12 +425,12 @@ begin
   linarith
 end
 
-@[simp] lemma truncate_zero_zero {X : Type*} [topological_space X] {a b : X}
-  (γ : path a b) : γ.truncate 0 0 = (path.refl a).cast (by rw [min_self, γ.extend_zero]) γ.extend_zero :=
+@[simp] lemma truncate_zero_zero {X : Type*} [topological_space X] {a b : X} (γ : path a b) :
+  γ.truncate 0 0 = (path.refl a).cast (by rw [min_self, γ.extend_zero]) γ.extend_zero :=
 by convert γ.truncate_self 0; exact γ.extend_zero.symm
 
-@[simp] lemma truncate_one_one {X : Type*} [topological_space X] {a b : X}
-  (γ : path a b) : γ.truncate 1 1 = (path.refl b).cast (by rw [min_self, γ.extend_one]) γ.extend_one :=
+@[simp] lemma truncate_one_one {X : Type*} [topological_space X] {a b : X} (γ : path a b) :
+  γ.truncate 1 1 = (path.refl b).cast (by rw [min_self, γ.extend_one]) γ.extend_one :=
 by convert γ.truncate_self 1; exact γ.extend_one.symm
 
 @[simp] lemma truncate_zero_one {X : Type*} [topological_space X] {a b : X}
@@ -580,7 +580,8 @@ begin
 end
 
 lemma path_component_subset_component (x : X) : path_component x ⊆ connected_component x :=
-λ y h, subset_connected_component (is_connected_range h.some_path.continuous).2 ⟨0, by simp⟩ ⟨1, by simp⟩
+λ y h, subset_connected_component (is_connected_range h.some_path.continuous).2
+  ⟨0, by simp⟩ ⟨1, by simp⟩
 
 /-- The path component of `x` in `F` is the set of points that can be joined to `x` in `F`. -/
 def path_component_in (x : X) (F : set X) := {y | joined_in F x y}
@@ -588,7 +589,8 @@ def path_component_in (x : X) (F : set X) := {y | joined_in F x y}
 @[simp] lemma path_component_in_univ (x : X) : path_component_in x univ = path_component x :=
 by simp [path_component_in, path_component, joined_in, joined, exists_true_iff_nonempty]
 
-lemma joined.mem_path_component (hyz : joined y z) (hxy : y ∈ path_component x) : z ∈ path_component x :=
+lemma joined.mem_path_component (hyz : joined y z) (hxy : y ∈ path_component x) :
+  z ∈ path_component x :=
 hxy.trans hyz
 
 /-! ### Path connected sets -/
@@ -652,7 +654,8 @@ end
 
 lemma is_path_connected.exists_path_through_family
   {X : Type*} [topological_space X] {n : ℕ} {s : set X} (h : is_path_connected s)
-  (p : fin (n+1) → X) (hp : ∀ i, p i ∈ s) : ∃ γ : path (p 0) (p n), (range γ ⊆ s) ∧ (∀ i, p i ∈ range γ) :=
+  (p : fin (n+1) → X) (hp : ∀ i, p i ∈ s) :
+  ∃ γ : path (p 0) (p n), (range γ ⊆ s) ∧ (∀ i, p i ∈ range γ) :=
 begin
   let p' : ℕ → X := λ k, if h : k < n+1 then p ⟨k, h⟩ else p ⟨0, n.zero_lt_succ⟩,
   obtain ⟨γ, hγ⟩ : ∃ (γ : path (p' 0) (p' n)), (∀ i ≤ n, p' i ∈ range γ) ∧ range γ ⊆ s,