chore(.): adapt to change by_cases t with h to by_cases h : t 746134d11ceec378a53ffd3b7ab8626fb291f3bd

Author: johoelzl

analysis/ennreal.lean

@@ -174,24 +174,24 @@ protected lemma mul_assoc : ∀a b c:ennreal, a * b * c = a * (b * c) :=
 begin
   rw [forall_ennreal], constructor,
   { intros ra ha,
-    by_cases ra = 0 with ha', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+    by_cases ha' : ra = 0, simp [*, ennreal.mul_zero, ennreal.zero_mul],
     rw [forall_ennreal], constructor,
     { intros rb hrb,
-      by_cases rb = 0 with hb', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+      by_cases hb' : rb = 0, simp [*, ennreal.mul_zero, ennreal.zero_mul],
       rw [forall_ennreal], constructor,
       { intros rc hrc, simp [*, zero_le_mul, mul_assoc] },
       simp [*, zero_le_mul, mul_eq_zero_iff_eq_zero_or_eq_zero] },
     rw [forall_ennreal], constructor,
       { intros rc hrc,
-        by_cases rc = 0 with hc', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+        by_cases hc' : rc = 0, simp [*, ennreal.mul_zero, ennreal.zero_mul],
         simp [*, zero_le_mul] },
     simp [*] },
   rw [forall_ennreal], constructor,
   { intros rb hrb,
-    by_cases rb = 0 with hb', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+    by_cases hb' : rb = 0, simp [*, ennreal.mul_zero, ennreal.zero_mul],
     rw [forall_ennreal], constructor,
     { intros rc hrc,
-      by_cases rc = 0 with hb';
+      by_cases hb' : rc = 0;
         simp [*, zero_le_mul, ennreal.mul_zero, mul_eq_zero_iff_eq_zero_or_eq_zero] },
     simp [*, zero_le_mul, mul_eq_zero_iff_eq_zero_or_eq_zero] },
   intro c, by_cases c = 0; simp *
@@ -201,24 +201,24 @@ protected lemma left_distrib : ∀a b c:ennreal, a * (b + c) = a * b + a * c :=
 begin
   rw [forall_ennreal], constructor,
   { intros ra ha,
-    by_cases ra = 0 with ha', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+    by_cases ha' : ra = 0, simp [*, ennreal.mul_zero, ennreal.zero_mul],
     rw [forall_ennreal], constructor,
     { intros rb hrb,
-      by_cases rb = 0 with hb', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+      by_cases hb' : rb = 0, simp [*, ennreal.mul_zero, ennreal.zero_mul],
       rw [forall_ennreal], constructor,
       { intros rc hrc, simp [*, zero_le_mul, add_nonneg, left_distrib] },
       simp [*, zero_le_mul, mul_eq_zero_iff_eq_zero_or_eq_zero] },
     rw [forall_ennreal], constructor,
       { intros rc hrc,
-        by_cases rc = 0 with hc', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+        by_cases hv' : rc = 0, simp [*, ennreal.mul_zero, ennreal.zero_mul],
         simp [*, zero_le_mul] },
     simp [*] },
   rw [forall_ennreal], constructor,
   { intros rb hrb,
-    by_cases rb = 0 with hb', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+    by_cases hb' : rb = 0, simp [*, ennreal.mul_zero, ennreal.zero_mul],
     rw [forall_ennreal], constructor,
     { intros rc hrc,
-      by_cases rc = 0 with hb';
+      by_cases hb' : rc = 0;
         simp [*, zero_le_mul, ennreal.mul_zero, mul_eq_zero_iff_eq_zero_or_eq_zero, add_nonneg,
           add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg] },
     simp [*, zero_le_mul, mul_eq_zero_iff_eq_zero_or_eq_zero] },
@@ -318,8 +318,8 @@ end
 
 lemma of_real_lt_of_real_iff_cases : of_real r < of_real p ↔ 0 < p ∧ r < p :=
 begin
-  by_cases 0 ≤ p with hp,
-  { by_cases 0 ≤ r with hr,
+  by_cases hp : 0 ≤ p,
+  { by_cases hr : 0 ≤ r,
     { simp [*, iff_def] {contextual := tt},
       show r < p → 0 < p, from lt_of_le_of_lt hr },
     { have h : r ≤ 0, from le_of_lt (lt_of_not_ge hr),

analysis/measure_theory/measurable_space.lean

@@ -52,7 +52,7 @@ begin
   rw [this],
   apply is_measurable_Union_nat _,
   intro i,
-  by_cases f i ∈ s with h'; simp [h', h, is_measurable_empty]
+  by_cases h' : f i ∈ s; simp [h', h, is_measurable_empty]
 end
 
 lemma is_measurable_bUnion {f : β → set α} {s : set β} (hs : countable s)

data/array/lemmas.lean

@@ -79,7 +79,7 @@ list.ext_le (by simp) $ λ j h₁ h₂, begin
   have h₃ : j < n, {simpa using h₁},
   rw [to_list_nth_le _ _ h₃],
   refine let ⟨_, e⟩ := list.nth_eq_some.1 _ in e.symm,
-  by_cases i.1 = j with ij,
+  by_cases ij : i.1 = j,
   { subst j, rw [show fin.mk i.val h₃ = i, from fin.eq_of_veq rfl,
       array.read_write, list.nth_update_nth_of_lt],
     simp [h₃] },
@@ -158,7 +158,7 @@ theorem read_foreach_aux (f : fin n → α → α) (ai : array n α) :
 | 0     hi a ⟨j, hj⟩ ji := absurd ji (nat.not_lt_zero _)
 | (i+1) hi a ⟨j, hj⟩ ji := begin
   dsimp [d_array.iterate_aux], dsimp at ji,
-  by_cases (⟨i, hi⟩ : fin _) = ⟨j, hj⟩ with e,
+  by_cases e : (⟨i, hi⟩ : fin _) = ⟨j, hj⟩,
   { rw [e], simp, refl },
   { rw [read_write_of_ne _ _ e, read_foreach_aux _ _ _ ⟨j, hj⟩],
     exact (lt_or_eq_of_le (nat.le_of_lt_succ ji)).resolve_right

data/equiv.lean

@@ -455,14 +455,14 @@ protected noncomputable def image {α β} (f : α → β) (s : set α) (H : inje
  λ ⟨x, h⟩, subtype.eq (H (classical.some_spec (mem_image_of_mem f h)).2),
  λ ⟨y, h⟩, subtype.eq (classical.some_spec h).2⟩
 
-@[simp] theorem image_apply {α β} (f : α → β) (s : set α) (H : injective f) (a h) : 
+@[simp] theorem image_apply {α β} (f : α → β) (s : set α) (H : injective f) (a h) :
   set.image f s H ⟨a, h⟩ = ⟨f a, mem_image_of_mem _ h⟩ := rfl
 
 protected noncomputable def range {α β} (f : α → β) (H : injective f) :
   α ≃ range f :=
 (set.univ _).symm.trans $ (set.image f univ H).trans (equiv.cast $ by rw range_eq_image)
 
-@[simp] theorem range_apply {α β} (f : α → β) (H : injective f) (a) : 
+@[simp] theorem range_apply {α β} (f : α → β) (H : injective f) (a) :
   set.range f H a = ⟨f a, set.mem_range⟩ :=
 by dunfold equiv.set.range equiv.set.univ;
    simp [set_coe_cast, range_eq_image]
@@ -490,25 +490,25 @@ by by_cases r = a; simp [swap_core, *]
 
 theorem swap_core_swap_core (r a b : α) : swap_core a b (swap_core a b r) = r :=
 begin
-  by_cases r = b with hb,
-  { by_cases r = a with ha,
+  by_cases hb : r = b,
+  { by_cases ha : r = a,
     { simp [hb.symm, ha.symm, swap_core_self] },
     { have : b ≠ a, by rwa [hb] at ha,
       simp [swap_core, *] } },
-  { by_cases r = a with ha,
+  { by_cases ha : r = a,
     { have : b ≠ a, begin rw [ha] at hb, exact ne.symm hb end,
       simp [swap_core, *] },
     simp [swap_core, *] }
 end
 
 theorem swap_core_comm (r a b : α) : swap_core a b r = swap_core b a r :=
 begin
-  by_cases r = b with hb,
-  { by_cases r = a with ha,
+  by_cases hb : r = b,
+  { by_cases ha : r = a,
     { simp [hb.symm, ha.symm, swap_core_self] },
     { have : b ≠ a, by rwa [hb] at ha,
       simp [swap_core, *] } },
-  { by_cases r = a with ha,
+  { by_cases ha : r = a,
     { have : a ≠ b, by rwa [ha] at hb,
       simp [swap_core, *] },
     simp [swap_core, *] }

data/finset.lean

@@ -302,7 +302,7 @@ by rw [inter_comm, insert_inter_of_mem h, inter_comm]
 
 @[simp] theorem insert_inter_of_not_mem {s₁ s₂ : finset α} {a : α} (h : a ∉ s₂) :
   insert a s₁ ∩ s₂ = s₁ ∩ s₂ :=
-ext.2 $ assume a', by by_cases a' = a with h'; simp [mem_inter, mem_insert, h, h', and_comm]
+ext.2 $ assume a', by by_cases h' : a' = a; simp [mem_inter, mem_insert, h, h', and_comm]
 
 @[simp] theorem inter_insert_of_not_mem {s₁ s₂ : finset α} {a : α} (h : a ∉ s₁) :
   s₁ ∩ insert a s₂ = s₁ ∩ s₂ :=

data/finsupp.lean

@@ -70,7 +70,7 @@ by simp [finset.ext]
 
 def single (a : α) (b : β) : α →₀ β :=
 ⟨λa', if a = a' then b else 0,
-  finite_subset (@finite_singleton α a) $ assume a', by by_cases a = a' with h; simp [h]⟩
+  finite_subset (@finite_singleton α a) $ assume a', by by_cases h : a = a'; simp [h]⟩
 
 lemma single_apply {a a' : α} {b : β} :
   (single a b : α →₀ β) a' = (if a = a' then b else 0) :=
@@ -87,7 +87,7 @@ by simp [single_apply, h]
 @[simp] lemma single_zero {a : α} : (single a 0 : α →₀ β) = 0 :=
 ext $ assume a',
 begin
-  by_cases a = a' with h,
+  by_cases h : a = a',
   { rw [h, single_eq_same, zero_apply] },
   { rw [single_eq_of_ne h, zero_apply] }
 end
@@ -180,7 +180,7 @@ by simp [finsupp.prod]
 lemma prod_single_index [add_comm_monoid β] [comm_monoid γ] {a : α} {b : β}
   {h : α → β → γ} (h_zero : h a 0 = 1) : (single a b).prod h = h a b :=
 begin
-  by_cases b = 0 with h,
+  by_cases h : b = 0,
   { simp [h, prod_zero_index, h_zero] },
   { simp [finsupp.prod, support_single_ne_zero h] }
 end
@@ -200,7 +200,7 @@ support_zip_with
   single a (b₁ + b₂) = single a b₁ + single a b₂ :=
 ext $ assume a',
 begin
-  by_cases a = a' with h,
+  by_cases h : a = a',
   { rw [h, add_apply, single_eq_same, single_eq_same, single_eq_same] },
   { rw [add_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, zero_add] }
 end
@@ -278,7 +278,7 @@ have ∀a:α, f.sum (λa' b, ite (a' = a) b 0) =
     ({a} : finset α).sum (λa', ite (a' = a) (f a') 0),
 begin
   intro a,
-  by_cases a ∈ f.support with h,
+  by_cases h : a ∈ f.support,
   { have : {a} ⊆ f.support,
       { simp [finset.subset_iff, *] at * },
     refine (finset.sum_subset this _).symm,

data/hash_map.lean

@@ -203,7 +203,7 @@ theorem valid.replace_aux (a : α) (b : β a) : Π (l : list (Σ a, β a)), a 
   ∃ (u w : list Σ a, β a) b', l = u ++ [⟨a, b'⟩] ++ w ∧ replace_aux a b l = u ++ [⟨a, b⟩] ++ w
 | []            := false.elim
 | (⟨a', b'⟩::t) := begin
-  by_cases a' = a with e,
+  by_cases e : a' = a,
   { subst a',
     suffices : ∃ u w (b'' : β a),
       sigma.mk a b' :: t = u ++ ⟨a, b''⟩ :: w ∧
@@ -257,7 +257,7 @@ theorem valid.erase_aux (a : α) : Π (l : list (Σ a, β a)), a ∈ l.map sigma
   ∃ (u w : list Σ a, β a) b, l = u ++ [⟨a, b⟩] ++ w ∧ erase_aux a l = u ++ [] ++ w
 | []            := false.elim
 | (⟨a', b'⟩::t) := begin
-  by_cases a' = a with e,
+  by_cases e : a' = a,
   { subst a',
     simpa [erase_aux, and_comm] using show ∃ u w (x : β a),
       t = u ++ w ∧ sigma.mk a b' :: t = u ++ ⟨a, x⟩ :: w, from ⟨[], t, b', by simp⟩ },
@@ -380,7 +380,7 @@ begin
   { intro m3,
     have : a ∈ list.map sigma.fst t.as_list := list.mem_map_of_mem _ (t.mem_as_list.2 ⟨_, m3⟩),
     exact dj (list.mem_map_of_mem sigma.fst m1) this },
-  by_cases mk_idx n' (hash_fn c.1) = i with h,
+  by_cases h : mk_idx n' (hash_fn c.1) = i,
   { subst h,
     have e : sigma.mk a b' = ⟨c.1, c.2⟩,
     { simpa [reinsert_aux, bucket_array.modify, array.read_write, this] using im },
@@ -433,7 +433,7 @@ theorem mem_insert : Π (m : hash_map α β) (a b a' b'),
     if a = a' then b == b' else sigma.mk a' b' ∈ bkts.as_list,
   { intros bkts' v1 u w hl hfl veq,
     rw [hl, hfl],
-    by_cases a = a' with h,
+    by_cases h : a = a',
     { subst a',
       suffices : b = b' ∨ sigma.mk a b' ∈ u ∨ sigma.mk a b' ∈ w ↔ b = b',
       { simpa [eq_comm, or.left_comm] },
@@ -445,7 +445,7 @@ theorem mem_insert : Π (m : hash_map α β) (a b a' b'),
         simp [hl, list.nodup_append] at nd', simp [nd'] } },
     { suffices : sigma.mk a' b' ∉ v1, {simp [h, ne.symm h, this]},
       rcases veq with ⟨rfl, Hnc⟩ | ⟨b'', rfl⟩; simp [ne.symm h] } },
-  by_cases (contains_aux a bkt : Prop) with Hc,
+  by_cases Hc : (contains_aux a bkt : Prop),
   { rcases hash_map.valid.replace_aux a b (array.read bkts (mk_idx n (hash_fn a)))
       ((contains_aux_iff nd).1 Hc) with ⟨u', w', b'', hl', hfl'⟩,
     rcases (append_of_modify u' [⟨a, b''⟩] [⟨a, b⟩] w' hl' hfl') with ⟨u, w, hl, hfl⟩,
@@ -458,7 +458,7 @@ theorem mem_insert : Π (m : hash_map α β) (a b a' b'),
       let ⟨u, w, hl, hfl⟩ := append_of_modify [] [] [⟨a, b⟩] _ rfl rfl in
       lem bkts' _ u w hl hfl $ or.inl ⟨rfl, Hc⟩,
     simp [insert, @dif_neg (contains_aux a bkt) _ Hc],
-    by_cases size' ≤ n.1 with h,
+    by_cases h : size' ≤ n.1,
     -- TODO(Mario): Why does the by_cases assumption look different than the stated one?
     { simpa [show size' ≤ n.1, from h] using mi },
     { let n' : ℕ+ := ⟨n.1 * 2, mul_pos n.2 dec_trivial⟩,
@@ -514,7 +514,7 @@ theorem mem_erase : Π (m : hash_map α β) (a a' b'),
   a ≠ a' ∧ sigma.mk a' b' ∈ m.entries
 | ⟨hash_fn, size, n, bkts, v⟩ a a' b' := begin
   let bkt := bkts.read hash_fn a,
-  by_cases (contains_aux a bkt : Prop) with Hc,
+  by_cases Hc : (contains_aux a bkt : Prop),
   { let bkts' := bkts.modify hash_fn a (erase_aux a),
     suffices : sigma.mk a' b' ∈ bkts'.as_list ↔ a ≠ a' ∧ sigma.mk a' b' ∈ bkts.as_list,
     { simpa [erase, @dif_pos (contains_aux a bkt) _ Hc] },

data/list/basic.lean

@@ -550,7 +550,7 @@ assume n, if_neg n
 theorem index_of_eq_length {a : α} {l : list α} : index_of a l = length l ↔ a ∉ l :=
 begin
   induction l with b l ih; simp [-add_comm],
-  by_cases a = b with h; simp [h, -add_comm],
+  by_cases h : a = b; simp [h, -add_comm],
   { intro, contradiction },
   { rw ← ih, exact ⟨succ_inj, congr_arg _⟩ }
 end
@@ -561,7 +561,7 @@ index_of_eq_length.2
 theorem index_of_le_length {a : α} {l : list α} : index_of a l ≤ length l :=
 begin
   induction l with b l ih; simp [-add_comm, index_of_cons],
-  by_cases a = b with h; simp [h, -add_comm, zero_le],
+  by_cases h : a = b; simp [h, -add_comm, zero_le],
   exact succ_le_succ ih
 end
 
@@ -622,7 +622,7 @@ ext $ λn, if h₁ : n < length l₁
   else let h₁ := le_of_not_gt h₁ in by rw [nth_ge_len h₁, nth_ge_len (by rwa [← hl])]
 
 @[simp] theorem index_of_nth_le [decidable_eq α] {a : α} : ∀ {l : list α} h, nth_le l (index_of a l) h = a
-| (b::l) h := by by_cases a = b with h'; simp *
+| (b::l) h := by by_cases h' : a = b; simp *
 
 @[simp] theorem index_of_nth [decidable_eq α] {a : α} {l : list α} (h : a ∈ l) : nth l (index_of a l) = some a :=
 by rw [nth_le_nth, index_of_nth_le (index_of_lt_length.2 h)]
@@ -1129,7 +1129,7 @@ theorem filter_map_eq_filter (p : α → Prop) [decidable_pred p] :
 begin
   funext l,
   induction l with a l IH, {simp},
-  by_cases p a with pa; simp [filter_map, option.guard, pa, IH]
+  by_cases pa : p a; simp [filter_map, option.guard, pa, IH]
 end
 
 theorem filter_map_filter_map (f : α → option β) (g : β → option γ) (l : list α) :
@@ -1253,11 +1253,11 @@ by rw ← filter_map_eq_filter; exact filter_map_sublist_filter_map _ s
 
 @[simp] theorem span_eq_take_drop (p : α → Prop) [decidable_pred p] : ∀ (l : list α), span p l = (take_while p l, drop_while p l)
 | []     := rfl
-| (a::l) := by by_cases p a with pa; simp [span, take_while, drop_while, pa, span_eq_take_drop l]
+| (a::l) := by by_cases pa : p a; simp [span, take_while, drop_while, pa, span_eq_take_drop l]
 
 @[simp] theorem take_while_append_drop (p : α → Prop) [decidable_pred p] : ∀ (l : list α), take_while p l ++ drop_while p l = l
 | []     := rfl
-| (a::l) := by by_cases p a with pa; simp [take_while, drop_while, pa, take_while_append_drop l]
+| (a::l) := by by_cases pa : p a; simp [take_while, drop_while, pa, take_while_append_drop l]
 
 def countp (p : α → Prop) [decidable_pred p] : list α → nat
 | []      := 0
@@ -1621,7 +1621,7 @@ by simp [insert.def, h]
 
 @[simp] theorem mem_insert_iff {a b : α} {l : list α} : a ∈ insert b l ↔ a = b ∨ a ∈ l :=
 begin
-  by_cases b ∈ l with h'; simp [h'],
+  by_cases h' : b ∈ l; simp [h'],
   apply (or_iff_right_of_imp _).symm,
   exact λ e, e.symm ▸ h'
 end
@@ -1670,7 +1670,7 @@ theorem exists_erase_eq {a : α} {l : list α} (h : a ∈ l) :
   ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂ :=
 by induction l with b l ih; [cases h, {
   simp at h,
-  by_cases b = a with e,
+  by_cases e : b = a,
   { subst b, exact ⟨[], l, not_mem_nil _, rfl, by simp⟩ },
   { exact let ⟨l₁, l₂, h₁, h₂, h₃⟩ := ih (h.resolve_left (ne.symm e)) in
     ⟨b::l₁, l₂, not_mem_cons_of_ne_of_not_mem (ne.symm e) h₁,
@@ -1684,7 +1684,7 @@ end
 
 theorem erase_append_left {a : α} : ∀ {l₁ : list α} (l₂), a ∈ l₁ → (l₁++l₂).erase a = l₁.erase a ++ l₂
 | (x::xs) l₂  h := begin
-  by_cases x = a with h'; simp [h'],
+  by_cases h' : x = a; simp [h'],
   rw erase_append_left l₂ (mem_of_ne_of_mem (ne.symm h') h)
 end
 
@@ -1939,7 +1939,7 @@ mem_union.2 (or.inr h)
 theorem sublist_suffix_of_union : ∀ l₁ l₂ : list α, ∃ t, t <+ l₁ ∧ t ++ l₂ = l₁ ∪ l₂
 | [] l₂ := ⟨[], by refl, rfl⟩
 | (a::l₁) l₂ := let ⟨t, s, e⟩ := sublist_suffix_of_union l₁ l₂ in
-  by simp [e.symm]; by_cases a ∈ t ++ l₂ with h;
+  by simp [e.symm]; by_cases h : a ∈ t ++ l₂;
      [existsi t, existsi a::t]; simp [h];
      [apply sublist_cons_of_sublist _ s, apply cons_sublist_cons _ s]
 
@@ -2036,7 +2036,7 @@ theorem mem_bag_inter {a : α} : ∀ {l₁ l₂ : list α}, a ∈ l₁.bag_inter
 | []      l₂ := by simp
 | (b::l₁) l₂ := by
   by_cases b ∈ l₂; simp [*, and_or_distrib_left];
-  by_cases a = b with ba; simp *
+  by_cases ba : a = b; simp *
 
 theorem bag_inter_sublist_left : ∀ l₁ l₂ : list α, l₁.bag_inter l₂ <+ l₁
 | []      l₂ := by simp [nil_sublist]
@@ -2523,7 +2523,7 @@ theorem nodup_concat {a : α} {l : list α} (h : a ∉ l) (h' : nodup l) : nodup
 by simp; exact nodup_append_of_nodup h' (nodup_singleton _) (disjoint_singleton.2 h)
 
 theorem nodup_insert [decidable_eq α] {a : α} {l : list α} (h : nodup l) : nodup (insert a l) :=
-by by_cases a ∈ l with h'; simp [h', h]; apply nodup_cons h' h
+by by_cases h' : a ∈ l; simp [h', h]; apply nodup_cons h' h
 
 theorem nodup_union [decidable_eq α] (l₁ : list α) {l₂ : list α} (h : nodup l₂) :
   nodup (l₁ ∪ l₂) :=

data/list/perm.lean

@@ -432,7 +432,7 @@ begin
   induction h with x _ _ _ _ x y _ _ _ _ _ _ ih_1 ih_2 generalizing t, {simp},
   { by_cases x ∈ t; simp [*, skip] },
   { by_cases x = y, {simp [h]},
-    by_cases x ∈ t with xt; by_cases y ∈ t with yt,
+    by_cases xt : x ∈ t; by_cases yt : y ∈ t,
     { simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (ne.symm h), erase_comm, swap] },
     { simp [xt, yt, mt mem_of_mem_erase, skip] },
     { simp [xt, yt, mt mem_of_mem_erase, skip] },
@@ -489,8 +489,8 @@ else by simpa [h, mt (mem_of_perm p).2 h] using skip a p
 theorem perm_insert_swap (x y : α) (l : list α) :
   insert x (insert y l) ~ insert y (insert x l) :=
 begin
-  by_cases x ∈ l with xl; by_cases y ∈ l with yl; simp [xl, yl],
-  by_cases x = y with xy, { simp [xy] },
+  by_cases xl : x ∈ l; by_cases yl : y ∈ l; simp [xl, yl],
+  by_cases xy : x = y, { simp [xy] },
   simp [not_mem_cons_of_ne_of_not_mem xy xl,
         not_mem_cons_of_ne_of_not_mem (ne.symm xy) yl],
   constructor

data/list/sort.lean

@@ -93,7 +93,7 @@ include totr transr
 theorem sorted_ordered_insert (a : α) : ∀ l, sorted r l → sorted r (ordered_insert a l)
 | []       h := sorted_singleton a
 | (b :: l) h := begin
-  by_cases a ≼ b with h',
+  by_cases h' : a ≼ b,
   { simpa [ordered_insert, h', h] using λ b' bm, transr h' (rel_of_sorted_cons h _ bm) },
   { suffices : ∀ (b' : α), b' ∈ ordered_insert r a l → r b b',
     { simpa [ordered_insert, h', sorted_ordered_insert l (sorted_of_sorted_cons h)] },