chore(*): split long lines (#5908)

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',

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),

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

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,29 +146,34 @@ 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))
   (option.some ((list.map output_alphabet.inv_fun) (eb.encode (f a))))
   (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) :=

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

src/data/list/basic.lean

@@ -1688,15 +1688,17 @@ 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'],
     rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n), from _, drop],
     { 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
 

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

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

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

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']

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₀)

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,