diff --git a/algebra/big_operators.lean b/algebra/big_operators.lean
index 9969f09ba8a44..b51a7212e5a2b 100644
--- a/algebra/big_operators.lean
+++ b/algebra/big_operators.lean
@@ -7,6 +7,7 @@ Some big operators for lists and finite sets.
 -/
 import data.list.basic data.list.perm data.finset
   algebra.group algebra.ordered_group algebra.group_power
+  tactic.squeeze
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
@@ -15,7 +16,7 @@ theorem directed.finset_le {r : α → α → Prop} [is_trans α r]
   {ι} (hι : nonempty ι) {f : ι → α} (D : directed r f) (s : finset ι) :
   ∃ z, ∀ i ∈ s, r (f i) (f z) :=
 show ∃ z, ∀ i ∈ s.1, r (f i) (f z), from
-multiset.induction_on s.1 (match hι with ⟨z⟩ := ⟨z, λ _, false.elim⟩ end) $
+multiset.induction_on s.1 (let ⟨z⟩ := hι in ⟨z, λ _, false.elim⟩) $
 λ i s ⟨j, H⟩, let ⟨k, h₁, h₂⟩ := D i j in
 ⟨k, λ a h, or.cases_on (multiset.mem_cons.1 h)
   (λ h, h.symm ▸ h₁)
@@ -373,7 +374,7 @@ lemma prod_sum {δ : α → Type*} [∀a, decidable_eq (δ a)]
 begin
   induction s using finset.induction with a s ha ih,
   { rw [pi_empty, sum_singleton], refl },
-  { have h₁ : ∀x ∈ t a, ∀y∈t a, ∀h : x ≠ y,
+  { have h₁ : ∀x ∈ t a, ∀y ∈ t a, ∀h : x ≠ y,
         image (pi.cons s a x) (pi s t) ∩ image (pi.cons s a y) (pi s t) = ∅,
     { assume x hx y hy h,
       apply eq_empty_of_forall_not_mem,
@@ -381,21 +382,20 @@ begin
       rintro p₁ ⟨⟨p₂, hp, eq⟩, ⟨p₃, hp₃, rfl⟩⟩,
       have : pi.cons s a x p₂ a (mem_insert_self _ _) = pi.cons s a y p₃ a (mem_insert_self _ _),
       { rw [eq] },
-      rw [pi.cons_same, pi.cons_same] at this, cc },
+      rw [pi.cons_same, pi.cons_same] at this,
+      exact h this },
     rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_bind h₁],
-    refine sum_congr rfl (λ x hx, _),
-    have h₂ : ∀p₁∈pi s t, ∀p₂∈pi s t, pi.cons s a x p₁ = pi.cons s a x p₂ → p₁ = p₂, from
+    refine sum_congr rfl (λ b _, _),
+    have h₂ : ∀p₁∈pi s t, ∀p₂∈pi s t, pi.cons s a b p₁ = pi.cons s a b p₂ → p₁ = p₂, from
       assume p₁ h₁ p₂ h₂ eq, injective_pi_cons ha eq,
     rw [sum_image h₂, mul_sum],
-    refine sum_congr rfl (λ g hg, _),
-    have h₃ : ∀ x ∈ attach s, ∀ y ∈ attach s, (⟨x.1, mem_insert_of_mem x.2⟩ : {x // x ∈ insert a s}) = ⟨y.1, mem_insert_of_mem y.2⟩ → x = y, from
-      λ _ _ _ _, subtype.eq ∘ subtype.mk.inj,
-    have h₄ : (⟨a, _⟩ : {x // x ∈ insert a s}) ∉ image (λ (x : {x // x ∈ s}), (⟨x.1, _⟩ : {x // x ∈ insert a s})) (attach s),
-    { simp only [mem_image], rintro ⟨⟨_, _⟩, _, rfl⟩, cc },
-    rw [attach_insert, prod_insert h₄, prod_image h₃],
-    simp only [pi.cons_same],
-    refine congr_arg _ (prod_congr rfl (λ v hv, congr_arg _ _)),
-    exact (pi.cons_ne (by rintro rfl; exact ha v.2)).symm }
+    refine sum_congr rfl (λ g _, _),
+    rw [attach_insert, prod_insert, prod_image],
+    { simp only [pi.cons_same],
+      congr', ext ⟨v, hv⟩, congr',
+      exact (pi.cons_ne (by rintro rfl; exact ha hv)).symm },
+    { exact λ _ _ _ _, subtype.eq ∘ subtype.mk.inj },
+    { simp only [mem_image], rintro ⟨⟨_, hm⟩, _, rfl⟩, exact ha hm } }
 end
 
 end comm_semiring
@@ -404,13 +404,9 @@ section integral_domain /- add integral_semi_domain to support nat and ennreal -
 variables [decidable_eq α] [integral_domain β]
 
 lemma prod_eq_zero_iff : s.prod f = 0 ↔ (∃a∈s, f a = 0) :=
-finset.induction_on s ⟨false.elim ∘ one_ne_zero, λ ⟨_, H, _⟩, H.elim⟩
-begin
-  intros a s ha,
-  rw [bex_def, bex_def, exists_mem_insert],
-  intro ih,
-  simp only [prod_insert ha, mul_eq_zero_iff_eq_zero_or_eq_zero, ih]
-end
+finset.induction_on s ⟨not.elim one_ne_zero, λ ⟨_, H, _⟩, H.elim⟩ $ λ a s ha ih,
+by rw [prod_insert ha, mul_eq_zero_iff_eq_zero_or_eq_zero,
+  bex_def, exists_mem_insert, ih, ← bex_def]
 
 end integral_domain
 
@@ -436,9 +432,9 @@ calc s₁.sum f ≤ (s₂ \ s₁).sum f + s₁.sum f :
 lemma sum_eq_zero_iff_of_nonneg : (∀x∈s, 0 ≤ f x) → (s.sum f = 0 ↔ ∀x∈s, f x = 0) :=
 finset.induction_on s (λ _, ⟨λ _ _, false.elim, λ _, rfl⟩) $ λ a s ha ih H,
 have ∀ x ∈ s, 0 ≤ f x, from λ _, H _ ∘ mem_insert_of_mem,
-⟨by rw [sum_insert ha, add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg' (H _ $ mem_insert_self _ _) (zero_le_sum' this)];
-  simp only [mem_insert]; rintro ⟨_, _⟩ x (rfl | h2); cases ih this; solve_by_elim,
-λ h1, (sum_congr rfl h1).trans sum_const_zero⟩
+by rw [sum_insert ha,
+  add_eq_zero_iff' (H _ $ mem_insert_self _ _) (zero_le_sum' this),
+  forall_mem_insert, ih this]
 
 lemma single_le_sum (hf : ∀x∈s, 0 ≤ f x) {a} (h : a ∈ s) : f a ≤ s.sum f :=
 have (singleton a).sum f ≤ s.sum f,
diff --git a/algebra/euclidean_domain.lean b/algebra/euclidean_domain.lean
index 9035b74387d64..a0027a6145b29 100644
--- a/algebra/euclidean_domain.lean
+++ b/algebra/euclidean_domain.lean
@@ -200,9 +200,9 @@ theorem xgcd_aux_P (a b : α) {r r' : α} : ∀ {s t s' t'}, P a b (r, s, t) →
   P a b (r', s', t') → P a b (xgcd_aux r s t r' s' t') :=
 gcd.induction r r' (by intros; simpa only [xgcd_zero_left]) $ λ x y h IH s t s' t' p p', begin
   rw [xgcd_aux_rec h], refine IH _ p, unfold P at p p' ⊢,
-  conv {to_lhs, rw mod_eq_sub_mul_div, congr, rw p', skip, congr, rw p },
-  rw [add_mul, mul_sub, mul_sub, sub_add_eq_sub_sub, add_sub, sub_add_eq_add_sub],
-  simp only [mul_assoc, mul_comm, mul_left_comm]
+  rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub,
+    mul_comm _ s, ← mul_assoc, mul_comm _ t, ← mul_assoc, ← add_mul, ← p,
+    mod_eq_sub_mul_div]
 end
 
 theorem gcd_eq_gcd_ab (a b : α) : (gcd a b : α) = a * gcd_a a b + b * gcd_b a b :=
diff --git a/algebra/field.lean b/algebra/field.lean
index ce65738c01f52..8950f3202da28 100644
--- a/algebra/field.lean
+++ b/algebra/field.lean
@@ -155,9 +155,6 @@ variables [discrete_field α] {a b c : α}
 
 attribute [simp] inv_zero div_zero
 
-lemma inv_sub_inv_eq (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b) :=
-inv_sub_inv ha hb
-
 lemma div_right_comm (a b c : α) : (a / b) / c = (a / c) / b :=
 if b0 : b = 0 then by simp only [b0, div_zero, zero_div] else
 if c0 : c = 0 then by simp only [c0, div_zero, zero_div] else
diff --git a/algebra/gcd_domain.lean b/algebra/gcd_domain.lean
index 64c2474fa560b..e062829a4f121 100644
--- a/algebra/gcd_domain.lean
+++ b/algebra/gcd_domain.lean
@@ -189,7 +189,7 @@ end gcd
 
 section lcm
 
-lemma lcm_dvd_iff (a b c : α) : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c :=
+lemma lcm_dvd_iff {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c :=
 classical.by_cases
   (assume : a = 0 ∨ b = 0, by rcases this with rfl | rfl;
     simp only [iff_def, lcm_zero_left, lcm_zero_right, zero_dvd_iff, dvd_zero,
@@ -202,14 +202,12 @@ classical.by_cases
         ← gcd_mul_left, dvd_gcd_iff, mul_comm c a, mul_dvd_mul_iff_left h1,
         mul_dvd_mul_iff_right h2, and_comm])
 
-lemma dvd_lcm_left (a b : α) : a ∣ lcm a b :=
-((lcm_dvd_iff _ _ _).1 (dvd_refl _)).1
+lemma dvd_lcm_left (a b : α) : a ∣ lcm a b := (lcm_dvd_iff.1 (dvd_refl _)).1
 
-lemma dvd_lcm_right (a b : α) : b ∣ lcm a b :=
-((lcm_dvd_iff _ _ _).1 (dvd_refl _)).2
+lemma dvd_lcm_right (a b : α) : b ∣ lcm a b := (lcm_dvd_iff.1 (dvd_refl _)).2
 
 lemma lcm_dvd {a b c : α} (hab : a ∣ b) (hcb : c ∣ b) : lcm a c ∣ b :=
-(lcm_dvd_iff _ _ _).2 ⟨hab, hcb⟩
+lcm_dvd_iff.2 ⟨hab, hcb⟩
 
 @[simp] theorem lcm_eq_zero_iff (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b = 0 :=
 iff.intro
diff --git a/algebra/group_power.lean b/algebra/group_power.lean
index e81a63fa4a738..8de2c7b6246f6 100644
--- a/algebra/group_power.lean
+++ b/algebra/group_power.lean
@@ -354,13 +354,11 @@ theorem is_semiring_hom.map_pow {β} [semiring α] [semiring β]
 by induction n with n ih; [exact is_semiring_hom.map_one f,
   rw [pow_succ, pow_succ, is_semiring_hom.map_mul f, ih]]
 
-theorem neg_one_pow_eq_or {R} [ring R] (n : ℕ) : (-1 : R)^n = 1 ∨ (-1 : R)^n = -1 :=
-begin
-  induction n with n ih, {left, refl},
-  cases ih with h h,
-  { right, rw [pow_succ, h, mul_one] },
-  { left, rw [pow_succ, h, neg_one_mul, neg_neg] }
-end
+theorem neg_one_pow_eq_or {R} [ring R] : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n = -1
+| 0     := or.inl rfl
+| (n+1) := (neg_one_pow_eq_or n).swap.imp
+  (λ h, by rw [pow_succ, h, neg_one_mul, neg_neg])
+  (λ h, by rw [pow_succ, h, mul_one])
 
 theorem gsmul_eq_mul [ring α] (a : α) : ∀ n, n •ℤ a = n * a
 | (n : ℕ) := add_monoid.smul_eq_mul _ _
@@ -384,11 +382,10 @@ by rw [← nat.mod_add_div n 2, pow_add, pow_mul]; simp [pow_two]
 
 theorem pow_ne_zero [domain α] {a : α} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 begin
-  induction n with n ih, { exact one_ne_zero },
+  induction n with n ih, {exact one_ne_zero},
   intro H,
   cases mul_eq_zero.1 H with h1 h1,
-  { exact h h1 },
-  { exact ih h1 }
+  exacts [h h1, ih h1]
 end
 
 @[simp] theorem one_div_pow [division_ring α] {a : α} (ha : a ≠ 0) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n :=
@@ -499,6 +496,7 @@ lemma units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) : u ^ n = u ^ (n % 2) :
 by conv {to_lhs, rw ← nat.mod_add_div n 2}; rw [pow_add, pow_mul, units_pow_two, one_pow, mul_one]
 
 end int
+
 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
 by simp [pow, monoid.pow]
 
diff --git a/algebra/ordered_group.lean b/algebra/ordered_group.lean
index 23d992985922c..dec1c227c7f17 100644
--- a/algebra/ordered_group.lean
+++ b/algebra/ordered_group.lean
@@ -119,8 +119,7 @@ add_lt_of_nonpos_of_lt' (le_of_lt ha) hbc
 lemma add_lt_of_lt_of_neg' (hbc : b < c) (ha : a < 0) : b + a < c :=
 add_lt_of_lt_of_nonpos' hbc (le_of_lt ha)
 
-lemma add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg'
-  (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
+lemma add_eq_zero_iff' (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
 iff.intro
   (assume hab : a + b = 0,
    have a ≤ 0, from hab ▸ le_add_of_le_of_nonneg' (le_refl _) hb,
@@ -340,7 +339,7 @@ canonically_ordered_monoid.le_iff_exists_add a b
 @[simp] lemma zero_le (a : α) : 0 ≤ a := le_iff_exists_add.mpr ⟨a, by simp⟩
 
 @[simp] lemma add_eq_zero_iff : a + b = 0 ↔ a = 0 ∧ b = 0 :=
-add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg' (zero_le _) (zero_le _)
+add_eq_zero_iff' (zero_le _) (zero_le _)
 
 @[simp] lemma le_zero_iff_eq : a ≤ 0 ↔ a = 0 :=
 iff.intro
diff --git a/analysis/topology/topological_space.lean b/analysis/topology/topological_space.lean
index 83d2345b248f0..22dd30c8427a1 100644
--- a/analysis/topology/topological_space.lean
+++ b/analysis/topology/topological_space.lean
@@ -55,27 +55,23 @@ rfl
 
 variables [topological_space α]
 
-lemma is_open_union (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∪ s₂) :=
-have (⋃₀ {s₁, s₂}) = (s₁ ∪ s₂), from (sUnion_insert _ _).trans $ by rw [sUnion_singleton, union_comm],
-this ▸ is_open_sUnion $ show ∀(t : set α), t ∈ ({s₁, s₂} : set (set α)) → is_open t,
-  from by rintro t (rfl|⟨rfl|ht⟩); [exact h₂, exact h₁, cases ht]
-
 lemma is_open_Union {f : ι → set α} (h : ∀i, is_open (f i)) : is_open (⋃i, f i) :=
-is_open_sUnion $ assume t ⟨i, (heq : t = f i)⟩, heq.symm ▸ h i
+is_open_sUnion $ by rintro _ ⟨i, rfl⟩; exact h i
 
 lemma is_open_bUnion {s : set β} {f : β → set α} (h : ∀i∈s, is_open (f i)) :
   is_open (⋃i∈s, f i) :=
 is_open_Union $ assume i, is_open_Union $ assume hi, h i hi
 
+lemma is_open_union (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∪ s₂) :=
+by rw union_eq_Union; exact is_open_Union (bool.forall_bool.2 ⟨h₂, h₁⟩)
+
 @[simp] lemma is_open_empty : is_open (∅ : set α) :=
-have is_open (⋃₀ ∅ : set α), from is_open_sUnion (assume a, false.elim),
-by rwa sUnion_empty at this
+by rw ← sUnion_empty; exact is_open_sUnion (assume a, false.elim)
 
 lemma is_open_sInter {s : set (set α)} (hs : finite s) : (∀t ∈ s, is_open t) → is_open (⋂₀ s) :=
-finite.induction_on hs (λ _, by rw sInter_empty; exact is_open_univ) $ λ a s has hs ih h, begin
-  suffices : is_open (a ∩ ⋂₀ s), { rwa sInter_insert },
-  exact is_open_inter (h _ $ mem_insert _ _) (ih $ assume t ht, h _ $ mem_insert_of_mem _ ht)
-end
+finite.induction_on hs (λ _, by rw sInter_empty; exact is_open_univ) $
+λ a s has hs ih h, by rw sInter_insert; exact
+is_open_inter (h _ $ mem_insert _ _) (ih $ λ t, h t ∘ mem_insert_of_mem _)
 
 lemma is_open_bInter {s : set β} {f : β → set α} (hs : finite s) :
   (∀i∈s, is_open (f i)) → is_open (⋂i∈s, f i) :=
@@ -562,7 +558,7 @@ lemma compact_of_finite_subcover {s : set α}
   (h : ∀c, (∀t∈c, is_open t) → s ⊆ ⋃₀ c → ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c') : compact s :=
 assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, f ⊓ nhds x ≠ ⊥),
   have hf : ∀x∈s, nhds x ⊓ f = ⊥,
-    by simpa only [not_exists, not_not, inf_comm] using this,
+    by simpa only [not_exists, not_not, inf_comm],
   have ¬ ∃x∈s, ∀t∈f.sets, x ∈ closure t,
     from assume ⟨x, hxs, hx⟩,
     have ∅ ∈ (nhds x ⊓ f).sets, by rw [empty_in_sets_eq_bot, hf x hxs],
@@ -572,7 +568,7 @@ assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, f ⊓ nhds
     have nhds x ⊓ principal t₂ = ⊥,
       by rwa [empty_in_sets_eq_bot] at this,
     by simp only [closure_eq_nhds] at hx; exact hx t₂ ht₂ this,
-  have ∀x∈s, ∃t∈f.sets, x ∉ closure t, by simpa only [not_exists, not_forall] using this,
+  have ∀x∈s, ∃t∈f.sets, x ∉ closure t, by simpa only [not_exists, not_forall],
   let c := (λt, - closure t) '' f.sets, ⟨c', hcc', hcf, hsc'⟩ := h c
     (assume t ⟨s, hs, h⟩, h ▸ is_closed_closure) (by simpa only [subset_def, sUnion_image, mem_Union]) in
   let ⟨b, hb⟩ := axiom_of_choice $
@@ -1022,8 +1018,7 @@ end
 
 lemma quotient_dense_of_dense [setoid α] [topological_space α] {s : set α} (H : ∀ x, x ∈ closure s) :
   closure (quotient.mk '' s) = univ :=
-begin
-  refine eq_univ_of_forall (λ x, _),
+eq_univ_of_forall $ λ x, begin
   rw mem_closure_iff,
   intros U U_op x_in_U,
   let V := quotient.mk ⁻¹' U,
@@ -1032,7 +1027,7 @@ begin
   have V_op : is_open V := U_op,
   have : V ∩ s ≠ ∅ := mem_closure_iff.1 (H y) V V_op y_in_V,
   rcases exists_mem_of_ne_empty this with ⟨w, w_in_V, w_in_range⟩,
-  exact ne_empty_of_mem ⟨by tauto, mem_image_of_mem quotient.mk w_in_range⟩
+  exact ne_empty_of_mem ⟨w_in_V, mem_image_of_mem quotient.mk w_in_range⟩
 end
 
 lemma generate_from_le {t : topological_space α} { g : set (set α) } (h : ∀s∈g, is_open s) :
@@ -1157,8 +1152,8 @@ begin
       let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ this in
       ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (subset.trans hu₃ (inter_subset_left _ _)),
         le_principal_iff.2 (subset.trans hu₃ (inter_subset_right _ _))⟩ },
-  { suffices : a ∈ (⋃₀ b), { rcases this with ⟨i, h1, h2⟩, exact ⟨i, h2, h1⟩ },
-    { rw [hb.2.1], trivial } }
+  { rcases eq_univ_iff_forall.1 hb.2.1 a with ⟨i, h1, h2⟩,
+    exact ⟨i, h2, h1⟩ }
 end
 
 lemma is_open_of_is_topological_basis {s : set α} {b : set (set α)}
diff --git a/data/finset.lean b/data/finset.lean
index 9bca502ed8852..74f9a83b03524 100644
--- a/data/finset.lean
+++ b/data/finset.lean
@@ -142,8 +142,7 @@ theorem subset_empty {s : finset α} : s ⊆ ∅ ↔ s = ∅ := subset_zero.tran
 theorem exists_mem_of_ne_empty {s : finset α} (h : s ≠ ∅) : ∃ a : α, a ∈ s :=
 exists_mem_of_ne_zero (mt val_eq_zero.1 h)
 
-@[simp] lemma coe_empty : ↑(∅ : finset α) = (∅ : set α) :=
-rfl
+@[simp] lemma coe_empty : ↑(∅ : finset α) = (∅ : set α) := rfl
 
 /-- `singleton a` is the set `{a}` containing `a` and nothing else. -/
 def singleton (a : α) : finset α := ⟨_, nodup_singleton a⟩
@@ -151,8 +150,7 @@ local prefix `ι`:90 := singleton
 
 @[simp] theorem singleton_val (a : α) : (ι a).1 = a :: 0 := rfl
 
-@[simp] theorem mem_singleton {a b : α} : b ∈ ι a ↔ b = a :=
-mem_singleton
+@[simp] theorem mem_singleton {a b : α} : b ∈ ι a ↔ b = a := mem_singleton
 
 theorem not_mem_singleton {a b : α} : a ∉ ι b ↔ a ≠ b := not_iff_not_of_iff mem_singleton
 
@@ -163,8 +161,7 @@ theorem singleton_inj {a b : α} : ι a = ι b ↔ a = b :=
 
 @[simp] theorem singleton_ne_empty (a : α) : ι a ≠ ∅ := ne_empty_of_mem (mem_singleton_self _)
 
-@[simp] lemma coe_singleton (a : α) : ↑(ι a) = ({a} : set α) :=
-rfl
+@[simp] lemma coe_singleton (a : α) : ↑(ι a) = ({a} : set α) := rfl
 
 /- insert -/
 section decidable_eq
@@ -377,7 +374,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 $ λ x, have x = a ∧ x ∈ s₂ ↔ false, from (iff_false _).2 $ by rintro ⟨rfl, H⟩; cc,
+ext.2 $ λ x, have ¬ (x = a ∧ x ∈ s₂), by rintro ⟨rfl, H⟩; exact h H,
 by simp only [mem_inter, mem_insert, or_and_distrib_right, this, false_or]
 
 @[simp] theorem inter_insert_of_not_mem {s₁ s₂ : finset α} {a : α} (h : a ∉ s₁) :
@@ -388,7 +385,7 @@ by rw [inter_comm, insert_inter_of_not_mem h, inter_comm]
 show insert a ∅ ∩ s = insert a ∅, by rw [insert_inter_of_mem H, empty_inter]
 
 @[simp] theorem singleton_inter_of_not_mem {a : α} {s : finset α} (H : a ∉ s) : ι a ∩ s = ∅ :=
-eq_empty_of_forall_not_mem $ by simp only [mem_inter, mem_singleton]; rintro x ⟨rfl, H⟩; cc
+eq_empty_of_forall_not_mem $ by simp only [mem_inter, mem_singleton]; rintro x ⟨rfl, h⟩; exact H h
 
 @[simp] theorem inter_singleton_of_mem {a : α} {s : finset α} (h : a ∈ s) : s ∩ ι a = ι a :=
 by rw [inter_comm, singleton_inter_of_mem h]
@@ -454,7 +451,7 @@ by simp only [mem_erase]; exact and.intro
 
 theorem erase_insert {a : α} {s : finset α} (h : a ∉ s) : erase (insert a s) a = s :=
 ext.2 $ assume x, by simp only [mem_erase, mem_insert, and_or_distrib_left, not_and_self, false_or];
-apply and_iff_right_of_imp; rintro H rfl; cc
+apply and_iff_right_of_imp; rintro H rfl; exact h H
 
 theorem insert_erase {a : α} {s : finset α} (h : a ∈ s) : insert a (erase s a) = s :=
 ext.2 $ assume x, by simp only [mem_insert, mem_erase, or_and_distrib_left, dec_em, true_and];
@@ -494,13 +491,15 @@ instance : has_sdiff (finset α) := ⟨λs₁ s₂, ⟨s₁.1 - s₂.1, nodup_of
   a ∈ s₁ \ s₂ ↔ a ∈ s₁ ∧ a ∉ s₂ := mem_sub_of_nodup s₁.2
 
 @[simp] theorem sdiff_union_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : (s₂ \ s₁) ∪ s₁ = s₂ :=
-ext.2 $ λ a, by simpa only [mem_sdiff, mem_union, or_comm, or_and_distrib_left, dec_em, and_true] using or_iff_right_of_imp (@h a)
+ext.2 $ λ a, by simpa only [mem_sdiff, mem_union, or_comm,
+  or_and_distrib_left, dec_em, and_true] using or_iff_right_of_imp (@h a)
 
 @[simp] theorem union_sdiff_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : s₁ ∪ (s₂ \ s₁) = s₂ :=
 (union_comm _ _).trans (sdiff_union_of_subset h)
 
 @[simp] theorem inter_sdiff_self (s₁ s₂ : finset α) : s₁ ∩ (s₂ \ s₁) = ∅ :=
-eq_empty_of_forall_not_mem $ by simp only [mem_inter, mem_sdiff]; rintro x ⟨h1, h2, h3⟩; cc
+eq_empty_of_forall_not_mem $
+by simp only [mem_inter, mem_sdiff]; rintro x ⟨h, _, hn⟩; exact hn h
 
 @[simp] theorem sdiff_inter_self (s₁ s₂ : finset α) : (s₂ \ s₁) ∩ s₁ = ∅ :=
 (inter_comm _ _).trans (inter_sdiff_self _ _)
@@ -761,9 +760,9 @@ ext.2 $ λ _, by simp only [mem_map, mem_union, exists_prop, or_and_distrib_righ
 
 theorem map_inter [decidable_eq α] [decidable_eq β]
   {f : α ↪ β} (s₁ s₂ : finset α) : (s₁ ∩ s₂).map f = s₁.map f ∩ s₂.map f :=
-ext.2 $ λ b, by simp only [mem_map, mem_inter, exists_prop, and_assoc]; exact
-⟨by rintro ⟨a, m₁, m₂, rfl⟩; exact ⟨⟨a, m₁, rfl⟩, ⟨a, m₂, rfl⟩⟩,
-by rintro ⟨⟨a, m₁, e⟩, ⟨a', m₂, rfl⟩⟩; cases f.2 e; exact ⟨_, m₁, m₂, rfl⟩⟩
+ext.2 $ λ b, by simp only [mem_map, mem_inter, exists_prop]; exact
+⟨by rintro ⟨a, ⟨m₁, m₂⟩, rfl⟩; exact ⟨⟨a, m₁, rfl⟩, ⟨a, m₂, rfl⟩⟩,
+by rintro ⟨⟨a, m₁, e⟩, ⟨a', m₂, rfl⟩⟩; cases f.2 e; exact ⟨_, ⟨m₁, m₂⟩, rfl⟩⟩
 
 @[simp] theorem map_singleton (f : α ↪ β) (a : α) : (singleton a).map f = singleton (f a) :=
 ext.2 $ λ _, by simp only [mem_map, mem_singleton, exists_prop, exists_eq_left]; exact eq_comm
@@ -820,9 +819,9 @@ by simp only [subset_def, image_val, subset_erase_dup', erase_dup_subset', multi
 
 theorem image_filter {p : β → Prop} [decidable_pred p] :
   (s.image f).filter p = (s.filter (p ∘ f)).image f :=
-ext.2 $ λ b, by simp only [mem_filter, mem_image, exists_prop, and_assoc]; exact
-⟨by rintro ⟨⟨x, h1, rfl⟩, h2⟩; exact ⟨x, h1, h2, rfl⟩,
-by rintro ⟨x, h1, h2, rfl⟩; exact ⟨⟨x, h1, rfl⟩, h2⟩⟩
+ext.2 $ λ b, by simp only [mem_filter, mem_image, exists_prop]; exact
+⟨by rintro ⟨⟨x, h1, rfl⟩, h2⟩; exact ⟨x, ⟨h1, h2⟩, rfl⟩,
+ by rintro ⟨x, ⟨h1, h2⟩, rfl⟩; exact ⟨⟨x, h1, rfl⟩, h2⟩⟩
 
 theorem image_union [decidable_eq α] {f : α → β} (s₁ s₂ : finset α) : (s₁ ∪ s₂).image f = s₁.image f ∪ s₂.image f :=
 ext.2 $ λ _, by simp only [mem_image, mem_union, exists_prop, or_and_distrib_right, exists_or_distrib]
@@ -858,7 +857,8 @@ theorem map_eq_image (f : α ↪ β) (s : finset α) : s.map f = s.image f :=
 eq_of_veq $ (multiset.erase_dup_eq_self.2 (s.map f).2).symm
 
 lemma image_const [decidable_eq β] {s : finset α} (h : s ≠ ∅) (b : β) : s.image (λa, b) = singleton b :=
-ext.2 $ assume b', by simp only [mem_image, exists_prop, exists_and_distrib_right, exists_mem_of_ne_empty h, true_and, mem_singleton, eq_comm]
+ext.2 $ assume b', by simp only [mem_image, exists_prop, exists_and_distrib_right,
+  exists_mem_of_ne_empty h, true_and, mem_singleton, eq_comm]
 
 end image
 
@@ -878,8 +878,10 @@ card_eq_zero.trans val_eq_zero
 theorem card_pos {s : finset α} : 0 < card s ↔ s ≠ ∅ :=
 pos_iff_ne_zero.trans $ not_congr card_eq_zero
 
-@[simp] theorem card_insert_of_not_mem [decidable_eq α] {a : α} {s : finset α} (h : a ∉ s) : card (insert a s) = card s + 1 :=
-by simpa only [card_cons, card, insert_val] using congr_arg multiset.card (ndinsert_of_not_mem h)
+@[simp] theorem card_insert_of_not_mem [decidable_eq α]
+  {a : α} {s : finset α} (h : a ∉ s) : card (insert a s) = card s + 1 :=
+by simpa only [card_cons, card, insert_val] using
+congr_arg multiset.card (ndinsert_of_not_mem h)
 
 theorem card_insert_le [decidable_eq α] (a : α) (s : finset α) : card (insert a s) ≤ card s + 1 :=
 by by_cases a ∈ s; [{rw [insert_eq_of_mem h], apply nat.le_add_right},
@@ -1018,7 +1020,8 @@ by simp only [mem_def, bind_val, mem_erase_dup, mem_bind, exists_prop]
 
 @[simp] theorem bind_insert [decidable_eq α] {a : α} : (insert a s).bind t = t a ∪ s.bind t :=
 ext.2 $ λ x, by simp only [mem_bind, exists_prop, mem_union, mem_insert,
-  or_and_distrib_right, exists_or_distrib, exists_eq_left] --by simp [or_and_distrib_right, exists_or_distrib]
+  or_and_distrib_right, exists_or_distrib, exists_eq_left]
+-- ext.2 $ λ x, by simp [or_and_distrib_right, exists_or_distrib]
 
 @[simp] lemma singleton_bind [decidable_eq α] {a : α} : (singleton a).bind t = t a :=
 show (insert a ∅ : finset α).bind t = t a, from bind_insert.trans $ union_empty _
@@ -1027,13 +1030,13 @@ theorem image_bind [decidable_eq γ] {f : α → β} {s : finset α} {t : β →
   (s.image f).bind t = s.bind (λa, t (f a)) :=
 by haveI := classical.dec_eq α; exact
 finset.induction_on s rfl (λ a s has ih,
-by simp only [image_insert, bind_insert, ih])
+  by simp only [image_insert, bind_insert, ih])
 
 theorem bind_image [decidable_eq γ] {s : finset α} {t : α → finset β} {f : β → γ} :
   (s.bind t).image f = s.bind (λa, (t a).image f) :=
 by haveI := classical.dec_eq α; exact
 finset.induction_on s rfl (λ a s has ih,
-by simp only [bind_insert, image_union, ih])
+  by simp only [bind_insert, image_union, ih])
 
 theorem bind_to_finset [decidable_eq α] (s : multiset α) (t : α → multiset β) :
   (s.bind t).to_finset = s.to_finset.bind (λa, (t a).to_finset) :=
@@ -1201,8 +1204,7 @@ variables {op} {f : α → β} {b : β} {s : finset α} {a : α}
 @[simp] theorem fold_insert [decidable_eq α] (h : a ∉ s) : (insert a s).fold op b f = f a * s.fold op b f :=
 by unfold fold; rw [insert_val, ndinsert_of_not_mem h, map_cons, fold_cons_left]
 
-@[simp] theorem fold_singleton : (singleton a).fold op b f = f a * b :=
-rfl
+@[simp] theorem fold_singleton : (singleton a).fold op b f = f a * b := rfl
 
 @[simp] theorem fold_image [decidable_eq α] {g : γ → α} {s : finset γ}
   (H : ∀ (x ∈ s) (y ∈ s), g x = g y → x = y) : (s.image g).fold op b f = s.fold op b (f ∘ g) :=
@@ -1260,8 +1262,8 @@ by rw [insert_union, sup_insert, sup_insert, ih, sup_assoc]
 lemma sup_mono_fun {g : β → α} : (∀b∈s, f b ≤ g b) → s.sup f ≤ s.sup g :=
 by letI := classical.dec_eq β; from
 finset.induction_on s (λ _, le_refl _) (λ a s has ih H,
-by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] at H;
-simp only [sup_insert]; exact sup_le_sup H.1 (ih H.2))
+  by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] at H;
+     simp only [sup_insert]; exact sup_le_sup H.1 (ih H.2))
 
 lemma le_sup {b : β} (hb : b ∈ s) : f b ≤ s.sup f :=
 by letI := classical.dec_eq β; from
@@ -1272,8 +1274,8 @@ calc f b ≤ f b ⊔ s.sup f : le_sup_left
 lemma sup_le {a : α} : (∀b ∈ s, f b ≤ a) → s.sup f ≤ a :=
 by letI := classical.dec_eq β; from
 finset.induction_on s (λ _, bot_le) (λ n s hns ih H,
-by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] at H;
-simp only [sup_insert]; exact sup_le H.1 (ih H.2))
+  by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] at H;
+     simp only [sup_insert]; exact sup_le H.1 (ih H.2))
 
 lemma sup_le_iff {a : α} : s.sup f ≤ a ↔ (∀b ∈ s, f b ≤ a) :=
 iff.intro (assume h b hb, le_trans (le_sup hb) h) sup_le
@@ -1310,8 +1312,8 @@ by rw [insert_union, inf_insert, inf_insert, ih, inf_assoc]
 lemma inf_mono_fun {g : β → α} : (∀b∈s, f b ≤ g b) → s.inf f ≤ s.inf g :=
 by letI := classical.dec_eq β; from
 finset.induction_on s (λ _, le_refl _) (λ a s has ih H,
-by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] at H;
-simp only [inf_insert]; exact inf_le_inf H.1 (ih H.2))
+  by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] at H;
+     simp only [inf_insert]; exact inf_le_inf H.1 (ih H.2))
 
 lemma inf_le {b : β} (hb : b ∈ s) : s.inf f ≤ f b :=
 by letI := classical.dec_eq β; from
@@ -1322,8 +1324,8 @@ calc f b ≥ f b ⊓ s.inf f : inf_le_left
 lemma le_inf {a : α} : (∀b ∈ s, a ≤ f b) → a ≤ s.inf f :=
 by letI := classical.dec_eq β; from
 finset.induction_on s (λ _, le_top) (λ n s hns ih H,
-by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] at H;
-simp only [inf_insert]; exact le_inf H.1 (ih H.2))
+  by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] at H;
+     simp only [inf_insert]; exact le_inf H.1 (ih H.2))
 
 lemma le_inf_iff {a : α} : a ≤ s.inf f ↔ (∀b ∈ s, a ≤ f b) :=
 iff.intro (assume h b hb, le_trans h (inf_le hb)) le_inf
@@ -1346,14 +1348,11 @@ theorem max_eq_sup_with_bot (s : finset α) :
 @[simp] theorem max_empty : (∅ : finset α).max = none := rfl
 
 @[simp] theorem max_insert {a : α} {s : finset α} :
-  (insert a s).max = option.lift_or_get max (some a) s.max :=
-fold_insert_idem
+  (insert a s).max = option.lift_or_get max (some a) s.max := fold_insert_idem
 
-@[simp] theorem max_singleton {a : α} : finset.max {a} = some a :=
-max_insert
+@[simp] theorem max_singleton {a : α} : finset.max {a} = some a := max_insert
 
-@[simp] theorem max_singleton' {a : α} : finset.max (singleton a) = some a :=
-max_singleton
+@[simp] theorem max_singleton' {a : α} : finset.max (singleton a) = some a := max_singleton
 
 theorem max_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ b, b ∈ s.max :=
 (@le_sup (with_bot α) _ _ _ _ _ h _ rfl).imp $ λ b, Exists.fst
@@ -1374,7 +1373,7 @@ finset.induction_on s (λ _ H, by cases H)
     { induction p, exact mem_insert_self b s },
     { cases option.lift_or_get_choice max_choice (some b) s.max with q q;
       rw [max_insert, q] at h,
-      { cases h, cc },
+      { cases h, cases p rfl },
       { exact mem_insert_of_mem (ih h) } }
   end)
 
@@ -1388,15 +1387,13 @@ fold (option.lift_or_get min) none some
 theorem min_eq_inf_with_top (s : finset α) :
   s.min = @inf (with_top α) α _ s some := rfl
 
-@[simp] theorem min_empty : (∅ : finset α).min = none :=
-rfl
+@[simp] theorem min_empty : (∅ : finset α).min = none := rfl
 
 @[simp] theorem min_insert {a : α} {s : finset α} :
   (insert a s).min = option.lift_or_get min (some a) s.min :=
 fold_insert_idem
 
-@[simp] theorem min_singleton {a : α} : finset.min {a} = some a :=
-min_insert
+@[simp] theorem min_singleton {a : α} : finset.min {a} = some a := min_insert
 
 theorem min_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ b, b ∈ s.min :=
 (@inf_le (with_top α) _ _ _ _ _ h _ rfl).imp $ λ b, Exists.fst
@@ -1417,7 +1414,7 @@ finset.induction_on s (λ _ H, by cases H) $
     { induction p, exact mem_insert_self b s },
     { cases option.lift_or_get_choice min_choice (some b) s.min with q q;
       rw [min_insert, q] at h,
-      { cases h, cc },
+      { cases h, cases p rfl },
       { exact mem_insert_of_mem (ih h) } }
   end
 
@@ -1532,15 +1529,7 @@ end finset
 namespace list
 variable [decidable_eq α]
 
-theorem to_finset_card_of_nodup {l : list α} : l.nodup → l.to_finset.card = l.length :=
-begin
-  induction l,
-  case list.nil { intros, refl },
-  case list.cons : _ _ ih {
-    intros nd,
-    cases list.nodup_cons.1 nd with h1 h2,
-    specialize ih h2,
-    rw [to_finset_cons, finset.card_insert_of_not_mem (mt mem_to_finset.1 h1), ih, length_cons] }
-end
+theorem to_finset_card_of_nodup {l : list α} (h : l.nodup) : l.to_finset.card = l.length :=
+congr_arg card $ (@multiset.erase_dup_eq_self α _ l).2 h
 
 end list
diff --git a/data/finsupp.lean b/data/finsupp.lean
index a6d16ca18b958..fd8fb33722d6d 100644
--- a/data/finsupp.lean
+++ b/data/finsupp.lean
@@ -51,9 +51,12 @@ instance : has_zero (α →₀ β) := ⟨⟨∅, (λ_, 0), λ _, ⟨false.elim,
 
 instance : inhabited (α →₀ β) := ⟨0⟩
 
-@[simp] lemma mem_support_iff (f : α →₀ β) : ∀a:α, a ∈ f.support ↔ f a ≠ 0 :=
+@[simp] lemma mem_support_iff {f : α →₀ β} : ∀{a:α}, a ∈ f.support ↔ f a ≠ 0 :=
 f.mem_support_to_fun
 
+lemma not_mem_support_iff {f : α →₀ β} {a} : a ∉ f.support ↔ f a = 0 :=
+by haveI := classical.dec; exact not_iff_comm.1 mem_support_iff.symm
+
 @[extensionality]
 lemma ext : ∀{f g : α →₀ β}, (∀a, f a = g a) → f = g
 | ⟨s, f, hf⟩ ⟨t, g, hg⟩ h :=
@@ -66,19 +69,19 @@ lemma ext : ∀{f g : α →₀ β}, (∀a, f a = g a) → f = g
 
 @[simp] lemma support_eq_empty [decidable_eq β] {f : α →₀ β} : f.support = ∅ ↔ f = 0 :=
 ⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext.1 h a).1 $
-  (mem_support_iff f a).2 H, by rintro rfl; refl⟩
+  mem_support_iff.2 H, by rintro rfl; refl⟩
 
 instance [decidable_eq α] [decidable_eq β] : decidable_eq (α →₀ β) :=
 assume f g, decidable_of_iff (f.support = g.support ∧ (∀a∈f.support, f a = g a))
   ⟨assume ⟨h₁, h₂⟩, ext $ assume a,
       if h : a ∈ f.support then h₂ a h else
-        have hf : f a = 0, by rwa [f.mem_support_iff, not_not] at h,
-        have hg : g a = 0, by rwa [h₁, g.mem_support_iff, not_not] at h,
+        have hf : f a = 0, by rwa [mem_support_iff, not_not] at h,
+        have hg : g a = 0, by rwa [h₁, mem_support_iff, not_not] at h,
         by rw [hf, hg],
     by rintro rfl; exact ⟨rfl, λ _ _, rfl⟩⟩
 
 lemma finite_supp (f : α →₀ β) : set.finite {a | f a ≠ 0} :=
-⟨set.fintype_of_finset f.support f.mem_support_iff⟩
+⟨set.fintype_of_finset f.support (λ _, mem_support_iff)⟩
 
 lemma support_subset_iff {s : set α} {f : α →₀ β} [decidable_eq α] :
   ↑f.support ⊆ s ↔ (∀a∉s, f a = 0) :=
@@ -93,22 +96,20 @@ variables [decidable_eq α] [decidable_eq β] [has_zero β] {a a' : α} {b : β}
 /-- `single a b` is the finitely supported function which has
   value `b` at `a` and zero otherwise. -/
 def single (a : α) (b : β) : α →₀ β :=
-⟨(if b = 0 then ∅ else {a}), (λa', if a = a' then b else 0),
-  begin intro a', by_cases hb : b = 0; by_cases a = a'; simp only [hb, h, if_pos, if_false,
-    insert_empty_eq_singleton, mem_singleton],
-    { exact ⟨false.elim, λ H, H rfl⟩ },
-    { exact ⟨false.elim, λ H, H rfl⟩ },
-    { exact ⟨λ _, hb, λ _, rfl⟩ },
-    { exact ⟨λ H _, h H.symm, λ H, (H rfl).elim⟩ } end⟩
-
-lemma single_apply : (single a b : α →₀ β) a' = (if a = a' then b else 0) :=
-rfl
+⟨if b = 0 then ∅ else finset.singleton a, λ a', if a = a' then b else 0, λ a', begin
+  by_cases hb : b = 0; by_cases a = a';
+    simp only [hb, h, if_pos, if_false, mem_singleton],
+  { exact ⟨false.elim, λ H, H rfl⟩ },
+  { exact ⟨false.elim, λ H, H rfl⟩ },
+  { exact ⟨λ _, hb, λ _, rfl⟩ },
+  { exact ⟨λ H _, h H.symm, λ H, (H rfl).elim⟩ }
+end⟩
 
-@[simp] lemma single_eq_same : (single a b : α →₀ β) a = b :=
-if_pos rfl
+lemma single_apply : (single a b : α →₀ β) a' = if a = a' then b else 0 := rfl
 
-@[simp] lemma single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ β) a' = 0 :=
-if_neg h
+@[simp] lemma single_eq_same : (single a b : α →₀ β) a = b := if_pos rfl
+
+@[simp] lemma single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ β) a' = 0 := if_neg h
 
 @[simp] lemma single_zero : (single a 0 : α →₀ β) = 0 :=
 ext $ assume a',
@@ -143,8 +144,7 @@ def on_finset (s : finset α) (f : α → β) (hf : ∀a, f a ≠ 0 → a ∈ s)
 rfl
 
 @[simp] lemma support_on_finset_subset {s : finset α} {f : α → β} {hf} :
-  (on_finset s f hf).support ⊆ s :=
-filter_subset _
+  (on_finset s f hf).support ⊆ s := filter_subset _
 
 end on_finset
 
@@ -178,16 +178,15 @@ variables [has_zero β] [has_zero β₁] [has_zero β₂] [decidable_eq α] [dec
 /-- `zip_with f hf g₁ g₂` is the finitely supported function satisfying
   `zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a)`, and well defined when `f 0 0 = 0`. -/
 def zip_with (f : β₁ → β₂ → β) (hf : f 0 0 = 0) (g₁ : α →₀ β₁) (g₂ : α →₀ β₂) : (α →₀ β) :=
-on_finset (g₁.support ∪ g₂.support) (λa, f (g₁ a) (g₂ a)) $
-  assume a, classical.by_cases
-    (assume h : g₁ a = 0, by simp only [h, mem_union, mem_support_iff, ne.def, ne_self_iff_false, false_or, not_imp_not];
-      intro H; rw H; exact hf)
-    (assume h : g₁ a ≠ 0, λ _, mem_union_left _ $ (mem_support_iff _ _).2 h)
+on_finset (g₁.support ∪ g₂.support) (λa, f (g₁ a) (g₂ a)) $ λ a H, begin
+  haveI := classical.dec_eq β₁,
+  simp only [mem_union, mem_support_iff, ne], rw [← not_and_distrib],
+  rintro ⟨h₁, h₂⟩, rw [h₁, h₂] at H, exact H hf
+end
 
 @[simp] lemma zip_with_apply
   {f : β₁ → β₂ → β} {hf : f 0 0 = 0} {g₁ : α →₀ β₁} {g₂ : α →₀ β₂} {a : α} :
-  zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a) :=
-rfl
+  zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a) := rfl
 
 lemma support_zip_with {f : β₁ → β₂ → β} {hf : f 0 0 = 0} {g₁ : α →₀ β₁} {g₂ : α →₀ β₂} :
   (zip_with f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support :=
@@ -232,12 +231,11 @@ lemma prod_map_range_index [has_zero β₁] [has_zero β₂] [comm_monoid γ] [d
   {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} {h : α → β₂ → γ} (h0 : ∀a, h a 0 = 1) :
   (map_range f hf g).prod h = g.prod (λa b, h a (f b)) :=
 finset.prod_subset support_map_range $ λ _ _ H,
-by rw [by_contradiction (mt (mem_support_iff _ _).2 H), h0]
+by rw [not_mem_support_iff.1 H, h0]
 
 @[to_additive finsupp.sum_zero_index]
 lemma prod_zero_index [add_comm_monoid β] [comm_monoid γ] {h : α → β → γ} :
-  (0 : α →₀ β).prod h = 1 :=
-rfl
+  (0 : α →₀ β).prod h = 1 := rfl
 
 section decidable
 variables [decidable_eq α] [decidable_eq β]
@@ -311,7 +309,7 @@ suffices p (single a (f a) + f.erase a), by rwa [single_add_erase] at this,
 begin
   apply ha,
   { rw [support_erase, mem_erase], exact λ H, H.1 rfl },
-  { rw [← mem_support_iff _ a, hf], exact mem_insert_self _ _ },
+  { rw [← mem_support_iff, hf], exact mem_insert_self _ _ },
   { apply ih _ _,
     rw [support_erase, hf, finset.erase_insert has] }
 end
@@ -326,7 +324,7 @@ suffices p (f.erase a + single a (f a)), by rwa [erase_add_single] at this,
 begin
   apply ha,
   { rw [support_erase, mem_erase], exact λ H, H.1 rfl },
-  { rw [← mem_support_iff _ a, hf], exact mem_insert_self _ _ },
+  { rw [← mem_support_iff, hf], exact mem_insert_self _ _ },
   { apply ih _ _,
     rw [support_erase, hf, finset.erase_insert has] }
 end
@@ -344,8 +342,8 @@ instance [add_group β] : add_group (α →₀ β) :=
 
 lemma single_multiset_sum [add_comm_monoid β] [decidable_eq α] [decidable_eq β]
   (s : multiset β) (a : α) : single a s.sum = (s.map (single a)).sum :=
-multiset.induction_on s single_zero (λ a s ih,
-by rw [multiset.sum_cons, single_add, ih, multiset.map_cons, multiset.sum_cons])
+multiset.induction_on s single_zero $ λ a s ih,
+by rw [multiset.sum_cons, single_add, ih, multiset.map_cons, multiset.sum_cons]
 
 lemma single_finset_sum [add_comm_monoid β] [decidable_eq α] [decidable_eq β]
   (s : finset γ) (f : γ → β) (a : α) : single a (s.sum f) = s.sum (λb, single a (f b)) :=
@@ -392,7 +390,7 @@ have ∀a₁ : α, f.sum (λ (a : α₁) (b : β₁), (g a b) a₁) ≠ 0 →
     (∃ (a : α₁), f a ≠ 0 ∧ ¬ (g a (f a)) a₁ = 0),
   from assume a₁ h,
   let ⟨a, ha, ne⟩ := finset.exists_ne_zero_of_sum_ne_zero h in
-  ⟨a, (f.mem_support_iff a).mp ha, ne⟩,
+  ⟨a, mem_support_iff.mp ha, ne⟩,
 by simpa only [finset.subset_iff, mem_support_iff, finset.mem_bind, sum_apply, exists_prop] using this
 
 @[simp] lemma sum_zero [add_comm_monoid β] [add_comm_monoid γ] {f : α →₀ β} :
@@ -425,13 +423,10 @@ begin
     refine (finset.sum_subset this (λ _ _ H, _)).symm,
     exact if_neg (mt mem_singleton.2 H) },
   { transitivity (f.support.sum (λa, (0 : β))),
-    { refine (finset.sum_congr rfl _),
-      intros a' ha',
-      have h: a' ≠ a,
-        { rintro rfl, exact h ha' },
-      exact if_neg h },
+    { refine (finset.sum_congr rfl $ λ a' ha', if_neg _),
+      rintro rfl, exact h ha' },
     { rw [sum_const_zero, insert_empty_eq_singleton, sum_singleton,
-        if_pos rfl, by_contradiction (mt (mem_support_iff _ _).2 h)] } }
+        if_pos rfl, not_mem_support_iff.1 h] } }
 end,
 ext $ assume a, by simp only [sum_apply, single_apply, this,
   insert_empty_eq_singleton, sum_singleton, if_pos]
@@ -442,14 +437,14 @@ lemma prod_add_index [add_comm_monoid β] [comm_monoid γ] {f g : α →₀ β}
   (f + g).prod h = f.prod h * g.prod h :=
 have f_eq : (f.support ∪ g.support).prod (λa, h a (f a)) = f.prod h,
   from (finset.prod_subset finset.subset_union_left $
-    by intros _ _ H; rw [by_contradiction (mt (mem_support_iff _ _).2 H), h_zero]).symm,
+    by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
 have g_eq : (f.support ∪ g.support).prod (λa, h a (g a)) = g.prod h,
   from (finset.prod_subset finset.subset_union_right $
-    by intros _ _ H; rw [by_contradiction (mt (mem_support_iff _ _).2 H), h_zero]).symm,
+    by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
 calc (f + g).support.prod (λa, h a ((f + g) a)) =
       (f.support ∪ g.support).prod (λa, h a ((f + g) a)) :
     finset.prod_subset support_add $
-      by intros _ _ H; rw [by_contradiction (mt (mem_support_iff _ _).2 H), h_zero]
+      by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]
   ... = (f.support ∪ g.support).prod (λa, h a (f a)) *
       (f.support ∪ g.support).prod (λa, h a (g a)) :
     by simp only [add_apply, h_add, finset.prod_mul_distrib]
@@ -590,8 +585,8 @@ variables [has_zero β] {p : α → Prop} [decidable_pred p] {f : α →₀ β}
 
 /-- `filter p f` is the function which is `f a` if `p a` is true and 0 otherwise. -/
 def filter (p : α → Prop) [decidable_pred p] (f : α →₀ β) : α →₀ β :=
-on_finset f.support (λa, if p a then f a else 0) (λ a H,
-(mem_support_iff f a).2 $ λ h, by rw [h, if_t_t] at H; exact H rfl)
+on_finset f.support (λa, if p a then f a else 0) $ λ a H,
+mem_support_iff.2 $ λ h, by rw [h, if_t_t] at H; exact H rfl
 
 @[simp] lemma filter_apply_pos {a : α} (h : p a) : f.filter p a = f a :=
 if_pos h
@@ -698,14 +693,9 @@ calc f.to_multiset.count a = f.sum (λx n, (add_monoid.smul n {x} : multiset α)
     (finset.sum_hom _ (multiset.count_zero a) (multiset.count_add a)).symm
   ... = f.sum (λx n, n * ({x} : multiset α).count a) : by simp only [multiset.count_smul]
   ... = f.sum (λx n, n * (x :: 0 : multiset α).count a) : rfl
-  ... = f a * (a :: 0 : multiset α).count a :
-    begin
-      refine sum_eq_single _ _ _,
-      { intros _ _ H,
-        simp only [multiset.count_cons_of_ne (ne.symm H), multiset.count_zero, mul_zero] },
-      { intro H,
-        simp only [by_contradiction (mt (mem_support_iff _ _).2 H), zero_mul] }
-    end
+  ... = f a * (a :: 0 : multiset α).count a : sum_eq_single _
+    (λ a' _ H, by simp only [multiset.count_cons_of_ne (ne.symm H), multiset.count_zero, mul_zero])
+    (λ H, by simp only [not_mem_support_iff.1 H, zero_mul])
   ... = f a : by simp only [multiset.count_singleton, mul_one]
 
 def of_multiset [decidable_eq α] (m : multiset α) : α →₀ ℕ :=
@@ -730,8 +720,8 @@ multiset.induction_on s false.elim
     by_cases a ∈ f.support,
     { exact ⟨f, multiset.mem_cons_self _ _, h⟩ },
     { simp only [multiset.sum_cons, mem_support_iff, add_apply,
-        by_contradiction (mt (mem_support_iff _ _).2 h), zero_add] at ha,
-      rcases ih ((mem_support_iff _ _).2 ha) with ⟨f', h₀, h₁⟩,
+        not_mem_support_iff.1 h, zero_add] at ha,
+      rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩,
       exact ⟨f', multiset.mem_cons_of_mem h₀, h₁⟩ }
   end
 
@@ -778,15 +768,10 @@ f.sum $ λa g, g.sum $ λb c, single (a, b) c
 
 def finsupp_prod_equiv [add_comm_monoid γ] [decidable_eq α] [decidable_eq β] [decidable_eq γ] :
   ((α × β) →₀ γ) ≃ (α →₀ (β →₀ γ)) :=
-⟨ finsupp.curry, finsupp.uncurry,
-  assume f, by simp only [finsupp.curry, finsupp.uncurry,
-    sum_sum_index, sum_zero_index, sum_add_index, sum_single_index,
-    single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
-    prod.mk.eta, sum_single],
-  assume f, by simp only [finsupp.curry, finsupp.uncurry,
-    sum_sum_index, sum_zero_index, sum_add_index, sum_single_index,
-    single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
-    prod.mk.eta, (single_sum _ _ _).symm, sum_single] ⟩
+by refine ⟨finsupp.curry, finsupp.uncurry, λ f, _, λ f, _⟩; simp only [
+  finsupp.curry, finsupp.uncurry, sum_sum_index, sum_zero_index, sum_add_index,
+  sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff,
+  forall_3_true_iff, prod.mk.eta, (single_sum _ _ _).symm, sum_single]
 
 end curry_uncurry
 
diff --git a/data/list/basic.lean b/data/list/basic.lean
index c7ce85b3a0469..51ef8a6e9ce9e 100644
--- a/data/list/basic.lean
+++ b/data/list/basic.lean
@@ -152,6 +152,52 @@ lemma bind_map {g : α → list β} {f : β → γ} :
 | [] := rfl
 | (a::l) := by simp only [cons_bind, map_append, bind_map l]
 
+/- bounded quantifiers over lists -/
+
+theorem forall_mem_nil (p : α → Prop) : ∀ x ∈ @nil α, p x.
+
+@[simp] theorem forall_mem_cons' {p : α → Prop} {a : α} {l : list α} :
+  (∀ (x : α), x = a ∨ x ∈ l → p x) ↔ p a ∧ ∀ x ∈ l, p x :=
+by simp only [or_imp_distrib, forall_and_distrib, forall_eq]
+
+theorem forall_mem_cons {p : α → Prop} {a : α} {l : list α} :
+  (∀ x ∈ a :: l, p x) ↔ p a ∧ ∀ x ∈ l, p x :=
+by simp only [mem_cons_iff, forall_mem_cons']
+
+theorem forall_mem_of_forall_mem_cons {p : α → Prop} {a : α} {l : list α}
+    (h : ∀ x ∈ a :: l, p x) :
+  ∀ x ∈ l, p x :=
+(forall_mem_cons.1 h).2
+
+theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ x ∈ [a], p x) ↔ p a :=
+by simp only [mem_singleton, forall_eq]
+
+theorem forall_mem_append {p : α → Prop} {l₁ l₂ : list α} :
+  (∀ x ∈ l₁ ++ l₂, p x) ↔ (∀ x ∈ l₁, p x) ∧ (∀ x ∈ l₂, p x) :=
+by simp only [mem_append, or_imp_distrib, forall_and_distrib]
+
+theorem not_exists_mem_nil (p : α → Prop) : ¬ ∃ x ∈ @nil α, p x.
+
+theorem exists_mem_cons_of {p : α → Prop} {a : α} (l : list α) (h : p a) :
+  ∃ x ∈ a :: l, p x :=
+bex.intro a (mem_cons_self _ _) h
+
+theorem exists_mem_cons_of_exists {p : α → Prop} {a : α} {l : list α} (h : ∃ x ∈ l, p x) :
+  ∃ x ∈ a :: l, p x :=
+bex.elim h (λ x xl px, bex.intro x (mem_cons_of_mem _ xl) px)
+
+theorem or_exists_of_exists_mem_cons {p : α → Prop} {a : α} {l : list α} (h : ∃ x ∈ a :: l, p x) :
+  p a ∨ ∃ x ∈ l, p x :=
+bex.elim h (λ x xal px,
+  or.elim (eq_or_mem_of_mem_cons xal)
+    (assume : x = a, begin rw ←this, left, exact px end)
+    (assume : x ∈ l, or.inr (bex.intro x this px)))
+
+@[simp] theorem exists_mem_cons_iff (p : α → Prop) (a : α) (l : list α) :
+  (∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x :=
+iff.intro or_exists_of_exists_mem_cons
+  (assume h, or.elim h (exists_mem_cons_of l) exists_mem_cons_of_exists)
+
 /- list subset -/
 
 theorem subset_def {l₁ l₂ : list α} : l₁ ⊆ l₂ ↔ ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ := iff.rfl
@@ -296,12 +342,9 @@ end
 
 attribute [simp] join
 
-theorem join_eq_nil {L : list (list α)} : join L = [] ↔ ∀ l ∈ L, l = [] :=
-begin
-  induction L with hd tl ih,
-  { split, { intros _ _ H, cases H }, { intro, refl } },
-  simp only [*, join, mem_cons_iff, or_imp_distrib, forall_and_distrib, forall_eq, append_eq_nil]
-end
+theorem join_eq_nil : ∀ {L : list (list α)}, join L = [] ↔ ∀ l ∈ L, l = []
+| []     := iff_of_true rfl (forall_mem_nil _)
+| (l::L) := by simp only [join, append_eq_nil, join_eq_nil, forall_mem_cons]
 
 @[simp] theorem join_append (L₁ L₂ : list (list α)) : join (L₁ ++ L₂) = join L₁ ++ join L₂ :=
 by induction L₁; [refl, simp only [*, join, cons_append, append_assoc]]
@@ -314,11 +357,9 @@ theorem eq_of_mem_repeat {a b : α} : ∀ {n}, b ∈ repeat a n → b = a
 | (n+1) h := or.elim h id $ @eq_of_mem_repeat _
 
 theorem eq_repeat_of_mem {a : α} : ∀ {l : list α}, (∀ b ∈ l, b = a) → l = repeat a l.length
-| [] H := rfl
-| (b::l) H :=
-  have b = a ∧ ∀ (x : α), x ∈ l → x = a,
-  by simpa only [mem_cons_iff, or_imp_distrib, forall_and_distrib, forall_eq] using H,
-  by unfold length repeat; congr; [exact this.1, exact eq_repeat_of_mem this.2]
+| []     H := rfl
+| (b::l) H := by cases forall_mem_cons.1 H with H₁ H₂;
+  unfold length repeat; congr; [exact H₁, exact eq_repeat_of_mem H₂]
 
 theorem eq_repeat' {a : α} {l : list α} : l = repeat a l.length ↔ ∀ b ∈ l, b = a :=
 ⟨λ h, h.symm ▸ λ b, eq_of_mem_repeat, eq_repeat_of_mem⟩
@@ -491,11 +532,9 @@ by {induction l, contradiction, refl}
 /- map -/
 
 lemma map_congr {f g : α → β} : ∀ {l : list α}, (∀ x ∈ l, f x = g x) → map f l = map g l
-| [] _     := rfl
-| (a::l) h :=
-  have h1 : f a = g a, from h _ (mem_cons_self _ _),
-  have h2 : map f l = map g l, from map_congr $ assume a', h _ ∘ mem_cons_of_mem _,
-  show f a :: map f l = g a :: map g l, by rw [h1, h2]
+| []     _ := rfl
+| (a::l) h := let ⟨h₁, h₂⟩ := forall_mem_cons.1 h in
+  by rw [map, map, h₁, map_congr h₂]
 
 theorem map_concat (f : α → β) (a : α) (l : list α) : map f (concat l a) = concat (map f l) (f a) :=
 by induction l; [refl, simp only [*, concat_eq_append, cons_append, map, map_append]]; split; refl
@@ -697,11 +736,10 @@ 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,
-  { split, { intros _ H, cases H }, { intro, refl } },
-  simp only [length, mem_cons_iff],
-  by_cases h : a = b,
-  { simp only [or.inl h, not_true, iff_false, index_of_cons, if_pos h], intro H, cases H },
-  { simp only [h, false_or, index_of_cons, if_false], rw ← ih, exact ⟨succ_inj, congr_arg _⟩ }
+  { exact iff_of_true rfl (not_mem_nil _) },
+  simp only [length, mem_cons_iff, index_of_cons], split_ifs,
+  { exact iff_of_false (by rintro ⟨⟩) (λ H, H $ or.inl h) },
+  { simp only [h, false_or], rw ← ih, exact succ_inj' }
 end
 
 @[simp] theorem index_of_of_not_mem {l : list α} {a : α} : a ∉ l → index_of a l = length l :=
@@ -906,8 +944,7 @@ theorem nth_update_nth_ne (a : α) {m n} (l : list α) (h : m ≠ n) :
 by simp only [update_nth_eq_modify_nth, nth_modify_nth_ne _ _ h]
 
 /- take, drop -/
-@[simp] theorem take_zero (l : list α) : take 0 l = [] :=
-rfl
+@[simp] theorem take_zero (l : list α) : take 0 l = [] := rfl
 
 @[simp] theorem take_nil : ∀ n, take n [] = ([] : list α)
 | 0     := rfl
@@ -1356,53 +1393,7 @@ preorder.to_has_le _
 instance [decidable_linear_order α] : decidable_linear_order (list α) :=
 decidable_linear_order_of_STO' (lex (<))
 
-/- all & any, bounded quantifiers over lists -/
-
-theorem forall_mem_nil (p : α → Prop) : ∀ x ∈ @nil α, p x :=
-by intros _ H; cases H
-
-@[simp] theorem forall_mem_cons' {p : α → Prop} {a : α} {l : list α} :
-  (∀ (x : α), x = a ∨ x ∈ l → p x) ↔ p a ∧ ∀ x ∈ l, p x :=
-by simp only [or_imp_distrib, forall_and_distrib, forall_eq]
-
-theorem forall_mem_cons {p : α → Prop} {a : α} {l : list α} :
-  (∀ x ∈ a :: l, p x) ↔ p a ∧ ∀ x ∈ l, p x :=
-by simp only [mem_cons_iff, forall_mem_cons']
-
-theorem forall_mem_of_forall_mem_cons {p : α → Prop} {a : α} {l : list α}
-    (h : ∀ x ∈ a :: l, p x) :
-  ∀ x ∈ l, p x :=
-(forall_mem_cons.1 h).2
-
-theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ x ∈ [a], p x) ↔ p a :=
-by simp only [mem_singleton, forall_eq]
-
-theorem forall_mem_append {p : α → Prop} {l₁ l₂ : list α} :
-  (∀ x ∈ l₁ ++ l₂, p x) ↔ (∀ x ∈ l₁, p x) ∧ (∀ x ∈ l₂, p x) :=
-by simp only [mem_append, or_imp_distrib, forall_and_distrib]
-
-theorem not_exists_mem_nil (p : α → Prop) : ¬ ∃ x ∈ @nil α, p x :=
-by rintro ⟨_, H, _⟩; cases H
-
-theorem exists_mem_cons_of {p : α → Prop} {a : α} (l : list α) (h : p a) :
-  ∃ x ∈ a :: l, p x :=
-bex.intro a (mem_cons_self _ _) h
-
-theorem exists_mem_cons_of_exists {p : α → Prop} {a : α} {l : list α} (h : ∃ x ∈ l, p x) :
-  ∃ x ∈ a :: l, p x :=
-bex.elim h (λ x xl px, bex.intro x (mem_cons_of_mem _ xl) px)
-
-theorem or_exists_of_exists_mem_cons {p : α → Prop} {a : α} {l : list α} (h : ∃ x ∈ a :: l, p x) :
-  p a ∨ ∃ x ∈ l, p x :=
-bex.elim h (λ x xal px,
-  or.elim (eq_or_mem_of_mem_cons xal)
-    (assume : x = a, begin rw ←this, left, exact px end)
-    (assume : x ∈ l, or.inr (bex.intro x this px)))
-
-@[simp] theorem exists_mem_cons_iff (p : α → Prop) (a : α) (l : list α) :
-  (∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x :=
-iff.intro or_exists_of_exists_mem_cons
-  (assume h, or.elim h (exists_mem_cons_of l) exists_mem_cons_of_exists)
+/- all & any -/
 
 @[simp] theorem all_nil (p : α → bool) : all [] p = tt := rfl
 
@@ -1411,8 +1402,8 @@ iff.intro or_exists_of_exists_mem_cons
 theorem all_iff_forall {p : α → bool} {l : list α} : all l p ↔ ∀ a ∈ l, p a :=
 begin
   induction l with a l ih,
-  { split, { intros _ _ H, cases H }, { intro, exact dec_trivial } },
-  simp only [all_cons, band_coe_iff, ih, forall_mem_cons, *]
+  { exact iff_of_true rfl (forall_mem_nil _) },
+  simp only [all_cons, band_coe_iff, ih, forall_mem_cons]
 end
 
 theorem all_iff_forall_prop {p : α → Prop} [decidable_pred p]
@@ -1426,7 +1417,7 @@ by simp only [all_iff_forall, bool.of_to_bool_iff]
 theorem any_iff_exists {p : α → bool} {l : list α} : any l p ↔ ∃ a ∈ l, p a :=
 begin
   induction l with a l ih,
-  { split, { intro H, cases H }, { rintro ⟨_, H, _⟩, cases H } },
+  { exact iff_of_false bool.not_ff (not_exists_mem_nil _) },
   simp only [any_cons, bor_coe_iff, ih, exists_mem_cons_iff]
 end
 
@@ -1522,10 +1513,10 @@ if_neg h
 @[simp] theorem find_eq_none : find p l = none ↔ ∀ x ∈ l, ¬ p x :=
 begin
   induction l with a l IH,
-  { split, { intros _ _ H, cases H }, { intro, refl } },
-  by_cases h : p a,
-  { simp only [find_cons_of_pos _ h, forall_mem_cons, h, not_true, false_and] },
-  simp only [find_cons_of_neg _ h, IH, forall_mem_cons, h, not_false_iff, true_and]
+  { exact iff_of_true rfl (forall_mem_nil _) },
+  rw forall_mem_cons, by_cases h : p a,
+  { simp only [find_cons_of_pos _ h, h, not_true, false_and] },
+  { rwa [find_cons_of_neg _ h, iff_true_intro h, true_and] }
 end
 
 @[simp] theorem find_some (H : find p l = some a) : p a :=
@@ -1577,7 +1568,7 @@ begin
   induction l with a l IH, {refl},
   by_cases pa : p a,
   { simp only [filter_map, option.guard, IH, if_pos pa, filter_cons_of_pos _ pa], split; refl },
-  simp only [filter_map, option.guard, IH, if_neg pa, filter_cons_of_neg _ pa],
+  { simp only [filter_map, option.guard, IH, if_neg pa, filter_cons_of_neg _ pa] }
 end
 
 theorem filter_map_filter_map (f : α → option β) (g : β → option γ) (l : list α) :
@@ -1614,7 +1605,7 @@ begin
   show (option.guard p x).bind f = ite (p x) (f x) none,
   by_cases h : p x,
   { simp only [option.guard, if_pos h, option.some_bind'] },
-  simp only [option.guard, if_neg h, option.none_bind']
+  { simp only [option.guard, if_neg h, option.none_bind'] }
 end
 
 @[simp] theorem filter_map_some (l : list α) : filter_map some l = l :=
@@ -1690,13 +1681,13 @@ theorem mem_filter_of_mem {a : α} : ∀ {l}, a ∈ l → p a → a ∈ filter p
 theorem filter_eq_self {l} : filter p l = l ↔ ∀ a ∈ l, p a :=
 begin
   induction l with a l ih,
-  { split, { intros _ _ H, cases H }, { intro, refl } },
-  by_cases p a,
-  { rw [filter_cons_of_pos _ h, cons_inj', ih, forall_mem_cons, and_iff_right h] },
-  rw [filter_cons_of_neg _ h, forall_mem_cons, iff_false_intro h, false_and, iff_false],
-  show filter p l ≠ a :: l, intro e,
-  have := filter_sublist l, rw e at this,
-  exact not_lt_of_ge (length_le_of_sublist this) (lt_succ_self _)
+  { exact iff_of_true rfl (forall_mem_nil _) },
+  rw forall_mem_cons, by_cases p a,
+  { rw [filter_cons_of_pos _ h, cons_inj', ih, and_iff_right h] },
+  { rw [filter_cons_of_neg _ h],
+    refine iff_of_false _ (mt and.left h), intro e,
+    have := filter_sublist l, rw e at this,
+    exact not_lt_of_ge (length_le_of_sublist this) (lt_succ_self _) }
 end
 
 theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a ∈ l, ¬p a :=
@@ -1786,8 +1777,7 @@ countp_le_of_sublist
 theorem count_le_count_cons (a b : α) (l : list α) : count a l ≤ count a (b :: l) :=
 count_le_of_sublist _ (sublist_cons _ _)
 
-theorem count_singleton (a : α) : count a [a] = 1 :=
-if_pos rfl
+theorem count_singleton (a : α) : count a [a] = 1 := if_pos rfl
 
 @[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
 countp_append
@@ -2206,7 +2196,7 @@ theorem sublists_aux_ne_nil : ∀ (l : list α), [] ∉ sublists_aux l cons
   rw [sublists_aux_cons_cons],
   refine not_mem_cons_of_ne_of_not_mem (cons_ne_nil _ _).symm _,
   have := sublists_aux_ne_nil l, revert this,
-  induction sublists_aux l cons; intro, { by rwa foldr },
+  induction sublists_aux l cons; intro, {rwa foldr},
   simp only [foldr, mem_cons_iff, false_or, not_or_distrib],
   exact ⟨ne_of_not_mem_cons this, ih (not_mem_of_not_mem_cons this)⟩
 end
@@ -2221,10 +2211,8 @@ by simp only [sublists_eq_sublists', length_map, length_sublists', length_revers
 theorem map_ret_sublist_sublists (l : list α) : map list.ret l <+ sublists l :=
 reverse_rec_on l (nil_sublist _) $
 λ l a IH, by simp only [map, map_append, sublists_concat]; exact
-((append_sublist_append_left _).2
-  (singleton_sublist.2 $ mem_map.2 ⟨[],
-    mem_sublists.2 (nil_sublist _),
-    by refl⟩)).trans
+((append_sublist_append_left _).2 $ singleton_sublist.2 $
+  mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by refl⟩).trans
 ((append_sublist_append_right _).2 IH)
 
 /- transpose -/
@@ -2261,7 +2249,7 @@ attribute [simp] forall₂.nil
 theorem forall₂.imp {R S : α → β → Prop}
   (H : ∀ a b, R a b → S a b) {l₁ l₂}
   (h : forall₂ R l₁ l₂) : forall₂ S l₁ l₂ :=
-by induction h; [constructor, constructor]; solve_by_elim
+by induction h; constructor; solve_by_elim
 
 lemma forall₂.mp {r q s : α → β → Prop} (h : ∀a b, r a b → q a b → s a b) :
   ∀{l₁ l₂}, forall₂ r l₁ l₂ → forall₂ q l₁ l₂ → forall₂ s l₁ l₂
@@ -2384,7 +2372,7 @@ lemma rel_mem (hr : bi_unique r) : (r ⇒ forall₂ r ⇒ iff) (∈) (∈)
 | a b h (a'::as) (b'::bs) (forall₂.cons h₁ h₂) := rel_or (rel_eq hr h h₁) (rel_mem h h₂)
 
 lemma rel_map : ((r ⇒ p) ⇒ forall₂ r ⇒ forall₂ p) map map
-| f g h [] [] forall₂.nil := by constructor
+| f g h [] [] forall₂.nil := forall₂.nil
 | f g h (a::as) (b::bs) (forall₂.cons h₁ h₂) := forall₂.cons (h h₁) (rel_map @h h₂)
 
 lemma rel_append : (forall₂ r ⇒ forall₂ r ⇒ forall₂ r) append append
@@ -2392,7 +2380,7 @@ lemma rel_append : (forall₂ r ⇒ forall₂ r ⇒ forall₂ r) append append
 | (a::as) (b::bs) (forall₂.cons h₁ h₂) l₁ l₂ hl := forall₂.cons h₁ (rel_append h₂ hl)
 
 lemma rel_join : (forall₂ (forall₂ r) ⇒ forall₂ r) join join
-| [] [] forall₂.nil := by constructor
+| [] [] forall₂.nil := forall₂.nil
 | (a::as) (b::bs) (forall₂.cons h₁ h₂) := rel_append h₁ (rel_join h₂)
 
 lemma rel_bind : (forall₂ r ⇒ (r ⇒ forall₂ p) ⇒ forall₂ p) list.bind list.bind :=
@@ -2457,11 +2445,11 @@ def sections : list (list α) → list (list α)
 theorem mem_sections {L : list (list α)} {f} : f ∈ sections L ↔ forall₂ (∈) f L :=
 begin
   refine ⟨λ h, _, λ h, _⟩,
-  { induction L generalizing f, {cases mem_singleton.1 h, constructor},
+  { induction L generalizing f, {cases mem_singleton.1 h, exact forall₂.nil},
     simp only [sections, bind_eq_bind, mem_bind, mem_map] at h,
     rcases h with ⟨_, _, _, _, rfl⟩,
     simp only [*, forall₂_cons, true_and] },
-  { induction h with a l f L al fL fs, { constructor, constructor },
+  { induction h with a l f L al fL fs, {exact or.inl rfl},
     simp only [sections, bind_eq_bind, mem_bind, mem_map],
     exact ⟨_, fs, _, al, rfl, rfl⟩ }
 end
@@ -2514,12 +2502,12 @@ def permutations (l : list α) : list (list α) :=
 l :: permutations_aux l []
 
 @[simp] theorem permutations_aux_nil (is : list α) : permutations_aux [] is = [] :=
-list.permutations_aux.rec.equations._eqn_1 _ _ _
+by rw [permutations_aux, permutations_aux.rec]
 
 @[simp] theorem permutations_aux_cons (t : α) (ts is : list α) :
   permutations_aux (t :: ts) is = foldr (λy r, (permutations_aux2 t ts r y id).2)
     (permutations_aux ts (t::is)) (permutations is) :=
-list.permutations_aux.rec.equations._eqn_2 _ _ _ _ _
+by rw [permutations_aux, permutations_aux.rec]; refl
 
 end permutations
 
@@ -2874,12 +2862,14 @@ l₁.bind $ λ a, l₂.map $ prod.mk a
 
 @[simp] theorem mem_product {l₁ : list α} {l₂ : list β} {a : α} {b : β} :
   (a, b) ∈ product l₁ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ :=
-by simp only [product, mem_bind, mem_map, prod.ext_iff, exists_prop, and.left_comm, exists_and_distrib_left, exists_eq_left, exists_eq_right]
+by simp only [product, mem_bind, mem_map, prod.ext_iff, exists_prop,
+  and.left_comm, exists_and_distrib_left, exists_eq_left, exists_eq_right]
 
 theorem length_product (l₁ : list α) (l₂ : list β) :
   length (product l₁ l₂) = length l₁ * length l₂ :=
 by induction l₁ with x l₁ IH; [exact (zero_mul _).symm,
-simp only [length, product_cons, length_append, IH, right_distrib, one_mul, length_map, add_comm]]
+  simp only [length, product_cons, length_append, IH,
+    right_distrib, one_mul, length_map, add_comm]]
 
 
 /- sigma -/
@@ -2903,7 +2893,8 @@ l₁.bind $ λ a, (l₂ a).map $ sigma.mk a
 
 @[simp] theorem mem_sigma {l₁ : list α} {l₂ : Π a, list (σ a)} {a : α} {b : σ a} :
   sigma.mk a b ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a :=
-by simp only [list.sigma, mem_bind, mem_map, exists_prop, exists_and_distrib_left, and.left_comm, exists_eq_left, heq_iff_eq, exists_eq_right]
+by simp only [list.sigma, mem_bind, mem_map, exists_prop, exists_and_distrib_left,
+  and.left_comm, exists_eq_left, heq_iff_eq, exists_eq_right]
 
 theorem length_sigma (l₁ : list α) (l₂ : Π a, list (σ a)) :
   length (l₁.sigma l₂) = (l₁.map (λ a, length (l₂ a))).sum :=
@@ -3168,9 +3159,10 @@ theorem mem_bag_inter {a : α} : ∀ {l₁ l₂ : list α}, a ∈ l₁.bag_inter
     { rw [cons_bag_inter_of_pos _ h, mem_cons_iff, mem_cons_iff, mem_bag_inter],
       by_cases ba : a = b,
       { simp only [ba, h, eq_self_iff_true, true_or, true_and] },
-      simp only [mem_erase_of_ne ba, ba, false_or] },
-    rw [cons_bag_inter_of_neg _ h, mem_bag_inter, mem_cons_iff, or_and_distrib_right],
-    symmetry, apply or_iff_right_of_imp, exact false.elim ∘ by rintro ⟨rfl, _⟩; cc
+      { simp only [mem_erase_of_ne ba, ba, false_or] } },
+    { rw [cons_bag_inter_of_neg _ h, mem_bag_inter, mem_cons_iff, or_and_distrib_right],
+      symmetry, apply or_iff_right_of_imp,
+      rintro ⟨rfl, h'⟩, exact h.elim h' }
   end
 
 theorem bag_inter_sublist_left : ∀ l₁ l₂ : list α, l₁.bag_inter l₂ <+ l₁
@@ -3361,7 +3353,7 @@ end
 suffices ∀ {R l}, @pairwise α R l → pairwise (λ x y, R y x) (reverse l),
 from λ R l, ⟨λ p, reverse_reverse l ▸ this p, this⟩,
 λ R l p, by induction p with a l h p IH;
-  [exact pairwise.nil _, simpa only [reverse_cons, pairwise_append, IH,
+  [apply pairwise.nil, simpa only [reverse_cons, pairwise_append, IH,
     pairwise_cons, forall_prop_of_false (not_mem_nil _), forall_true_iff,
     pairwise.nil, mem_reverse, mem_singleton, forall_eq, true_and] using h]
 
@@ -3399,9 +3391,10 @@ by have := pairwise_sublists' (pairwise_reverse.2 H);
    rwa [sublists'_reverse, pairwise_map] at this
 
 variable [decidable_rel R]
+
 instance decidable_pairwise (l : list α) : decidable (pairwise R l) :=
 by induction l with hd tl ih; [exact is_true (pairwise.nil _),
-  exact @@decidable_of_iff' _ pairwise_cons (@@and.decidable _ ih)]
+  exactI decidable_of_iff' _ pairwise_cons]
 
 /- pairwise reduct -/
 
@@ -3692,7 +3685,7 @@ begin
   by_cases b = a,
   { subst h, rw [erase_cons_head, filter_cons_of_neg],
     symmetry, rw filter_eq_self, simpa only [ne.def, eq_comm] using m, exact not_not_intro rfl },
-  rw [erase_cons_tail _ h, filter_cons_of_pos, IH], exact h
+  { rw [erase_cons_tail _ h, filter_cons_of_pos, IH], exact h }
 end
 
 theorem nodup_erase_of_nodup [decidable_eq α] (a : α) {l} : nodup l → nodup (l.erase a) :=
@@ -3719,20 +3712,21 @@ theorem nodup_product {l₁ : list α} {l₂ : list β} (d₁ : nodup l₁) (d
   nodup (product l₁ l₂) :=
  nodup_bind.2
   ⟨λ a ma, nodup_map (injective_of_left_inverse (λ b, (rfl : (a,b).2 = b))) d₂,
-  d₁.imp (λ a₁ a₂ n x,
-    suffices ∀ (b₁ : β), b₁ ∈ l₂ → (a₁, b₁) = x → ∀ (b₂ : β), b₂ ∈ l₂ → (a₂, b₂) ≠ x,
-      by simpa only [mem_map, exists_imp_distrib, and_imp],
-    λ b₁ mb₁ e b₂ mb₂ e', by subst e'; injection e; contradiction)⟩
+  d₁.imp $ λ a₁ a₂ n x h₁ h₂, begin
+    rcases mem_map.1 h₁ with ⟨b₁, mb₁, rfl⟩,
+    rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩,
+    exact n rfl
+  end⟩
 
 theorem nodup_sigma {σ : α → Type*} {l₁ : list α} {l₂ : Π a, list (σ a)}
   (d₁ : nodup l₁) (d₂ : ∀ a, nodup (l₂ a)) : nodup (l₁.sigma l₂) :=
  nodup_bind.2
   ⟨λ a ma, nodup_map (λ b b' h, by injection h with _ h; exact eq_of_heq h) (d₂ a),
-  d₁.imp (λ a₁ a₂ n x,
-    suffices ∀ (b₁ : σ a₁), sigma.mk a₁ b₁ = x → b₁ ∈ l₂ a₁ →
-      ∀ (b₂ : σ a₂), sigma.mk a₂ b₂ = x → b₂ ∉ l₂ a₂,
-      by simpa only [and_comm, mem_map, exists_imp_distrib, and_imp],
-    λ b₁ e mb₁ b₂ e' mb₂, by subst e'; injection e; contradiction)⟩
+  d₁.imp $ λ a₁ a₂ n x h₁ h₂, begin
+    rcases mem_map.1 h₁ with ⟨b₁, mb₁, rfl⟩,
+    rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩,
+    exact n rfl
+  end⟩
 
 theorem nodup_filter_map {f : α → option β} {l : list α}
   (H : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a') :
@@ -3743,10 +3737,8 @@ theorem nodup_concat {a : α} {l : list α} (h : a ∉ l) (h' : nodup l) : nodup
 by rw concat_eq_append; 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) :=
-begin
-  by_cases h' : a ∈ l, {rw [insert_of_mem h'], exact h},
-  rw [insert_of_not_mem h', nodup_cons], split; assumption
-end
+if h' : a ∈ l then by rw [insert_of_mem h']; exact h
+else by rw [insert_of_not_mem h', nodup_cons]; split; assumption
 
 theorem nodup_union [decidable_eq α] (l₁ : list α) {l₂ : list α} (h : nodup l₂) :
   nodup (l₁ ∪ l₂) :=
@@ -3846,7 +3838,8 @@ end erase_dup
     from λ e, e ▸ lt_succ_of_le (le_add_right _ _),
   have l : m = s ∨ s + 1 ≤ m ↔ s ≤ m,
     by simpa only [eq_comm] using (@le_iff_eq_or_lt _ _ s m).symm,
-  (mem_cons_iff _ _ _).trans $ by simp only [@mem_range' (s+1) n, or_and_distrib_left, or_iff_right_of_imp this, l, add_right_comm]; refl
+  (mem_cons_iff _ _ _).trans $ by simp only [mem_range',
+    or_and_distrib_left, or_iff_right_of_imp this, l, add_right_comm]; refl
 
 theorem map_add_range' (a) : ∀ s n : ℕ, map ((+) a) (range' s n) = range' (a + s) n
 | s 0     := rfl
@@ -3950,8 +3943,7 @@ theorem reverse_range' : ∀ s n : ℕ,
 | s 0     := rfl
 | s (n+1) := by rw [range'_concat, reverse_append, range_succ_eq_map];
   simpa only [show s + (n + 1) - 1 = s + n, from rfl, (∘),
-    λ a i, show a - 1 - i = a - succ i,
-    by rw [nat.sub_sub, add_comm]; refl,
+    λ a i, show a - 1 - i = a - succ i, from pred_sub _ _,
     reverse_singleton, map_cons, nat.sub_zero, cons_append,
     nil_append, eq_self_iff_true, true_and, map_map]
   using reverse_range' s n
@@ -4030,8 +4022,6 @@ end tfae
 
 end list
 
-theorem option.to_list_nodup {α} (o : option α) : o.to_list.nodup :=
-match o with
-| none := list.nodup_nil
-| some x := list.nodup_singleton x
-end
\ No newline at end of file
+theorem option.to_list_nodup {α} : ∀ o : option α, o.to_list.nodup
+| none     := list.nodup_nil
+| (some x) := list.nodup_singleton x
diff --git a/data/nat/basic.lean b/data/nat/basic.lean
index 05d8bc5598d05..b534e464af2af 100644
--- a/data/nat/basic.lean
+++ b/data/nat/basic.lean
@@ -12,6 +12,9 @@ universe u
 namespace nat
 variables {m n k : ℕ}
 
+theorem succ_inj' {n m : ℕ} : succ n = succ m ↔ n = m :=
+⟨succ_inj, congr_arg _⟩
+
 theorem pred_sub (n m : ℕ) : pred n - m = pred (n - m) :=
 by rw [← sub_one, nat.sub_sub, one_add]; refl
 
diff --git a/data/polynomial.lean b/data/polynomial.lean
index ca8db0e9f36f8..d9b0e75a361e0 100644
--- a/data/polynomial.lean
+++ b/data/polynomial.lean
@@ -377,12 +377,10 @@ by unfold monic; apply_instance
 
 @[simp] lemma degree_zero : degree (0 : polynomial α) = ⊥ := rfl
 
-@[simp] lemma nat_degree_zero : nat_degree (0 : polynomial α) = 0 :=
-rfl
+@[simp] lemma nat_degree_zero : nat_degree (0 : polynomial α) = 0 := rfl
 
 @[simp] lemma degree_C (ha : a ≠ 0) : degree (C a) = (0 : with_bot ℕ) :=
-show sup (ite (a = 0) ∅ {0}) some = 0,
-by rw [if_neg ha]; refl
+show sup (ite (a = 0) ∅ {0}) some = 0, by rw if_neg ha; refl
 
 lemma degree_C_le : degree (C a) ≤ (0 : with_bot ℕ) :=
 by by_cases h : a = 0; [rw [h, C_0], rw [degree_C h]]; [exact bot_le, exact le_refl _]
@@ -403,7 +401,7 @@ by rw [nat_degree, hn]; refl
 
 @[simp] lemma degree_le_nat_degree : degree p ≤ nat_degree p :=
 begin
-  by_cases hp : p = 0, { rw [hp], exact bot_le },
+  by_cases hp : p = 0, { rw hp, exact bot_le },
   rw [degree_eq_nat_degree hp],
   exact le_refl _
 end
@@ -413,7 +411,7 @@ by unfold nat_degree; rw h
 
 lemma le_degree_of_ne_zero (h : p n ≠ 0) : (n : with_bot ℕ) ≤ degree p :=
 show @has_le.le (with_bot ℕ) _ (some n : with_bot ℕ) (p.support.sup some : with_bot ℕ),
-from finset.le_sup ((finsupp.mem_support_iff _ _).2 h)
+from finset.le_sup (finsupp.mem_support_iff.2 h)
 
 lemma le_nat_degree_of_ne_zero (h : p n ≠ 0) : n ≤ nat_degree p :=
 begin
@@ -425,8 +423,8 @@ end
 lemma degree_le_degree (h : q (nat_degree p) ≠ 0) : degree p ≤ degree q :=
 begin
   by_cases hp : p = 0,
-  { rw [hp], exact bot_le },
-  { rw [degree_eq_nat_degree hp], exact le_degree_of_ne_zero h }
+  { rw hp, exact bot_le },
+  { rw degree_eq_nat_degree hp, exact le_degree_of_ne_zero h }
 end
 
 @[simp] lemma nat_degree_C (a : α) : nat_degree (C a) = 0 :=
@@ -471,7 +469,7 @@ calc degree (p + q) = ((p + q).support).sup some : rfl
 @[simp] lemma leading_coeff_zero : leading_coeff (0 : polynomial α) = 0 := rfl
 
 @[simp] lemma leading_coeff_eq_zero : leading_coeff p = 0 ↔ p = 0 :=
-⟨λ h, by_contradiction $ λ hp, mt (mem_support_iff _ _).1
+⟨λ h, by_contradiction $ λ hp, mt mem_support_iff.1
   (not_not.2 h) (mem_of_max (degree_eq_nat_degree hp)),
 λ h, h.symm ▸ leading_coeff_zero⟩
 
@@ -580,19 +578,20 @@ begin
   assume i hpi hid,
   rw [finset.sum_eq_single (nat_degree q), if_neg (mt add_right_cancel hid)],
   { assume j hqj hjd,
-    have hi : j < nat_degree q, from lt_of_le_of_ne (le_nat_degree_of_ne_zero ((mem_support_iff _ _).1 hqj)) hjd,
+    have hi : j < nat_degree q, from lt_of_le_of_ne (le_nat_degree_of_ne_zero (mem_support_iff.1 hqj)) hjd,
     have hj : i < nat_degree p, from lt_of_le_of_ne (le_nat_degree_of_ne_zero hpi) hid,
     exact if_neg (ne_of_lt $ add_lt_add hj hi) },
-  { intro, rw [if_neg (mt add_right_cancel hid)] }
+  { intro, rw if_neg (mt add_right_cancel hid) }
 end,
 begin
   rw [mul_def, sum_apply, finsupp.sum, finset.sum_eq_single (nat_degree p),
       sum_apply, finsupp.sum, finset.sum_eq_single (nat_degree q),
       single_apply, if_pos rfl, leading_coeff, leading_coeff],
   { intros j hjq hjd, rw [single_apply, if_neg (mt add_left_cancel hjd)] },
-  { intro H, rw [single_eq_same, by_contradiction (mt (mem_support_iff _ _).2 H), mul_zero] },
+  { intro H, rw [single_eq_same, not_mem_support_iff.1 H, mul_zero] },
   { simpa only [mem_support_iff, sum_apply, single_apply] },
-  { intro H, simp only [sum_apply, single_apply, by_contradiction (mt (mem_support_iff _ _).2 H), zero_mul, if_t_t], exact sum_const_zero }
+  { intro H, simp only [sum_apply, single_apply, not_mem_support_iff.1 H,
+      zero_mul, if_t_t], exact sum_const_zero }
 end
 
 lemma degree_mul_eq' (h : leading_coeff p * leading_coeff q ≠ 0) :
@@ -1280,12 +1279,12 @@ lemma derivative_apply (p : polynomial α) (n : ℕ) : (derivative p) n = p (n +
 begin
   rw [derivative],
   simp only [finsupp.sum, X_pow_apply, sum_apply, C_mul_apply],
-  rw [finset.sum_eq_single (n + 1)],
+  rw finset.sum_eq_single (n + 1),
   { rw [if_pos (nat.add_sub_cancel _ _), mul_one, nat.cast_add, nat.cast_one] },
   { assume b, cases b,
     { intros, rw [nat.cast_zero, mul_zero, zero_mul] },
     { intros _ H, rw [nat.succ_sub_one b, if_neg (mt (congr_arg nat.succ) H), mul_zero] } },
-  { intro H, rw [by_contradiction (mt (mem_support_iff _ _).2 H), zero_mul, zero_mul] }
+  { intro H, rw [not_mem_support_iff.1 H, zero_mul, zero_mul] }
 end
 
 @[simp] lemma derivative_zero : derivative (0 : polynomial α) = 0 :=
@@ -1335,20 +1334,15 @@ calc derivative (f * g) = f.sum (λn a, g.sum (λm b, C ((a * b) * (n + m : ℕ)
   ... = f.sum (λn a, g.sum (λm b,
       (C (a * n) * X^(n - 1)) * (C b * X^m) + (C a * X^n) * (C (b * m) * X^(m - 1)))) :
     sum_congr rfl $ assume n hn, sum_congr rfl $ assume m hm,
-      by simp only [nat.cast_add, mul_add, add_mul, C_add, C_mul, mul_assoc, mul_left_comm];
-      cases n; simp only [nat.cast_zero, C_0, nat.succ_sub_succ, zero_mul, mul_zero,
-        zero_add, nat.sub_zero, pow_zero, pow_add, one_mul, mul_one];
+      by simp only [nat.cast_add, mul_add, add_mul, C_add, C_mul];
+      cases n; simp only [nat.succ_sub_succ, pow_zero];
       cases m; simp only [nat.cast_zero, C_0, nat.succ_sub_succ, zero_mul, mul_zero,
-        zero_add, nat.sub_zero, pow_zero, pow_add, one_mul, mul_one];
-      simp only [pow_succ, mul_comm, mul_left_comm]
+        nat.sub_zero, pow_zero, pow_add, one_mul, pow_succ, mul_comm, mul_left_comm]
   ... = derivative f * g + f * derivative g :
     begin
-      conv {
-        to_rhs,
-        congr,
+      conv { to_rhs, congr,
         { rw [← sum_C_mul_X_eq g] },
-        { rw [← sum_C_mul_X_eq f] },
-      },
+        { rw [← sum_C_mul_X_eq f] } },
       unfold derivative finsupp.sum,
       simp only [sum_add_distrib, finset.mul_sum, finset.sum_mul]
     end
diff --git a/data/set/lattice.lean b/data/set/lattice.lean
index e3254a623d182..b05c20cb0bb60 100644
--- a/data/set/lattice.lean
+++ b/data/set/lattice.lean
@@ -357,6 +357,12 @@ theorem sInter_union (S T : set (set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂
 
 @[simp] theorem sInter_insert (s : set α) (T : set (set α)) : ⋂₀ (insert s T) = s ∩ ⋂₀ T := Inf_insert
 
+theorem sUnion_pair (s t : set α) : ⋃₀ {s, t} = s ∪ t :=
+(sUnion_insert _ _).trans $ by rw [union_comm, sUnion_singleton]
+
+theorem sInter_pair (s t : set α) : ⋂₀ {s, t} = s ∩ t :=
+(sInter_insert _ _).trans $ by rw [inter_comm, sInter_singleton]
+
 @[simp] theorem sUnion_image (f : α → set β) (s : set α) : ⋃₀ (f '' s) = ⋃ x ∈ s, f x := Sup_image
 
 @[simp] theorem sInter_image (f : α → set β) (s : set α) : ⋂₀ (f '' s) = ⋂ x ∈ s, f x := Inf_image
diff --git a/order/basic.lean b/order/basic.lean
index 465190da2b146..4ffa0f7b90562 100644
--- a/order/basic.lean
+++ b/order/basic.lean
@@ -324,6 +324,13 @@ instance is_extensional_of_is_strict_total_order'
 @[algebra] class is_well_order (α : Type u) (r : α → α → Prop) extends is_strict_total_order' α r : Prop :=
 (wf : well_founded r)
 
+instance is_well_order.is_strict_total_order {α} (r : α → α → Prop) [is_well_order α r] : is_strict_total_order α r := by apply_instance
+instance is_well_order.is_extensional {α} (r : α → α → Prop) [is_well_order α r] : is_extensional α r := by apply_instance
+instance is_well_order.is_trichotomous {α} (r : α → α → Prop) [is_well_order α r] : is_trichotomous α r := by apply_instance
+instance is_well_order.is_trans {α} (r : α → α → Prop) [is_well_order α r] : is_trans α r := by apply_instance
+instance is_well_order.is_irrefl {α} (r : α → α → Prop) [is_well_order α r] : is_irrefl α r := by apply_instance
+instance is_well_order.is_asymm {α} (r : α → α → Prop) [is_well_order α r] : is_asymm α r := by apply_instance
+
 instance empty_relation.is_well_order [subsingleton α] : is_well_order α empty_relation :=
 { trichotomous := λ a b, or.inr $ or.inl $ subsingleton.elim _ _,
   irrefl       := λ a, id,
diff --git a/order/conditionally_complete_lattice.lean b/order/conditionally_complete_lattice.lean
index 5bb9f8b8eff63..19c6f7def948e 100644
--- a/order/conditionally_complete_lattice.lean
+++ b/order/conditionally_complete_lattice.lean
@@ -62,13 +62,11 @@ a notion of maximum and minimum, i.e., a lattice structure, see later on.-/
 
 /-If a set is included in another one, boundedness of the second implies boundedness
 of the first-/
-lemma bdd_above_subset (_ : s ⊆ t) (_ : bdd_above t) : bdd_above s :=
-let ⟨w, hw⟩ := ‹bdd_above t› in  /-hw : ∀ (y : α), y ∈ t → y ≤ w-/
-⟨w, assume (y : α) (_ : y ∈ s), hw _ (‹s ⊆ t› ‹y ∈ s›)⟩
+lemma bdd_above_subset (st : s ⊆ t) : bdd_above t → bdd_above s
+| ⟨w, hw⟩ := ⟨w, λ y ys, hw _ (st ys)⟩
 
-lemma bdd_below_subset (_ : s ⊆ t) (_ : bdd_below t) : bdd_below s :=
-let ⟨w, hw⟩ := ‹bdd_below t› in  /-hw : ∀ (y : α), y ∈ t → w ≤ y-/
-⟨w, assume (y : α) (_ : y ∈ s), hw _ (‹s ⊆ t› ‹y ∈ s›)⟩
+lemma bdd_below_subset (st : s ⊆ t) : bdd_below t → bdd_below s
+| ⟨w, hw⟩ := ⟨w, λ y ys, hw _ (st ys)⟩
 
 /- Boundedness of intersections of sets, in different guises, deduced from the
 monotonicity of boundedness.-/
@@ -127,12 +125,12 @@ show (bdd_above s ∧ bdd_above t) → bdd_above (s ∪ t), from
 
 /--Adding a point to a set preserves its boundedness above.-/
 @[simp] lemma bdd_above_insert : bdd_above (insert a s) ↔ bdd_above s :=
-⟨show bdd_above (insert a s) → bdd_above s, from bdd_above_subset (by simp only [set.subset_insert]),
- show bdd_above s → bdd_above (insert a s), by rw [insert_eq]; simp only [bdd_above_singleton, and_self, bdd_above_union, forall_true_iff] {contextual := tt}⟩
+⟨bdd_above_subset (by simp only [set.subset_insert]),
+ λ h, by rw [insert_eq, bdd_above_union]; exact ⟨bdd_above_singleton, h⟩⟩
 
 /--A finite set is bounded above.-/
-lemma bdd_above_finite [inhabited α] (_ : finite s) : bdd_above s :=
-by apply finite.induction_on ‹finite s›; simp only [bdd_above_insert, imp_self, forall_const, forall_true_iff,bdd_above_empty]
+lemma bdd_above_finite [inhabited α] (hs : finite s) : bdd_above s :=
+finite.induction_on hs bdd_above_empty $ λ a s _ _, bdd_above_insert.2
 
 /--A finite union of sets which are all bounded above is still bounded above.-/
 lemma bdd_above_finite_union [inhabited α] {β : Type v} {I : set β} {S : β → set α} (H : finite I) :
diff --git a/order/filter.lean b/order/filter.lean
index 4433956502bda..1041d9d07836e 100644
--- a/order/filter.lean
+++ b/order/filter.lean
@@ -25,8 +25,8 @@ lemma Inf_eq_finite_sets {s : set α} :
 le_antisymm
   (le_infi $ assume t, le_infi $ assume ⟨_, h⟩, Inf_le_Inf h)
   (le_Inf $ assume b h, infi_le_of_le {b} $ infi_le_of_le
-  (by simp only [h, finite_singleton, and_self, mem_set_of_eq,
-    singleton_subset_iff]) $ Inf_le $ by simp only [mem_singleton])
+    (by simp only [h, finite_singleton, and_self, mem_set_of_eq,
+      singleton_subset_iff]) $ Inf_le $ by simp only [mem_singleton])
 
 lemma infi_insert_finset {ι : Type v} {s : finset ι} {f : ι → α} {i : ι} :
   (⨅j∈insert i s, f j) = f i ⊓ (⨅j∈s, f j) :=
@@ -505,10 +505,10 @@ le_antisymm
 
 lemma infi_sup_eq { f : filter α } {g : ι → filter α} : (⨅ x, f ⊔ g x) = f ⊔ infi g :=
 calc (⨅ x, f ⊔ g x) = (⨅ x (h : ∃i, g i = x), f ⊔ x) :
-  by simp only [infi_exists]; rw [infi_comm]; simp only [infi_infi_eq_right, eq_self_iff_true]
+  by simp only [infi_exists]; rw infi_comm; simp only [infi_infi_eq_right, eq_self_iff_true]
   ... = f ⊔ Inf {x | ∃i, g i = x} : binfi_sup_eq
-  ... = f ⊔ infi g : by rw [Inf_eq_infi]; dsimp; simp only [infi_exists];
-                        rw [infi_comm]; simp only [infi_infi_eq_right, eq_self_iff_true]
+  ... = f ⊔ infi g : by rw Inf_eq_infi; dsimp; simp only [infi_exists];
+                        rw infi_comm; simp only [infi_infi_eq_right, eq_self_iff_true]
 
 lemma mem_infi_sets_finset {s : finset α} {f : α → filter β} :
   ∀t, t ∈ (⨅a∈s, f a).sets ↔ (∃p:α → set β, (∀a∈s, p a ∈ (f a).sets) ∧ (⋂a∈s, p a) ⊆ t) :=
@@ -955,8 +955,7 @@ end
 le_antisymm
   (le_principal_iff.2 $ sets_of_superset (map f (pure a)) (image_mem_map singleton_mem_pure_sets) $
     by simp only [image_singleton, mem_singleton, singleton_subset_iff])
-  (le_map $ assume s,
-  begin
+  (le_map $ assume s, begin
     simp only [mem_image, pure_def, mem_principal_sets, singleton_subset_iff],
     exact assume has, ⟨a, has, rfl⟩
   end)
@@ -1780,8 +1779,9 @@ le_of_inf_eq $ ultrafilter_unique hf h inf_le_left
 lemma mem_or_compl_mem_of_ultrafilter (hf : ultrafilter f) (s : set α) :
   s ∈ f.sets ∨ - s ∈ f.sets :=
 classical.or_iff_not_imp_right.2 $ assume : - s ∉ f.sets,
-  have f ≤ principal s,
-    from le_of_ultrafilter hf $ assume h, this $ mem_sets_of_neq_bot $ by simp only [h, eq_self_iff_true, lattice.neg_neg],
+  have f ≤ principal s, from
+    le_of_ultrafilter hf $ assume h, this $ mem_sets_of_neq_bot $
+    by simp only [h, eq_self_iff_true, lattice.neg_neg],
   by simp only [le_principal_iff] at this; assumption
 
 lemma mem_or_mem_of_ultrafilter {s t : set α} (hf : ultrafilter f) (h : s ∪ t ∈ f.sets) :
@@ -1862,7 +1862,7 @@ begin
   split,
   { induction fs generalizing t,
     case nil { simp only [sequence, pure_def, imp_self, forall₂_nil_left_iff, pure_def,
-    exists_eq_left, mem_principal_sets, set.pure_def, singleton_subset_iff, traverse_nil] },
+      exists_eq_left, mem_principal_sets, set.pure_def, singleton_subset_iff, traverse_nil] },
     case cons : b fs ih t {
       assume ht,
       rcases mem_seq_sets_iff.1 ht with ⟨u, hu, v, hv, ht⟩,
diff --git a/set_theory/ordinal.lean b/set_theory/ordinal.lean
index 465f6f3e0b76b..9ca0185e8cb0d 100644
--- a/set_theory/ordinal.lean
+++ b/set_theory/ordinal.lean
@@ -100,7 +100,7 @@ by haveI := f.to_order_embedding.is_well_order; exact
 
 @[simp] theorem antisymm_symm [is_well_order α r] [is_well_order β s]
   (f : r ≼i s) (g : s ≼i r) : (antisymm f g).symm = antisymm g f :=
-order_iso.eq_of_to_fun_eq $ rfl
+order_iso.eq_of_to_fun_eq rfl
 
 theorem eq_or_principal [is_well_order β s] (f : r ≼i s) : surjective f ∨ ∃ b, ∀ x, s x b ↔ ∃ y, f y = x :=
 or_iff_not_imp_right.2 $ λ h b,
@@ -119,7 +119,7 @@ def cod_restrict (p : set β) (f : r ≼i s) (H : ∀ a, f a ∈ p) : r ≼i sub
 
 def le_add (r : α → α → Prop) (s : β → β → Prop) : r ≼i sum.lex r s :=
 ⟨⟨⟨sum.inl, λ _ _, sum.inl.inj⟩, λ a b, sum.lex_inl_inl.symm⟩,
-  λ a b, by cases b; [exact (λ _, ⟨_, rfl⟩), exact (false.elim ∘ sum.lex_inr_inl)]⟩
+  λ a b, by cases b; [exact λ _, ⟨_, rfl⟩, exact false.elim ∘ sum.lex_inr_inl]⟩
 
 @[simp] theorem le_add_apply (r : α → α → Prop) (s : β → β → Prop)
   (a) : le_add r s a = sum.inl a := rfl
@@ -394,18 +394,20 @@ private theorem wo : is_well_order U R :=
       (λ o, o.imp (subtype.eq ∘ subtype.mk.inj)
       (R_iff sc _ _).2),
   irrefl :=  λ ⟨a, au⟩ h, let ⟨s, sc, ha⟩ := mem_U.1 au in
+    -- by haveI := s.2.2; exact irrefl _ ((R_iff hc sc _ ha).1 h),
     @irrefl _ s.2.1 s.2.2.1.2.1 _ ((R_iff sc _ ha).1 h),
   trans := λ ⟨a, au⟩ ⟨b, bu⟩ ⟨d, du⟩ ab bd,
     let ⟨s, sc, as, bs⟩ := mem_U2 au bu, ⟨t, tc, dt⟩ := mem_U.1 du,
         ⟨k, kc, ks, kt⟩ := hc.directed sc tc in begin
       simp only [R_iff hc kc, sub_of_le ks as, sub_of_le ks bs, sub_of_le kt dt] at ab bd ⊢,
+      -- haveI := k.2.2, exact trans ab bd
       exact @trans _ k.2.1 k.2.2.1.2.2 _ _ _ ab bd
     end,
   wf := ⟨λ ⟨a, au⟩, let ⟨s, sc, ha⟩ := mem_U.1 au in
     suffices ∀ (a : s.1) (au : a.1 ∈ U), acc R ⟨a.1, au⟩, from this ⟨a, ha⟩ au,
-    (λ a, acc.rec_on ((@is_well_order.wf _ _ s.2.2).apply a) $
+    λ a, acc.rec_on ((@is_well_order.wf _ _ s.2.2).apply a) $
     λ ⟨a, ha⟩ H IH au, ⟨_, λ ⟨b, hb⟩ h,
-      let ⟨hb, h⟩ := R_ex sc ha h in IH ⟨b, hb⟩ h _⟩)⟩ }
+      let ⟨hb, h⟩ := R_ex sc ha h in IH ⟨b, hb⟩ h _⟩⟩ }
 
 theorem chain_ub : ∃ ub, ∀ a ∈ c, a ≤ ub :=
 ⟨⟨U, R, wo⟩, λ s sc, ⟨⟨⟨⟨
@@ -431,7 +433,7 @@ let f : (insert a m.1 : set σ) ≃ (m.1 ⊕ unit) :=
   λ x, sum.cases_on x (λ x, ⟨x.1, or.inr x.2⟩) (λ _, ⟨a, or.inl rfl⟩),
   λ x, match x with
     | ⟨_, or.inl rfl⟩ := by dsimp only; rw dif_neg ha
-    | ⟨x, or.inr h⟩ := by dsimp only; rw [dif_pos h]
+    | ⟨x, or.inr h⟩ := by dsimp only; rw dif_pos h
     end,
   λ x, by rcases x with ⟨x, h⟩ | ⟨⟨⟩⟩; dsimp only;
     [rw [dif_pos h], rw [dif_neg ha]]⟩ in
@@ -444,7 +446,7 @@ let g : m.2.1 ≼i r' := ⟨⟨⟨sum.inl, λ a b, sum.inl.inj⟩,
   λ a b h, begin
     rcases b with b | ⟨⟨⟩⟩,
     { exact ⟨_, rfl⟩ },
-    { exact false.elim (sum.lex_inr_inl h) }
+    { cases sum.lex_inr_inl h }
   end⟩ in
 ha (sub_of_le (MM m' ⟨g.trans
   (initial_seg.of_iso (order_iso.preimage f r').symm),
@@ -707,16 +709,16 @@ theorem succ_le {a b : ordinal} : succ a ≤ b ↔ a < b :=
 ⟨lt_of_lt_of_le (lt_succ_self _),
 induction_on a $ λ α r hr, induction_on b $ λ β s hs ⟨⟨f, t, hf⟩⟩, begin
   refine ⟨⟨@order_embedding.of_monotone (α ⊕ punit) β _ _
-    (@sum.lex.is_well_order _ _ _ _ hr _).1.1 
+    (@sum.lex.is_well_order _ _ _ _ hr _).1.1
     (@is_asymm_of_is_trans_of_is_irrefl _ _ hs.1.2.2 hs.1.2.1)
     (sum.rec _ _) (λ a b, _), λ a b, _⟩⟩,
   { exact f }, { exact λ _, t },
-  { rcases a with a|u; rcases b with b|u,
+  { rcases a with a|_; rcases b with b|_,
     { simpa only [sum.lex_inl_inl] using f.ord'.1 },
     { intro _, rw hf, exact ⟨_, rfl⟩ },
     { exact false.elim ∘ sum.lex_inr_inl },
     { exact false.elim ∘ sum.lex_inr_inr.1 } },
-  { rcases a with a|u,
+  { rcases a with a|_,
     { intro h, have := @principal_seg.init _ _ _ _ hs.1.2.2 ⟨f, t, hf⟩ _ _ h,
       cases this with w h, exact ⟨sum.inl w, h⟩ },
     { intro h, cases (hf b).1 h with w h, exact ⟨sum.inl w, h⟩ } }
@@ -762,21 +764,15 @@ theorem add_le_add_left {a b : ordinal} : a ≤ b → ∀ c, c + a ≤ c + b :=
 induction_on a $ λ α₁ r₁ _, induction_on b $ λ α₂ r₂ _ ⟨⟨⟨f, fo⟩, fi⟩⟩ c,
 induction_on c $ λ β s _,
 ⟨⟨⟨(embedding.refl _).sum_congr f,
-  λ a b, ⟨λ H, match a, b, H with
-    | _, _, sum.lex.inl _ h := sum.lex.inl _ h
-    | _, _, sum.lex.inr _ h := sum.lex.inr _ (fo.1 h)
-    | _, _, sum.lex.sep _ _ _ _ := sum.lex.sep _ _ _ _
-    end,
-    λ H, match a, b, H with
-    | sum.inl a, sum.inl b, H := sum.lex.inl _ $ sum.lex_inl_inl.1 H
-    | sum.inl a, sum.inr b, H := sum.lex.sep _ _ _ _
-    | sum.inr a, sum.inl b, H := false.elim $ sum.lex_inr_inl H
-    | sum.inr a, sum.inr b, H := sum.lex.inr _ $ fo.2 $ sum.lex_inr_inr.1 H
-    end⟩⟩,
+  λ a b, match a, b with
+    | sum.inl a, sum.inl b := sum.lex_inl_inl.trans sum.lex_inl_inl.symm
+    | sum.inl a, sum.inr b := by apply iff_of_true; apply sum.lex.sep
+    | sum.inr a, sum.inl b := by apply iff_of_false; exact sum.lex_inr_inl
+    | sum.inr a, sum.inr b := sum.lex_inr_inr.trans $ fo.trans sum.lex_inr_inr.symm
+    end⟩,
   λ a b H, match a, b, H with
-    | sum.inl a, sum.inl b, H := ⟨sum.inl b, rfl⟩
-    | sum.inl a, sum.inr b, H := false.elim $ sum.lex_inr_inl H
-    | sum.inr a, sum.inl b, H := ⟨sum.inl b, rfl⟩
+    | _,         sum.inl b, _ := ⟨sum.inl b, rfl⟩
+    | sum.inl a, sum.inr b, H := (sum.lex_inr_inl H).elim
     | sum.inr a, sum.inr b, H := let ⟨w, h⟩ := fi _ _ (sum.lex_inr_inr.1 H) in
         ⟨sum.inr w, congr_arg sum.inr h⟩
     end⟩⟩
@@ -788,7 +784,8 @@ theorem add_le_add_iff_left (a) {b c : ordinal} : a + b ≤ a + c ↔ b ≤ c :=
 ⟨induction_on a $ λ α r hr, induction_on b $ λ β₁ s₁ hs₁, induction_on c $ λ β₂ s₂ hs₂ ⟨f⟩, ⟨
   have fl : ∀ a, f (sum.inl a) = sum.inl a := λ a,
     by simpa only [initial_seg.trans_apply, initial_seg.le_add_apply]
-      using @initial_seg.eq _ _ _ _ (@sum.lex.is_well_order _ _ _ _ hr hs₂) ((initial_seg.le_add r s₁).trans f) (initial_seg.le_add r s₂) a,
+      using @initial_seg.eq _ _ _ _ (@sum.lex.is_well_order _ _ _ _ hr hs₂)
+        ((initial_seg.le_add r s₁).trans f) (initial_seg.le_add r s₂) a,
   have ∀ b, {b' // f (sum.inr b) = sum.inr b'}, begin
     intro b, cases e : f (sum.inr b),
     { rw ← fl at e, have := f.inj e, contradiction },
@@ -798,16 +795,13 @@ theorem add_le_add_iff_left (a) {b c : ordinal} : a + b ≤ a + c ↔ b ≤ c :=
   have fr : ∀ b, f (sum.inr b) = sum.inr (g b), from λ b, (this b).2,
   ⟨⟨⟨g, λ x y h, by injection f.inj
     (by rw [fr, fr, h] : f (sum.inr x) = f (sum.inr y))⟩,
-    λ a b, by simpa only [sum.lex_inr_inr, fr, order_embedding.coe_fn_to_embedding, initial_seg.coe_fn_to_order_embedding, function.embedding.coe_fn_mk]
-      using @order_embedding.ord _ _ _ _
-      f.to_order_embedding (sum.inr a) (sum.inr b)⟩,
+    λ a b, by simpa only [sum.lex_inr_inr, fr, order_embedding.coe_fn_to_embedding,
+        initial_seg.coe_fn_to_order_embedding, function.embedding.coe_fn_mk]
+      using @order_embedding.ord _ _ _ _ f.to_order_embedding (sum.inr a) (sum.inr b)⟩,
     λ a b H, begin
-      have nex : ¬ ∃ (a : α), f (sum.inl a) = sum.inr b :=
-        λ ⟨a, e⟩, by rw [fl] at e; injection e,
-      have : sum.lex r s₂ (sum.inr b) (f (sum.inr a)) → ∃ a', f a' = sum.inr b := f.init (sum.inr a) (sum.inr b),
-      rw [fr] at this, rcases this (sum.lex_inr_inr.2 H) with ⟨a'|a', h⟩,
-      { exact false.elim (nex ⟨a', h⟩) },
-      rw [fr, sum.inr.inj_iff] at h, exact ⟨a', h⟩
+      rcases f.init' (by rw fr; exact sum.lex_inr_inr.2 H) with ⟨a'|a', h⟩,
+      { rw fl at h, cases h },
+      { rw fr at h, exact ⟨a', sum.inr.inj h⟩ }
     end⟩⟩,
 λ h, add_le_add_left h _⟩
 
@@ -952,11 +946,9 @@ induction_on c $ λ β s hs, (@type_le' _ _ _ _
   (@sum.lex.is_well_order _ _ _ _ hr₁ hs)
   (@sum.lex.is_well_order _ _ _ _ hr₂ hs)).2
 ⟨⟨embedding.sum_congr f (embedding.refl _), λ a b, begin
-  split,
-  { intro H, cases H with _ _ H1 _ _ H1 _ _ H1; constructor,
-    { rw ← fo, assumption }, assumption },
-  { intro H, cases a with a a; cases b with b b; cases H; constructor,
-    { rw fo, assumption }, assumption }
+  split; intro H,
+  { cases H; constructor; [rwa ← fo, assumption] },
+  { cases a with a a; cases b with b b; cases H; constructor; [rwa fo, assumption] }
 end⟩⟩
 
 theorem le_add_left (a b : ordinal) : a ≤ b + a :=
@@ -971,8 +963,8 @@ match lt_or_eq_of_le (le_add_left b a), lt_or_eq_of_le (le_add_right a b) with
     resetI,
     rw [← typein_top f, ← typein_top g, le_iff_lt_or_eq,
         le_iff_lt_or_eq, typein_lt_typein, typein_lt_typein],
-    rcases trichotomous_of (sum.lex r₁ r₂) g.top f.top with h|h|h,
-    { left, left, assumption }, { rw h, left, right, refl }, { right, left, assumption }
+    rcases trichotomous_of (sum.lex r₁ r₂) g.top f.top with h|h|h;
+    [exact or.inl (or.inl h), {left, right, rw h}, exact or.inr (or.inl h)]
   end) h₁ h₂
 end
 
@@ -1239,7 +1231,7 @@ theorem add_le_of_limit {a b c : ordinal.{u}}
 ⟨λ h b' l, le_trans (add_le_add_left (le_of_lt l) _) h,
 λ H, le_of_not_lt $
 induction_on a (λ α r _, induction_on b $ λ β s _ h H l, begin
-  try_for 2000 { resetI,
+  resetI,
   suffices : ∀ x : β, sum.lex r s (sum.inr x) (enum _ _ l),
   { cases enum _ _ l with x x,
     { cases this (enum s 0 h.pos) },
@@ -1254,7 +1246,7 @@ induction_on a (λ α r _, induction_on b $ λ β s _ h H l, begin
     { exact sum.inl a },
     { exact sum.inr ⟨b, by cases h; assumption⟩ } },
   { rcases a with ⟨a | a, h₁⟩; rcases b with ⟨b | b, h₂⟩; cases h₁; cases h₂;
-    rintro ⟨H⟩; constructor; assumption } }
+      rintro ⟨⟩; constructor; assumption }
 end) h H⟩
 
 theorem add_is_normal (a : ordinal) : is_normal ((+) a) :=
@@ -1326,7 +1318,7 @@ theorem univ_umax : univ.{u (max (u+1) v)} = univ.{u v} := congr_fun lift_umax _
 
 def lift.principal_seg : @principal_seg ordinal.{u} ordinal.{max (u+1) v} (<) (<) :=
 ⟨↑lift.initial_seg.{u (max (u+1) v)}, univ.{u v}, begin
-  try_for 3000 { refine λ b, induction_on b _, introsI β s _,
+  refine λ b, induction_on b _, introsI β s _,
   rw [univ, ← lift_umax], split; intro h,
   { rw ← lift_id (type s) at h ⊢,
     cases lift_type_lt.1 h with f, cases f with f a hf,
@@ -1343,7 +1335,7 @@ def lift.principal_seg : @principal_seg ordinal.{u} ordinal.{max (u+1) v} (<) (<
   { cases h with a e, rw [← e],
     apply induction_on a, intros α r _,
     exact lift_type_lt.{u (u+1) (max (u+1) v)}.2
-      ⟨typein.principal_seg r⟩ } }
+      ⟨typein.principal_seg r⟩ }
 end⟩
 
 @[simp] theorem lift.principal_seg_coe :
@@ -1420,8 +1412,8 @@ begin
   have : is_well_order unit empty_relation := by apply_instance,
   refine ⟨order_embedding.collapse (order_embedding.of_monotone _ _)⟩,
   { apply sum.rec, exact λ _, 0, exact nat.succ },
-  { intros a b, cases a; cases b; intro H; cases H with _ _ H _ _ H,
-    { cases H }, { exact nat.succ_pos _ }, { exact nat.succ_lt_succ H } }
+  { intros a b, cases a; cases b; intro H; cases H with _ _ H _ _ H;
+    [cases H, exact nat.succ_pos _, exact nat.succ_lt_succ H] }
 end
 
 @[simp] theorem one_add_of_omega_le {o} (h : omega ≤ o) : 1 + o = o :=
@@ -1471,21 +1463,11 @@ type_eq_zero_iff_empty.2 (λ ⟨⟨_, e⟩⟩, e.elim)
 
 theorem mul_add (a b c : ordinal) : a * (b + c) = a * b + a * c :=
 quotient.induction_on₃ a b c $ λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩,
-quotient.sound ⟨⟨equiv.sum_prod_distrib _ _ _, λ a b,
-begin
-  split; intro H,
-  { cases H with _ _ _ _ H1 bc _ _ H1,
-    { cases H1; constructor; left; assumption },
-    { cases bc; constructor; right; assumption } },
-  { rcases a with ⟨a₁|a₁,a₂⟩; rcases b with ⟨b₁|b₁,b₂⟩;
-    cases H with _ _ H1 _ _ H1 _ _ H1,
-    { cases H1,
-      { left, constructor, assumption },
-      { right, assumption } },
-    { left, constructor },
-    { cases H1,
-      { left, constructor, assumption },
-      { right, assumption} } }
+quotient.sound ⟨⟨equiv.sum_prod_distrib _ _ _, begin
+  rintro ⟨a₁|a₁, a₂⟩ ⟨b₁|b₁, b₂⟩; simp only [prod.lex_def,
+    sum.lex_inl_inl, sum.lex.sep, sum.lex_inr_inl, sum.lex_inr_inr,
+    equiv.sum_prod_distrib_apply_left, equiv.sum_prod_distrib_apply_right];
+  simp only [sum.inl.inj_iff, true_or, false_and, false_or]
 end⟩⟩
 
 @[simp] theorem mul_add_one (a b : ordinal) : a * (b + 1) = a * b + a :=
@@ -1518,13 +1500,10 @@ end
 theorem mul_le_mul {a b c d : ordinal} (h₁ : a ≤ c) (h₂ : b ≤ d) : a * b ≤ c * d :=
 le_trans (mul_le_mul_left _ h₂) (mul_le_mul_right _ h₁)
 
-theorem mul_le_of_limit {a b c : ordinal.{u}}
-  (h : is_limit b) : a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c :=
-⟨λ h b' l, le_trans (mul_le_mul_left _ (le_of_lt l)) h,
-λ H, le_of_not_lt $
-induction_on a (λ α r _, induction_on b $ λ β s _ h H l, begin
-try_for 300 {
-  resetI,
+private lemma mul_le_of_limit_aux {α β r s} [is_well_order α r] [is_well_order β s]
+  {c} (h : is_limit (type s)) (H : ∀ b' < type s, type r * b' ≤ c)
+  (l : c < type r * type s) : false :=
+begin
   suffices : ∀ a b, prod.lex s r (b, a) (enum _ _ l),
   { cases enum _ _ l with b a, exact irrefl _ (this _ _) },
   intros a b,
@@ -1536,9 +1515,7 @@ try_for 300 {
   refine lt_of_le_of_lt _ this,
   refine (type_le'.2 _),
   constructor,
-}, try_for 800 {
   refine order_embedding.of_monotone (λ a, _) (λ a b, _),
-},
   { rcases a with ⟨⟨b', a'⟩, h⟩,
     by_cases e : b = b',
     { refine sum.inr ⟨a', _⟩,
@@ -1556,7 +1533,13 @@ try_for 300 {
       cases h₂; [exact asymm h h₂_h, exact e₂ rfl] },
     { simp only [e₂, dif_pos, eq_self_iff_true, dif_neg e₁, not_false_iff, sum.lex.sep] },
     { simpa only [dif_neg e₁, dif_neg e₂, prod.lex_def, subrel_val, subtype.mk_eq_mk, sum.lex_inl_inl] using h } }
-end) h H⟩
+end
+
+theorem mul_le_of_limit {a b c : ordinal.{u}}
+  (h : is_limit b) : a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c :=
+⟨λ h b' l, le_trans (mul_le_mul_left _ (le_of_lt l)) h,
+λ H, le_of_not_lt $ induction_on a (λ α r _, induction_on b $ λ β s _,
+  by exactI mul_le_of_limit_aux) h H⟩
 
 theorem mul_is_normal {a : ordinal} (h : 0 < a) : is_normal ((*) a) :=
 ⟨λ b, by rw mul_succ; simpa only [add_zero] using (add_lt_add_iff_left (a*b)).2 h,
@@ -2769,8 +2752,7 @@ def aleph_idx.order_iso : @order_iso cardinal.{u} ordinal.{u} (<) (<) :=
 end
 
 @[simp] theorem aleph_idx.order_iso_coe :
-  (aleph_idx.order_iso : cardinal → ordinal) = aleph_idx :=
-rfl
+  (aleph_idx.order_iso : cardinal → ordinal) = aleph_idx := rfl
 
 @[simp] theorem type_cardinal : @ordinal.type cardinal (<) _ = ordinal.univ.{u (u+1)} :=
 by rw ordinal.univ_id; exact quotient.sound ⟨aleph_idx.order_iso⟩