From c1aff1b5c52b7996d69da2d2522cd696d811ed06 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 18 Apr 2019 22:33:17 -0400
Subject: [PATCH] style(tactic/omega): whitespace and minor tweaks

missed the PR review cycle
---
 src/data/list/basic.lean           | 174 ++++++++++++++---------------
 src/tactic/omega/coeffs.lean       |  78 ++++++-------
 src/tactic/omega/eq_elim.lean      |  98 ++++++++--------
 src/tactic/omega/find_ees.lean     |  10 +-
 src/tactic/omega/int/dnf.lean      |  28 ++---
 src/tactic/omega/int/form.lean     |  12 +-
 src/tactic/omega/int/main.lean     |  70 ++++++------
 src/tactic/omega/int/preterm.lean  |  12 +-
 src/tactic/omega/misc.lean         |   8 +-
 src/tactic/omega/nat/dnf.lean      |  26 ++---
 src/tactic/omega/nat/form.lean     |  78 ++++++-------
 src/tactic/omega/nat/main.lean     | 146 ++++++++++++------------
 src/tactic/omega/nat/neg_elim.lean |  52 ++++-----
 src/tactic/omega/nat/preterm.lean  | 104 ++++++++---------
 src/tactic/omega/nat/sub_elim.lean |  30 ++---
 src/tactic/omega/term.lean         |  18 ++-
 test/omega.lean                    |  14 +--
 17 files changed, 481 insertions(+), 477 deletions(-)

diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index 50efb93086f8c..0bebfbc161f3d 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -4517,10 +4517,10 @@ end choose
 
 namespace func
 
-variables {a : α} 
+variables {a : α}
 variables {as as1 as2 as3 : list α}
 
-local notation as `{` m `↦` a `}` := set a as m
+local notation as ` {` m ` ↦ ` a `}` := set a as m
 
 /- set -/
 
@@ -4531,8 +4531,8 @@ lemma length_set [inhabited α] : ∀ {m : ℕ} {as : list α},
 | (m+1) []      := by simp only [set, nat.zero_max, length, @length_set m]
 | (m+1) (a::as) := by simp only [set, nat.max_succ_succ, length, @length_set m]
 
-@[simp] lemma get_nil [inhabited α] {k : ℕ} : get k [] = default α := 
-by {cases k; refl} 
+@[simp] lemma get_nil [inhabited α] {k : ℕ} : get k [] = default α :=
+by {cases k; refl}
 
 lemma get_eq_default_of_le [inhabited α] :
   ∀ (k : ℕ) {as : list α}, as.length ≤ k → get k as = default α
@@ -4548,7 +4548,7 @@ lemma get_eq_default_of_le [inhabited α] :
 @[simp] lemma get_set [inhabited α] {a : α} :
   ∀ {k : ℕ} {as : list α}, get k (as {k ↦ a}) = a
 | 0 as     := by {cases as; refl, }
-| (k+1) as := by {cases as; simp [get_set]} 
+| (k+1) as := by {cases as; simp [get_set]}
 
 lemma eq_get_of_mem [inhabited α] {a : α} :
   ∀ {as : list α}, a ∈ as → ∃ n : nat, ∀ d : α, a = (get n as)
@@ -4588,7 +4588,7 @@ lemma get_set_eq_of_ne [inhabited α] {a : α} :
   ∀ {as : list α} (k : ℕ) (m : ℕ),
   m ≠ k → get m (as {k ↦ a}) = get m as
 | as 0 m h1 :=
-  by { cases m, contradiction, cases as; 
+  by { cases m, contradiction, cases as;
        simp only [set, get, get_nil] }
 | as (k+1) m h1 :=
   begin
@@ -4599,36 +4599,36 @@ lemma get_set_eq_of_ne [inhabited α] {a : α} :
         intro hc, apply h1, simp [hc] },
       apply h3 },
     simp only [set, get],
-    { apply get_set_eq_of_ne k m, 
+    { apply get_set_eq_of_ne k m,
       intro hc, apply h1, simp [hc], }
   end
 
-lemma get_map [inhabited α] [inhabited β] {f : α → β} : 
-  ∀ {n : ℕ} {as : list α}, n < as.length → 
+lemma get_map [inhabited α] [inhabited β] {f : α → β} :
+  ∀ {n : ℕ} {as : list α}, n < as.length →
   get n (as.map f) = f (get n as)
 | _ [] h := by cases h
 | 0 (a::as) h := rfl
 | (n+1) (a::as) h1 :=
   begin
-    have h2 : n < length as, 
-    { rw [← nat.succ_le_iff, ← nat.lt_succ_iff], 
+    have h2 : n < length as,
+    { rw [← nat.succ_le_iff, ← nat.lt_succ_iff],
       apply h1 },
     apply get_map h2,
   end
 
-lemma get_map' [inhabited α] [inhabited β] 
+lemma get_map' [inhabited α] [inhabited β]
   {f : α → β} {n : ℕ} {as : list α} :
-  f (default α) = (default β) → 
+  f (default α) = (default β) →
   get n (as.map f) = f (get n as) :=
 begin
   intro h1, by_cases h2 : n < as.length,
   { apply get_map h2, },
   { rw not_lt at h2,
-    rw [get_eq_default_of_le _ h2, get_eq_default_of_le, h1], 
+    rw [get_eq_default_of_le _ h2, get_eq_default_of_le, h1],
     rw [length_map], apply h2 }
 end
 
-lemma forall_val_of_forall_mem [inhabited α] 
+lemma forall_val_of_forall_mem [inhabited α]
   {as : list α} {p : α → Prop} :
   p (default α) → (∀ x ∈ as, p x) → (∀ n, p (get n as)) :=
 begin
@@ -4643,93 +4643,93 @@ end
 
 lemma equiv_refl [inhabited α] : equiv as as := λ k, rfl
 
-lemma equiv_symm [inhabited α] : equiv as1 as2 → equiv as2 as1 := 
+lemma equiv_symm [inhabited α] : equiv as1 as2 → equiv as2 as1 :=
 λ h1 k, (h1 k).symm
 
 lemma equiv_trans [inhabited α] :
   equiv as1 as2 → equiv as2 as3 → equiv as1 as3 :=
 λ h1 h2 k, eq.trans (h1 k) (h2 k)
 
-lemma equiv_of_eq [inhabited α] : as1 = as2 → equiv as1 as2 := 
+lemma equiv_of_eq [inhabited α] : as1 = as2 → equiv as1 as2 :=
 begin intro h1, rw h1, apply equiv_refl end
 
 lemma eq_of_equiv [inhabited α] :
-  ∀ {as1 as2 : list α}, as1.length = as2.length → 
-  equiv as1 as2 → as1 = as2 
+  ∀ {as1 as2 : list α}, as1.length = as2.length →
+  equiv as1 as2 → as1 = as2
 | []     [] h1 h2 := rfl
 | (_::_) [] h1 h2 := by cases h1
 | [] (_::_) h1 h2 := by cases h1
-| (a1::as1) (a2::as2) h1 h2 := 
+| (a1::as1) (a2::as2) h1 h2 :=
   begin
     congr,
     { apply h2 0 },
-    have h3 : as1.length = as2.length, 
+    have h3 : as1.length = as2.length,
     { simpa [add_left_inj, add_comm, length] using h1 },
     apply eq_of_equiv h3,
-    intro m, apply h2 (m+1) 
+    intro m, apply h2 (m+1)
   end
 
 /- neg -/
 
-@[simp] lemma get_neg [inhabited α] [add_group α] 
+@[simp] lemma get_neg [inhabited α] [add_group α]
   {k : ℕ} {as : list α} : @get α ⟨0⟩ k (neg as) = -(@get α ⟨0⟩ k as) :=
 by {unfold neg, rw (@get_map' α α ⟨0⟩), apply neg_zero}
 
-@[simp] lemma length_neg 
-  [inhabited α] [has_neg α] (as : list α) : 
-  (neg as).length = as.length := 
+@[simp] lemma length_neg
+  [inhabited α] [has_neg α] (as : list α) :
+  (neg as).length = as.length :=
 by simp only [neg, length_map]
 
 /- pointwise -/
 
-lemma nil_pointwise [inhabited α] [inhabited β] {f : α → β → γ} : 
-  ∀ bs : list β, pointwise f [] bs = bs.map (f $ default α) 
+lemma nil_pointwise [inhabited α] [inhabited β] {f : α → β → γ} :
+  ∀ bs : list β, pointwise f [] bs = bs.map (f $ default α)
 | []      := rfl
-| (b::bs) := 
-  by simp only [nil_pointwise bs, pointwise, 
-     eq_self_iff_true, and_self, map] 
+| (b::bs) :=
+  by simp only [nil_pointwise bs, pointwise,
+     eq_self_iff_true, and_self, map]
 
-lemma pointwise_nil [inhabited α] [inhabited β] {f : α → β → γ} : 
-  ∀ as : list α, pointwise f as [] = as.map (λ a, f a $ default β) 
+lemma pointwise_nil [inhabited α] [inhabited β] {f : α → β → γ} :
+  ∀ as : list α, pointwise f as [] = as.map (λ a, f a $ default β)
 | []      := rfl
-| (a::as) := 
-  by simp only [pointwise_nil as, pointwise, 
-     eq_self_iff_true, and_self, list.map] 
-
-lemma get_pointwise [inhabited α] [inhabited β] [inhabited γ] 
-  {f : α → β → γ} (h1 : f (default α) (default β) = default γ) : 
-  ∀ (k : nat) (as : list α) (bs : list β), 
-  get k (pointwise f as bs) = f (get k as) (get k bs) 
+| (a::as) :=
+  by simp only [pointwise_nil as, pointwise,
+     eq_self_iff_true, and_self, list.map]
+
+lemma get_pointwise [inhabited α] [inhabited β] [inhabited γ]
+  {f : α → β → γ} (h1 : f (default α) (default β) = default γ) :
+  ∀ (k : nat) (as : list α) (bs : list β),
+  get k (pointwise f as bs) = f (get k as) (get k bs)
 | k [] [] := by simp only [h1, get_nil, pointwise, get]
-| 0 [] (b::bs) := 
-  by simp only [get_pointwise, get_nil, 
-      pointwise, get, nat.nat_zero_eq_zero, map] 
-| (k+1) [] (b::bs) := 
+| 0 [] (b::bs) :=
+  by simp only [get_pointwise, get_nil,
+      pointwise, get, nat.nat_zero_eq_zero, map]
+| (k+1) [] (b::bs) :=
   by { have : get k (map (f $ default α) bs) = f (default α) (get k bs),
        { simpa [nil_pointwise, get_nil] using (get_pointwise k [] bs) },
        simpa [get, get_nil, pointwise, map] }
-| 0 (a::as) [] := 
-  by simp only [get_pointwise, get_nil, 
-     pointwise, get, nat.nat_zero_eq_zero, map] 
-| (k+1) (a::as) [] := 
-  by simpa [get, get_nil, pointwise, map, pointwise_nil, get_nil] 
+| 0 (a::as) [] :=
+  by simp only [get_pointwise, get_nil,
+     pointwise, get, nat.nat_zero_eq_zero, map]
+| (k+1) (a::as) [] :=
+  by simpa [get, get_nil, pointwise, map, pointwise_nil, get_nil]
      using get_pointwise k as []
-| 0 (a::as) (b::bs) := by simp only [pointwise, get] 
-| (k+1) (a::as) (b::bs) := 
-  by simp only [pointwise, get, get_pointwise k] 
+| 0 (a::as) (b::bs) := by simp only [pointwise, get]
+| (k+1) (a::as) (b::bs) :=
+  by simp only [pointwise, get, get_pointwise k]
 
-lemma length_pointwise [inhabited α] [inhabited β] {f : α → β → γ} : 
-  ∀ {as : list α} {bs : list β}, 
-  (pointwise f as bs).length = _root_.max as.length bs.length 
+lemma length_pointwise [inhabited α] [inhabited β] {f : α → β → γ} :
+  ∀ {as : list α} {bs : list β},
+  (pointwise f as bs).length = _root_.max as.length bs.length
 | []      []      := rfl
-| []      (b::bs) := 
+| []      (b::bs) :=
   by simp only [pointwise, length, length_map,
      max_eq_right (nat.zero_le (length bs + 1))]
-| (a::as) []      := 
+| (a::as) []      :=
   by simp only [pointwise, length, length_map,
      max_eq_left (nat.zero_le (length as + 1))]
 | (a::as) (b::bs) :=
-  by simp only [pointwise, length, 
+  by simp only [pointwise, length,
      nat.max_succ_succ, @length_pointwise as bs]
 
 /- add -/
@@ -4738,27 +4738,27 @@ lemma length_pointwise [inhabited α] [inhabited β] {f : α → β → γ} :
   @get α ⟨0⟩ k (add xs ys) = ( @get α ⟨0⟩ k xs + @get α ⟨0⟩ k ys) :=
 by {apply get_pointwise, apply zero_add}
 
-@[simp] lemma length_add {α : Type u} 
-  [has_zero α] [has_add α] {xs ys : list α} : 
-  (add xs ys).length = _root_.max xs.length ys.length := 
+@[simp] lemma length_add {α : Type u}
+  [has_zero α] [has_add α] {xs ys : list α} :
+  (add xs ys).length = _root_.max xs.length ys.length :=
 @length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
 
-@[simp] lemma nil_add {α : Type u} [add_monoid α] 
-  (as : list α) : add [] as = as := 
+@[simp] lemma nil_add {α : Type u} [add_monoid α]
+  (as : list α) : add [] as = as :=
 begin
   rw [add, @nil_pointwise α α α ⟨0⟩ ⟨0⟩],
-  apply eq.trans _ (map_id as), 
-  congr, ext, 
+  apply eq.trans _ (map_id as),
+  congr, ext,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, zero_add], refl
 end
 
-@[simp] lemma add_nil {α : Type u} [add_monoid α] 
-  (as : list α) : add as [] = as := 
+@[simp] lemma add_nil {α : Type u} [add_monoid α]
+  (as : list α) : add as [] = as :=
 begin
-  rw [add, @pointwise_nil α α α ⟨0⟩ ⟨0⟩], 
-  apply eq.trans _ (map_id as), 
-  congr, ext, 
+  rw [add, @pointwise_nil α α α ⟨0⟩ ⟨0⟩],
+  apply eq.trans _ (map_id as),
+  congr, ext,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, add_zero], refl
 end
@@ -4768,10 +4768,10 @@ lemma map_add_map {α : Type u} [add_monoid α] (f g : α → α) {as : list α}
 begin
   apply @eq_of_equiv _ (⟨0⟩ : inhabited α),
   { rw [length_map, length_add, max_eq_left, length_map],
-    apply le_of_eq, 
+    apply le_of_eq,
     rw [length_map, length_map] },
-  intros m, 
-  rw [get_add], 
+  intros m,
+  rw [get_add],
   by_cases h : m < length as,
   { repeat {rw [@get_map α α ⟨0⟩ ⟨0⟩ _ _ _ h]} },
   rw not_lt at h,
@@ -4782,30 +4782,30 @@ end
 
 /- sub -/
 
-@[simp] lemma get_sub {α : Type u} 
+@[simp] lemma get_sub {α : Type u}
   [add_group α] {k : ℕ} {xs ys : list α} :
   @get α ⟨0⟩ k (sub xs ys) = (@get α ⟨0⟩ k xs - @get α ⟨0⟩ k ys) :=
 by {apply get_pointwise, apply sub_zero}
 
-@[simp] lemma length_sub [has_zero α] [has_sub α] {xs ys : list α} : 
-  (sub xs ys).length = _root_.max xs.length ys.length := 
+@[simp] lemma length_sub [has_zero α] [has_sub α] {xs ys : list α} :
+  (sub xs ys).length = _root_.max xs.length ys.length :=
 @length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
 
-@[simp] lemma nil_sub {α : Type} [add_group α] 
-  (as : list α) : sub [] as = @neg α ⟨0⟩ _ as := 
+@[simp] lemma nil_sub {α : Type} [add_group α]
+  (as : list α) : sub [] as = @neg α ⟨0⟩ _ as :=
 begin
-  rw [sub, nil_pointwise], 
-  congr, ext, 
+  rw [sub, nil_pointwise],
+  congr, ext,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, zero_sub]
 end
 
-@[simp] lemma sub_nil {α : Type} [add_group α] 
-  (as : list α) : sub as [] = as := 
+@[simp] lemma sub_nil {α : Type} [add_group α]
+  (as : list α) : sub as [] = as :=
 begin
-  rw [sub, pointwise_nil], 
-  apply eq.trans _ (map_id as), 
-  congr, ext, 
+  rw [sub, pointwise_nil],
+  apply eq.trans _ (map_id as),
+  congr, ext,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, sub_zero], refl
 end
@@ -4816,4 +4816,4 @@ end list
 
 theorem option.to_list_nodup {α} : ∀ o : option α, o.to_list.nodup
 | none     := list.nodup_nil
-| (some x) := list.nodup_singleton x
\ No newline at end of file
+| (some x) := list.nodup_singleton x
diff --git a/src/tactic/omega/coeffs.lean b/src/tactic/omega/coeffs.lean
index 42f2b2f63a885..a76b0515188ea 100644
--- a/src/tactic/omega/coeffs.lean
+++ b/src/tactic/omega/coeffs.lean
@@ -11,7 +11,7 @@ import data.list.basic
 import tactic.ring
 import tactic.omega.misc
 
-namespace omega 
+namespace omega
 namespace coeffs
 
 open list.func
@@ -25,8 +25,8 @@ variable {v : nat → int}
 @[simp] lemma val_between_nil {l : nat} :
   ∀ m, val_between v [] l m = 0
 | 0     := by simp only [val_between]
-| (m+1) := 
-  by simp only [val_between_nil m, omega.coeffs.val_between, 
+| (m+1) :=
+  by simp only [val_between_nil m, omega.coeffs.val_between,
      get_nil, zero_add, zero_mul, int.default_eq_zero]
 
 def val (v : nat → int) (as : list int) : int :=
@@ -45,8 +45,8 @@ lemma val_between_eq_of_le {as : list int} {l : nat} :
     { rw [h1, add_comm l, nat.add_sub_cancel] },
     have h2 :  list.length as ≤ l + m,
     { rw ← nat.lt_succ_iff, apply h1 },
-    simpa [ get_eq_default_of_le _ h2, zero_mul, add_zero, 
-      val_between ] using val_between_eq_of_le _ h2 
+    simpa [ get_eq_default_of_le _ h2, zero_mul, add_zero,
+      val_between ] using val_between_eq_of_le _ h2
   end
 
 lemma val_eq_of_le {as : list int} {k : nat} :
@@ -76,7 +76,7 @@ lemma val_between_eq_val_between
     apply nat.le_add_right
   end
 
-local notation as `{` m `↦` a `}` := set a as m
+local notation as ` {` m ` ↦ ` a `}` := set a as m
 
 def val_between_set {a : int} {l n : nat} :
   ∀ {m}, l ≤ n → n < l + m → val_between v ([] {n ↦ a}) l m = a * v n
@@ -85,7 +85,7 @@ def val_between_set {a : int} {l n : nat} :
 | (m+1) h1 h2 :=
   begin
     rw [← add_assoc, nat.lt_succ_iff, le_iff_eq_or_lt] at h2,
-    cases h2; unfold val_between, 
+    cases h2; unfold val_between,
     { have h3 : val_between v ([] {l + m ↦ a}) l m = 0,
       { apply @eq.trans _ _ (val_between v [] l m),
         { apply val_between_eq_val_between,
@@ -99,7 +99,7 @@ def val_between_set {a : int} {l n : nat} :
     { have h3 : l + m ≠ n,
       { apply ne_of_gt h2 },
       rw [@val_between_set m h1 h2, get_set_eq_of_ne _ _ h3],
-      simp only [h3, get_nil, add_zero, zero_mul, int.default_eq_zero] } 
+      simp only [h3, get_nil, add_zero, zero_mul, int.default_eq_zero] }
   end
 
 @[simp] def val_set {m : nat} {a : int} :
@@ -117,22 +117,22 @@ lemma val_between_neg {as : list int} {l : nat} :
   begin
     unfold val_between,
     rw [neg_add, neg_mul_eq_neg_mul],
-    apply fun_mono_2, 
+    apply fun_mono_2,
     apply val_between_neg,
     apply fun_mono_2 _ rfl,
     apply get_neg
   end
 
 @[simp] lemma val_neg {as : list int} :
-   val v (neg as) = -(val v as) := 
+   val v (neg as) = -(val v as) :=
 by simpa only [val, length_neg] using val_between_neg
 
 lemma val_between_add {is js : list int} {l : nat} :
   ∀ m, val_between v (add is js) l m =
   (val_between v is l m) + (val_between v js l m)
 | 0     := rfl
-| (m+1) := 
-  by { simp only [val_between, val_between_add m, 
+| (m+1) :=
+  by { simp only [val_between, val_between_add m,
       list.func.get, get_add], ring }
 
 @[simp] lemma val_add {is js : list int} :
@@ -149,19 +149,19 @@ lemma val_between_sub {is js : list int} {l : nat} :
   ∀ m, val_between v (sub is js) l m =
   (val_between v is l m) - (val_between v js l m)
 | 0 := rfl
-| (m+1) := 
-  by { simp only [val_between, val_between_sub m, 
+| (m+1) :=
+  by { simp only [val_between, val_between_sub m,
       list.func.get, get_sub], ring }
 
 @[simp] lemma val_sub {is js : list int} :
   val v (sub is js) = (val v is) - (val v js) :=
 begin
   unfold val,
-  rw val_between_sub, 
+  rw val_between_sub,
   apply fun_mono_2;
   apply val_between_eq_of_le;
   rw [zero_add, length_sub],
-  apply le_max_left, 
+  apply le_max_left,
   apply le_max_right
 end
 
@@ -175,29 +175,29 @@ lemma val_except_eq_val_except
 begin
   intros h1 h2, unfold val_except,
   apply fun_mono_2,
-  { apply val_between_eq_val_between; 
+  { apply val_between_eq_val_between;
     intros x h3 h4;
-    [ {apply h1}, {apply h2} ]; 
+    [ {apply h1}, {apply h2} ];
     apply ne_of_lt;
-    rw zero_add at h4; 
+    rw zero_add at h4;
     apply h4 },
   { repeat { rw ← val_between_eq_of_le
       ((max is.length js.length) - (k+1)) },
-    { apply val_between_eq_val_between; 
+    { apply val_between_eq_val_between;
       intros x h3 h4;
-      [ {apply h1}, {apply h2} ]; 
+      [ {apply h1}, {apply h2} ];
       apply ne.symm;
-      apply ne_of_lt; 
-      rw nat.lt_iff_add_one_le; 
+      apply ne_of_lt;
+      rw nat.lt_iff_add_one_le;
       exact h3 },
-    repeat { rw add_comm, 
+    repeat { rw add_comm,
              apply le_trans _ (nat.le_sub_add _ _),
             { apply le_max_right <|> apply le_max_left } } }
 end
 
-local notation v `⟨` m `↦` a `⟩` := update m a v
+local notation v ` ⟨` m ` ↦ ` a `⟩` := update m a v
 
-lemma val_except_update_set 
+lemma val_except_update_set
   {n : nat} {as : list int} {i j : int} :
   val_except n (v⟨n ↦ i⟩) (as {n ↦ j}) = val_except n v as :=
 by apply val_except_eq_val_except update_eq_of_ne (get_set_eq_of_ne _)
@@ -208,10 +208,10 @@ lemma val_between_add_val_between {as : list int} {l m : nat} :
 | 0 := by simp only [val_between, add_zero]
 | (n+1) :=
   begin
-    rw ← add_assoc, 
+    rw ← add_assoc,
     unfold val_between,
     rw add_assoc,
-    rw ← @val_between_add_val_between n, 
+    rw ← @val_between_add_val_between n,
     ring,
   end
 
@@ -229,11 +229,11 @@ begin
   have h2 : (list.length as - (n + 1)) = 0,
   { apply nat.sub_eq_zero_of_le
     (le_trans h1 (nat.le_add_right _ _)) },
-  have h3 : val_between v as 0 (list.length as) = 
-            val_between v as 0 (n + 1), 
-  { simpa only [val] using @val_eq_of_le v as (n+1) 
+  have h3 : val_between v as 0 (list.length as) =
+            val_between v as 0 (n + 1),
+  { simpa only [val] using @val_eq_of_le v as (n+1)
       (le_trans h1 (nat.le_add_right _ _)) },
-  simp only [add_zero, val_between, zero_add, h2, h3] 
+  simp only [add_zero, val_between, zero_add, h2, h3]
 end
 
 @[simp] lemma val_between_map_mul {i : int} {as: list int} {l : nat} :
@@ -241,20 +241,20 @@ end
 | 0     := by simp only [val_between, mul_zero, list.map]
 | (m+1) :=
   begin
-    unfold val_between, 
+    unfold val_between,
     rw [@val_between_map_mul m, mul_add],
     apply fun_mono_2 rfl,
     by_cases h1 : l + m < as.length,
     { rw [get_map h1, mul_assoc] },
     rw not_lt at h1,
     rw [get_eq_default_of_le, get_eq_default_of_le];
-    try {simp}; apply h1 
+    try {simp}; apply h1
   end
 
 lemma forall_val_dvd_of_forall_mem_dvd {i : int} {as : list int} :
   (∀ x ∈ as, i ∣ x) → (∀ n, i ∣ get n as) | h1 n :=
 by { apply forall_val_of_forall_mem _ h1,
-     apply dvd_zero } 
+     apply dvd_zero }
 
 lemma dvd_val_between {i} {as: list int} {l : nat} :
   ∀ {m}, (∀ x ∈ as, i ∣ x) → (i ∣ val_between v as l m)
@@ -267,26 +267,26 @@ lemma dvd_val_between {i} {as: list int} {l : nat} :
     apply dvd_mul_of_dvd_left,
     by_cases h2 : get (l+m) as = 0,
     { rw h2, apply dvd_zero },
-    apply h1, apply mem_get_of_ne_zero h2 
+    apply h1, apply mem_get_of_ne_zero h2
   end
 
 lemma dvd_val {as : list int} {i : int} :
   (∀ x ∈ as, i ∣ x) → (i ∣ val v as) := by apply dvd_val_between
 
-@[simp] lemma val_between_map_div 
+@[simp] lemma val_between_map_div
   {as: list int} {i : int} {l : nat} (h1 : ∀ x ∈ as, i ∣ x) :
   ∀ {m}, val_between v (list.map (λ x, x / i) as) l m = (val_between v as l m) / i
 | 0     := by simp only [int.zero_div, val_between, list.map]
 | (m+1) :=
   begin
-    unfold val_between, 
+    unfold val_between,
     rw [@val_between_map_div m, int.add_div_of_dvd (dvd_val_between h1)],
     apply fun_mono_2 rfl,
     { apply calc get (l + m) (list.map (λ (x : ℤ), x / i) as) * v (l + m)
           = ((get (l + m) as) / i) * v (l + m) :
             begin
               apply fun_mono_2 _ rfl,
-              rw get_map', 
+              rw get_map',
               apply int.zero_div
             end
       ... =  get (l + m) as * v (l + m) / i :
diff --git a/src/tactic/omega/eq_elim.lean b/src/tactic/omega/eq_elim.lean
index 53447a3f7104e..f25ca36c1f6b1 100644
--- a/src/tactic/omega/eq_elim.lean
+++ b/src/tactic/omega/eq_elim.lean
@@ -9,7 +9,7 @@ See 5.5 of http://www.decision-procedures.org/ for details.
 
 import tactic.omega.clause
 
-open list.func 
+open list.func
 
 namespace omega
 
@@ -29,10 +29,10 @@ begin
   intro h1,
   unfold symmod,
   rw [int.mod_eq_of_lt (le_of_lt h1) (lt_add_one _), if_neg],
-  simp only [add_comm, add_neg_cancel_left, 
+  simp only [add_comm, add_neg_cancel_left,
     neg_add_rev, sub_eq_add_neg],
   have h2 : 2 * i = (1 + 1) * i := rfl,
-  simpa only [h2, add_mul, one_mul, 
+  simpa only [h2, add_mul, one_mul,
     add_lt_add_iff_left, not_lt] using h1
 end
 
@@ -52,7 +52,7 @@ lemma symmod_eq {i j : int} :
   symmod i j = i - j * (symdiv i j) :=
 by rw [mul_symdiv_eq, sub_sub_cancel]
 
-/- (sgm v b as n) is the new value assigned to the nth variable 
+/- (sgm v b as n) is the new value assigned to the nth variable
    after a single step of equality elimination using valuation v,
    term ⟨b, as⟩, and variable index n. If v satisfies the initial
    constraint set, then (v ⟨n ↦ sgm v b as n⟩) satisfies the new
@@ -62,7 +62,7 @@ let a_n : int := get n as in
 let m : int := a_n + 1 in
 ((symmod b m) + (coeffs.val v (as.map (λ x, symmod x m)))) / m
 
-local notation as `{` m `↦` a `}` := set a as m
+local notation as ` {` m ` ↦ ` a `}` := set a as m
 
 def rhs : nat → int → list int → term
 | n b as :=
@@ -73,28 +73,28 @@ lemma rhs_correct_aux {v : nat → int} {m : int} {as : list int} :
 ∀ {k}, ∃ d, (m * d +
   coeffs.val_between v (as.map (λ (x : ℤ), symmod x m)) 0 k =
       coeffs.val_between v as 0 k)
-| 0 := 
-  begin 
-    existsi (0 : int), 
+| 0 :=
+  begin
+    existsi (0 : int),
     simp only [add_zero, mul_zero, coeffs.val_between]
   end
 | (k+1) :=
   begin
-    simp only [zero_add, coeffs.val_between, list.map], 
+    simp only [zero_add, coeffs.val_between, list.map],
     cases @rhs_correct_aux k with d h1, rw ← h1,
     by_cases hk : k < as.length,
     { rw [get_map hk, symmod_eq, sub_mul],
-      existsi (d + (symdiv (get k as) m * v k)), 
+      existsi (d + (symdiv (get k as) m * v k)),
       ring },
     { rw not_lt at hk,
       repeat {rw get_eq_default_of_le},
-      existsi d, 
-      rw add_assoc, 
+      existsi d,
+      rw add_assoc,
       exact hk,
       simp only [hk, list.length_map] }
   end
 
-local notation v `⟨` m `↦` a `⟩` := update m a v
+local notation v ` ⟨` m ` ↦ ` a `⟩` := update m a v
 
 lemma rhs_correct {v : nat → int}
   {b : int} {as : list int} (n : nat) :
@@ -119,7 +119,7 @@ begin
       cases h5 with d h5, rw symmod_eq,
       existsi (symdiv b m + d),
       unfold term.val, rw ← h5,
-      simp only [term.val, mul_add, add_mul, m, a_n], 
+      simp only [term.val, mul_add, add_mul, m, a_n],
       ring },
     cases h4 with c h4,
     rw [dvd_add_iff_right (dvd_mul_right m c), h4, ← h1],
@@ -133,9 +133,9 @@ begin
           { by_contra hc, rw not_lt at hc,
             rw (get_eq_default_of_le n hc) at h0,
             cases h0 },
-          rw get_map hn, 
+          rw get_map hn,
           simp only [a_n, m],
-          rw [add_comm, symmod_add_one_self h0], 
+          rw [add_comm, symmod_add_one_self h0],
           ring
         end
   ... = term.val (v⟨n↦sgm v b as n⟩) (rhs n b as) :
@@ -143,8 +143,8 @@ begin
           unfold rhs, unfold term.val,
           rw [← coeffs.val_except_add_eq n, get_set, update_eq],
           have h2 : ∀ a b c : int, a + b + c = b + (c + a) := by {intros, ring},
-          rw (h2 (- _)), 
-          apply fun_mono_2 rfl, 
+          rw (h2 (- _)),
+          apply fun_mono_2 rfl,
           apply fun_mono_2,
           { rw coeffs.val_except_update_set },
           { simp only [m, a_n], ring }
@@ -169,8 +169,8 @@ begin
   intros h1 h2,
   let a_n := get n as,
   let m := a_n + 1,
-  have h3 : m ≠ 0, 
-  { apply ne_of_gt, 
+  have h3 : m ≠ 0,
+  { apply ne_of_gt,
     apply lt_trans h1,
     simp only [m, lt_add_iff_pos_right] },
   have h4 : 0 = (term.val (v⟨n↦sgm v b as n⟩) (coeffs_reduce n b as)) * m :=
@@ -183,13 +183,13 @@ begin
           rw [← coeffs.val_except_add_eq n, rhs_correct n h1 h2],
           simp only [a_n, add_assoc],
         end
-  ... = -(m * a_n * sgm v b as n) + (b + a_n * (symmod b m)) + 
-        (coeffs.val_except n v as + 
+  ... = -(m * a_n * sgm v b as n) + (b + a_n * (symmod b m)) +
+        (coeffs.val_except n v as +
         a_n * coeffs.val_except n v (as.map (λ x, symmod x m))) :
           begin
             simp only [term.val, rhs, mul_add, m, a_n,
               add_assoc, add_left_inj, add_comm, add_left_comm],
-            rw [← coeffs.val_except_add_eq n, 
+            rw [← coeffs.val_except_add_eq n,
               get_set, update_eq, mul_add],
             apply fun_mono_2,
             { rw coeffs.val_except_eq_val_except
@@ -226,7 +226,7 @@ begin
           rw ← add_assoc,
           have h4 : ∀ (x : ℤ), x + a_n * symmod x m = m * sym_sym m x,
           { intro x, have h5 : a_n = m - 1,
-            { simp only [m], 
+            { simp only [m],
               rw add_sub_cancel },
             rw [h5, sub_mul, one_mul, add_sub,
               add_comm, add_sub_assoc, ← mul_symdiv_eq],
@@ -235,27 +235,27 @@ begin
           apply coeffs.val_except_eq_val_except; intros x h5, refl,
           apply congr_arg,
           apply fun_mono_2 _ rfl,
-          rw function.funext_iff, 
+          rw function.funext_iff,
           apply h4
         end
   ... = (-(a_n * sgm v b as n) + (sym_sym m b)
         + coeffs.val_except n v (as.map (sym_sym m))) * m :
         begin
-          simp only [add_mul _ _ m], 
+          simp only [add_mul _ _ m],
           apply fun_mono_2, ring,
           simp only [coeffs.val_except, add_mul _ _ m],
           apply fun_mono_2,
           { rw [mul_comm _ m, ← coeffs.val_between_map_mul, list.map_map] },
           simp only [list.length_map, mul_comm _ m],
-          rw [← coeffs.val_between_map_mul, list.map_map] 
+          rw [← coeffs.val_between_map_mul, list.map_map]
         end
-  ... = (sym_sym m b + (coeffs.val_except n v (as.map (sym_sym m)) + 
+  ... = (sym_sym m b + (coeffs.val_except n v (as.map (sym_sym m)) +
           (-a_n * sgm v b as n))) * m : by ring
   ... = (term.val (v ⟨n ↦ sgm v b as n⟩) (coeffs_reduce n b as)) * m :
         begin
           simp only [coeffs_reduce, term.val, m, a_n],
-          rw [← coeffs.val_except_add_eq n, 
-            coeffs.val_except_update_set, get_set, update_eq] 
+          rw [← coeffs.val_except_add_eq n,
+            coeffs.val_except_update_set, get_set, update_eq]
         end,
   rw [← int.mul_div_cancel (term.val _ _) h3, ← h4, int.zero_div]
 end
@@ -272,11 +272,11 @@ lemma subst_correct {v : nat → int} {b : int}
   0 < get n as → 0 = term.val v (b,as) →
   term.val v t = term.val (v ⟨n ↦ sgm v b as n⟩) (subst n (rhs n b as) t) :=
 begin
-  intros h1 h2, 
+  intros h1 h2,
   simp only [subst, term.val, term.val_add, term.val_mul],
-  rw ← rhs_correct _ h1 h2, 
+  rw ← rhs_correct _ h1 h2,
   cases t with b' as',
-  simp only [term.val], 
+  simp only [term.val],
   have h3 : coeffs.val (v ⟨n ↦ sgm v b as n⟩) (as' {n ↦ 0}) =
     coeffs.val_except n v as',
   { rw [← coeffs.val_except_add_eq n, get_set,
@@ -356,14 +356,14 @@ lemma sat_eq_elim :
 | (ee.neg::es) ((eq::eqs), les) h1 :=
   begin
     simp only [eq_elim], apply sat_eq_elim,
-    cases h1 with v h1, 
+    cases h1 with v h1,
     existsi v,
-    cases h1 with hl hr, 
+    cases h1 with hl hr,
     apply and.intro _ hr,
     rw list.forall_mem_cons at *,
     apply and.intro _ hl.right,
-    rw term.val_neg, 
-    rw ← hl.left, 
+    rw term.val_neg,
+    rw ← hl.left,
     refl
   end
 | (ee.nondiv i::es) ((b,as)::eqs, les) h1 :=
@@ -375,7 +375,7 @@ lemma sat_eq_elim :
       have h4 : i ∣ coeffs.val v as     := coeffs.dvd_val h2.right,
       have h5 : i ∣ b + coeffs.val v as := by { rw ← h3, apply dvd_zero },
       rw ← dvd_add_iff_left h4 at h5, apply h2.left h5 },
-    rw if_neg h2, apply sat_empty 
+    rw if_neg h2, apply sat_empty
   end
 | (ee.factor i::es) ((b,as)::eqs, les) h1 :=
   begin
@@ -390,18 +390,18 @@ lemma sat_eq_elim :
   end
 | (ee.reduce n::es) ((b,as)::eqs, les) h1 :=
   begin
-    simp only [eq_elim], 
+    simp only [eq_elim],
     by_cases h2 : 0 < get n as,
     tactic.rotate 1,
     { rw if_neg h2, apply sat_empty },
-    rw if_pos h2, 
+    rw if_pos h2,
     apply sat_eq_elim,
     cases h1 with v h1,
-    existsi v ⟨n ↦ sgm v b as n⟩, 
+    existsi v ⟨n ↦ sgm v b as n⟩,
     cases h1 with h1 h3,
-    rw list.forall_mem_cons at h1, 
+    rw list.forall_mem_cons at h1,
     cases h1 with h4 h5,
-    constructor, 
+    constructor,
     { rw list.forall_mem_cons,
       constructor,
       { apply coeffs_reduce_correct h2 h4 },
@@ -414,22 +414,22 @@ lemma sat_eq_elim :
    end
 | (ee.cancel m::es) ((eq::eqs), les) h1 :=
   begin
-    unfold eq_elim, 
+    unfold eq_elim,
     apply sat_eq_elim,
-    cases h1 with v h1, 
-    existsi v, 
+    cases h1 with v h1,
+    existsi v,
     cases h1 with h1 h2,
     rw list.forall_mem_cons at h1, cases h1 with h1 h3,
     constructor; intros t h4; rw list.mem_map at h4;
     rcases h4 with ⟨s,h4,h5⟩; rw ← h5;
     simp only [term.val_add, term.val_mul, cancel];
     rw [← h1, mul_zero, zero_add],
-    { apply h3 _ h4 }, 
+    { apply h3 _ h4 },
     { apply h2 _ h4 }
   end
 
 lemma unsat_of_unsat_eq_elim (ee : list ee) (c : clause) :
   (eq_elim ee c).unsat → c.unsat :=
-by {intros h1 h2, apply h1, apply sat_eq_elim h2} 
+by {intros h1 h2, apply h1, apply sat_eq_elim h2}
 
-end omega
\ No newline at end of file
+end omega
diff --git a/src/tactic/omega/find_ees.lean b/src/tactic/omega/find_ees.lean
index 631fb1c55613c..8b4af497338e3 100644
--- a/src/tactic/omega/find_ees.lean
+++ b/src/tactic/omega/find_ees.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
 
-A tactic for finding a sequence of equality 
+A tactic for finding a sequence of equality
 elimination rules for a given set of constraints.
 -/
 
@@ -15,7 +15,7 @@ open tactic
 
 namespace omega
 
-meta structure ee_state :=
+structure ee_state :=
 (eqs : list term)
 (les : list term)
 (ees : list ee)
@@ -95,9 +95,7 @@ t ← head_eq,
 i ← get_gcd t,
     factor i t !>>= (set_eqs [] >> add_ee (ee.nondiv i)) ;
 λ s, find_min_coeff s !>>= add_ee ee.drop ;
-λ x, let i : int := x.fst in
-     let n : nat := x.snd.fst in
-     let u : term := x.snd.snd in
+λ ⟨i, n, u⟩,
 if i = 1
 then do eqs ← get_eqs,
         les ← get_les,
@@ -119,4 +117,4 @@ elim_eq !>>= get_ees ; λ _, elim_eqs
 meta def find_ees : clause → tactic (list ee)
 | (eqs,les) := run eqs les elim_eqs
 
-end omega
\ No newline at end of file
+end omega
diff --git a/src/tactic/omega/int/dnf.lean b/src/tactic/omega/int/dnf.lean
index 8936251272d8b..6042952439f8a 100644
--- a/src/tactic/omega/int/dnf.lean
+++ b/src/tactic/omega/int/dnf.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
 
-DNF transformation. 
+DNF transformation.
 -/
 
 import tactic.omega.clause
@@ -12,11 +12,11 @@ import tactic.omega.int.form
 namespace omega
 namespace int
 
-local notation x `=*` y := form.eq x y
-local notation x `≤*` y := form.le x y
-local notation `¬*` p   := form.not p
-local notation p `∨*` q := form.or p q
-local notation p `∧*` q := form.and p q
+local notation x ` =* ` y := form.eq x y
+local notation x ` ≤* ` y := form.le x y
+local notation `¬* ` p   := form.not p
+local notation p ` ∨* ` q := form.or p q
+local notation p ` ∧* ` q := form.and p q
 
 @[simp] def push_neg : form → form
 | (p ∨* q) := (push_neg p) ∧* (push_neg q)
@@ -108,14 +108,14 @@ begin
   form.induce `[intros v h, try {apply h}],
   { cases p with t s t s; try {apply h},
     { simp only [le_and_le_iff_eq.symm,
-        classical.not_and_distrib, not_le, 
+        classical.not_and_distrib, not_le,
         preterm.val, form.holds] at h,
-      simp only [int.add_one_le_iff, preterm.add_one, 
+      simp only [int.add_one_le_iff, preterm.add_one,
         preterm.val, form.holds, neg_elim],
       rw or_comm, assumption },
-    { simp only [not_le, int.add_one_le_iff, 
-        preterm.add_one, not_le, preterm.val, 
-        form.holds, neg_elim] at *, 
+    { simp only [not_le, int.add_one_le_iff,
+        preterm.add_one, not_le, preterm.val,
+        form.holds, neg_elim] at *,
       assumption} },
   { simp only [neg_elim], cases h; [{left, apply ihp},
     {right, apply ihq}]; assumption },
@@ -140,7 +140,7 @@ begin
   form.induce `[intros h1 h2],
   { apply list.exists_mem_cons_of, constructor,
     { simp only [preterm.val, form.holds] at h2,
-      rw [list.forall_mem_singleton], 
+      rw [list.forall_mem_singleton],
       simp only [h2, omega.int.val_canonize,
         omega.term.val_sub, sub_self] },
     { apply list.forall_mem_nil } },
@@ -148,7 +148,7 @@ begin
     { apply list.forall_mem_nil },
     { simp only [preterm.val, form.holds] at h2 ,
       rw [list.forall_mem_singleton],
-      simp only [val_canonize, 
+      simp only [val_canonize,
         preterm.val, term.val_sub],
       rw [le_sub, sub_zero], assumption } },
     { cases h1 },
@@ -163,7 +163,7 @@ begin
       refine ⟨clause.append cp cq, ⟨_, clause.holds_append hp2 hq2⟩⟩,
       simp only [dnf_core, list.mem_map],
       refine ⟨(cp,cq),⟨_,rfl⟩⟩,
-      rw list.mem_product, 
+      rw list.mem_product,
       constructor; assumption }
 end
 
diff --git a/src/tactic/omega/int/form.lean b/src/tactic/omega/int/form.lean
index 7cc3607adfe34..808351d3b79de 100644
--- a/src/tactic/omega/int/form.lean
+++ b/src/tactic/omega/int/form.lean
@@ -19,11 +19,11 @@ inductive form
 | or  : form → form → form
 | and : form → form → form
 
-local notation x `=*` y := form.eq x y
-local notation x `≤*` y := form.le x y
-local notation `¬*` p   := form.not p
-local notation p `∨*` q := form.or p q
-local notation p `∧*` q := form.and p q
+local notation x ` =* ` y := form.eq x y
+local notation x ` ≤* ` y := form.le x y
+local notation `¬* ` p   := form.not p
+local notation p ` ∨* ` q := form.or p q
+local notation p ` ∧* ` q := form.and p q
 
 namespace form
 
@@ -81,7 +81,7 @@ def repr : form → string
 | (t =* s) := "(" ++ t.repr ++ " = " ++ s.repr ++ ")"
 | (t ≤* s) := "(" ++ t.repr ++ " ≤ " ++ s.repr ++ ")"
 | (¬* p)   := "¬" ++ p.repr
-| (p ∨* q) := "(" ++ p.repr ++ " ∨  " ++ q.repr ++ ")"
+| (p ∨* q) := "(" ++ p.repr ++ " ∨ " ++ q.repr ++ ")"
 | (p ∧* q) := "(" ++ p.repr ++ " ∧ " ++ q.repr ++ ")"
 
 instance has_repr : has_repr form := ⟨repr⟩
diff --git a/src/tactic/omega/int/main.lean b/src/tactic/omega/int/main.lean
index 375728c43bae0..636373b490d04 100644
--- a/src/tactic/omega/int/main.lean
+++ b/src/tactic/omega/int/main.lean
@@ -14,19 +14,19 @@ open tactic
 namespace omega
 namespace int
 
-local notation x `=*` y := form.eq x y
-local notation x `≤*` y := form.le x y
-local notation `¬*` p   := form.not p
-local notation p `∨*` q := form.or p q
-local notation p `∧*` q := form.and p q
+local notation x ` =* ` y := form.eq x y
+local notation x ` ≤* ` y := form.le x y
+local notation `¬* ` p   := form.not p
+local notation p ` ∨* ` q := form.or p q
+local notation p ` ∧* ` q := form.and p q
 
 run_cmd mk_simp_attr `sugar
-attribute [sugar] 
+attribute [sugar]
   not_le not_lt
   int.lt_iff_add_one_le
   or_false false_or
   and_true true_and
-  ge gt mul_add add_mul 
+  ge gt mul_add add_mul
   mul_comm sub_eq_add_neg
   classical.imp_iff_not_or
   classical.iff_iff_not_or_and_or_not
@@ -34,65 +34,65 @@ attribute [sugar]
 meta def desugar := `[try {simp only with sugar}]
 
 lemma univ_close_of_unsat_clausify (m : nat) (p : form) :
-  clauses.unsat (dnf (¬* p)) → univ_close p (λ x, 0) m | h1 := 
+  clauses.unsat (dnf (¬* p)) → univ_close p (λ x, 0) m | h1 :=
 begin
   apply univ_close_of_valid,
   apply valid_of_unsat_not,
   apply unsat_of_clauses_unsat,
-  exact h1 
+  exact h1
 end
 
 /- Given a (p : form), return the expr of a (t : univ_close m p) -/
-meta def prove_univ_close (m : nat) (p : form) : tactic expr :=  
-do x ← prove_unsats (dnf (¬*p)), 
+meta def prove_univ_close (m : nat) (p : form) : tactic expr :=
+do x ← prove_unsats (dnf (¬*p)),
    return `(univ_close_of_unsat_clausify %%`(m) %%`(p) %%x)
 
-meta def to_preterm : expr → tactic preterm 
+meta def to_preterm : expr → tactic preterm
 | (expr.var k) := return (preterm.var 1 k)
 | `(-%%(expr.var k)) := return (preterm.var (-1 : int) k)
-| `(%%(expr.var k) * %%zx) := 
-  do z ← eval_expr int zx, 
+| `(%%(expr.var k) * %%zx) :=
+  do z ← eval_expr int zx,
      return (preterm.var z k)
-| `(%%t1x + %%t2x) := 
-  do t1 ← to_preterm t1x, 
-     t2 ← to_preterm t2x, 
+| `(%%t1x + %%t2x) :=
+  do t1 ← to_preterm t1x,
+     t2 ← to_preterm t2x,
      return (preterm.add t1 t2)
-| zx := 
+| zx :=
   do z ← eval_expr int zx,
      return (preterm.cst z)
 
-meta def to_form_core : expr → tactic form 
-| `(%%tx1 = %%tx2) := 
-  do t1 ← to_preterm tx1, 
-     t2 ← to_preterm tx2, 
+meta def to_form_core : expr → tactic form
+| `(%%tx1 = %%tx2) :=
+  do t1 ← to_preterm tx1,
+     t2 ← to_preterm tx2,
      return (t1 =* t2)
-| `(%%tx1 ≤ %%tx2) := 
-  do t1 ← to_preterm tx1, 
-     t2 ← to_preterm tx2, 
+| `(%%tx1 ≤ %%tx2) :=
+  do t1 ← to_preterm tx1,
+     t2 ← to_preterm tx2,
      return (t1 ≤* t2)
 | `(¬ %%px) := do p ← to_form_core px, return (¬* p)
-| `(%%px ∨ %%qx) := 
-  do p ← to_form_core px, 
-     q ← to_form_core qx, 
+| `(%%px ∨ %%qx) :=
+  do p ← to_form_core px,
+     q ← to_form_core qx,
      return (p ∨* q)
-| `(%%px ∧ %%qx) := 
-  do p ← to_form_core px, 
-     q ← to_form_core qx, 
+| `(%%px ∧ %%qx) :=
+  do p ← to_form_core px,
+     q ← to_form_core qx,
      return (p ∧* q)
 | _ := failed
 
-meta def to_form : nat → expr → tactic (form × nat) 
+meta def to_form : nat → expr → tactic (form × nat)
 | m `(_ → %%px) := to_form (m+1) px
 | m x := do p ← to_form_core x, return (p,m)
 
 meta def prove_lia : tactic expr :=
 do (p,m) ← target >>= to_form 0,
-   prove_univ_close m p 
+   prove_univ_close m p
 
 end int
 end omega
 
 open omega.int
 
-meta def omega_int : tactic unit := 
-desugar >> prove_lia >>= apply >> skip
\ No newline at end of file
+meta def omega_int : tactic unit :=
+desugar >> prove_lia >>= apply >> skip
diff --git a/src/tactic/omega/int/preterm.lean b/src/tactic/omega/int/preterm.lean
index 47b2fa23de4c9..12373415538f4 100644
--- a/src/tactic/omega/int/preterm.lean
+++ b/src/tactic/omega/int/preterm.lean
@@ -18,7 +18,7 @@ inductive preterm : Type
 | add : preterm → preterm → preterm
 
 local notation `&` k    := preterm.cst k
-local infix `**`  : 300 := preterm.var
+local infix ` ** ` : 300 := preterm.var
 local notation t `+*` s := preterm.add t s
 
 namespace preterm
@@ -47,7 +47,7 @@ def repr : preterm → string
 
 end preterm
 
-local notation as `{` m `↦` a `}` := list.func.set a as m
+local notation as ` {` m ` ↦ ` a `}` := list.func.set a as m
 
 @[simp] def canonize : preterm → term
 | (& i)      := ⟨i, []⟩
@@ -56,19 +56,19 @@ local notation as `{` m `↦` a `}` := list.func.set a as m
 
 @[simp] lemma val_canonize {v : nat → int} :
   ∀ {t : preterm}, (canonize t).val v = t.val v
-| (& i) := 
+| (& i) :=
   by simp only [preterm.val, add_zero, term.val, canonize, coeffs.val_nil]
 | (i ** n)   :=
   begin
-    simp only [coeffs.val_set, canonize, 
+    simp only [coeffs.val_set, canonize,
       preterm.val, zero_add, term.val],
     split_ifs with h1 h2,
     { simp only [one_mul, h1] },
     { simp only [neg_mul_eq_neg_mul_symm, one_mul, h2] },
     { rw mul_comm }
   end
-| (t +* s) := 
-  by simp only [canonize, val_canonize, 
+| (t +* s) :=
+  by simp only [canonize, val_canonize,
      term.val_add, preterm.val]
 
 end int
diff --git a/src/tactic/omega/misc.lean b/src/tactic/omega/misc.lean
index 8a0818c20a3ca..a2ed98da5b452 100644
--- a/src/tactic/omega/misc.lean
+++ b/src/tactic/omega/misc.lean
@@ -6,7 +6,7 @@ Author: Seul Baek
 Miscellaneous.
 -/
 
-variables {α β γ : Type} 
+variables {α β γ : Type}
 
 namespace omega
 
@@ -25,17 +25,17 @@ lemma pred_mono_2' {c : Prop → Prop → Prop} {a1 a2 b1 b2 : Prop} :
 def update (m : nat) (a : α) (v : nat → α) : nat → α
 | n := if n = m then a else v n
 
-local notation v `⟨` m `↦` a `⟩` := update m a v
+local notation v ` ⟨` m ` ↦ ` a `⟩` := update m a v
 
 lemma update_eq (m : nat) (a : α) (v : nat → α) : (v ⟨m ↦ a⟩) m = a :=
 by simp only [update, if_pos rfl]
 
 lemma update_eq_of_ne {m : nat} {a : α} {v : nat → α} (k : nat) :
   k ≠ m → update m a v k = v k :=
-by {intro h1, unfold update, rw if_neg h1} 
+by {intro h1, unfold update, rw if_neg h1}
 
 def update_zero (a : α) (v : nat → α) : nat → α
 | 0     := a
 | (k+1) := v k
 
-end omega 
\ No newline at end of file
+end omega
diff --git a/src/tactic/omega/nat/dnf.lean b/src/tactic/omega/nat/dnf.lean
index 9efd227e10336..b3a49ab3d5bfa 100644
--- a/src/tactic/omega/nat/dnf.lean
+++ b/src/tactic/omega/nat/dnf.lean
@@ -12,11 +12,11 @@ import tactic.omega.nat.sub_elim
 namespace omega
 namespace nat
 
-local notation x `=*` y := form.eq x y
-local notation x `≤*` y := form.le x y
-local notation `¬*` p   := form.not p
-local notation p `∨*` q := form.or p q
-local notation p `∧*` q := form.and p q
+local notation x ` =* ` y := form.eq x y
+local notation x ` ≤* ` y := form.le x y
+local notation `¬* ` p   := form.not p
+local notation p ` ∨* ` q := form.or p q
+local notation p ` ∧* ` q := form.and p q
 
 @[simp] def dnf_core : form → list clause
 | (p ∨* q) := (dnf_core p) ++ (dnf_core q)
@@ -35,17 +35,17 @@ begin
   form.induce `[intros h1 h0 h2],
   { apply list.exists_mem_cons_of,
     constructor, rw list.forall_mem_singleton,
-    cases h0 with ht hs, 
-    simp only [val_canonize ht, val_canonize hs, 
+    cases h0 with ht hs,
+    simp only [val_canonize ht, val_canonize hs,
       term.val_sub, form.holds, sub_eq_add_neg] at *,
     rw [h2, add_neg_self], apply list.forall_mem_nil },
   { apply list.exists_mem_cons_of,
-    constructor, 
+    constructor,
     apply list.forall_mem_nil,
     rw list.forall_mem_singleton,
     simp only [val_canonize (h0.left), val_canonize (h0.right),
       term.val_sub, form.holds, sub_eq_add_neg] at *,
-    rw [←sub_eq_add_neg, le_sub, sub_zero, int.coe_nat_le], 
+    rw [←sub_eq_add_neg, le_sub, sub_zero, int.coe_nat_le],
     assumption },
   { cases h1 },
   { cases h2 with h2 h2;
@@ -59,7 +59,7 @@ begin
     refine ⟨clause.append cp cq, ⟨_, clause.holds_append hp2 hq2⟩⟩,
     simp only [dnf_core, list.mem_map],
     refine ⟨(cp,cq),⟨_,rfl⟩⟩,
-    rw list.mem_product, 
+    rw list.mem_product,
     constructor; assumption }
 end
 
@@ -78,7 +78,7 @@ def terms.vars : list term → list bool
 | []      := []
 | (t::ts) := bools.or (term.vars t) (terms.vars ts)
 
-local notation as `{` m `↦` a `}` := list.func.set a as m
+local notation as ` {` m ` ↦ ` a `}` := list.func.set a as m
 
 def nonneg_consts_core : nat → list bool → list term
 | _ [] := []
@@ -104,9 +104,9 @@ lemma holds_nonneg_consts_core {v : nat → int} (h1 : ∀ x, 0 ≤ v x) :
 | k (tt::bs) :=
   begin
     simp only [nonneg_consts_core],
-    rw list.forall_mem_cons, 
+    rw list.forall_mem_cons,
     constructor,
-    { simp only [term.val, one_mul, zero_add, coeffs.val_set], 
+    { simp only [term.val, one_mul, zero_add, coeffs.val_set],
       apply h1 },
     { apply holds_nonneg_consts_core (k+1) bs }
   end
diff --git a/src/tactic/omega/nat/form.lean b/src/tactic/omega/nat/form.lean
index 18f8ddac6355e..ec0fce316a43e 100644
--- a/src/tactic/omega/nat/form.lean
+++ b/src/tactic/omega/nat/form.lean
@@ -6,29 +6,29 @@ Author: Seul Baek
 Linear natural number arithmetic formulas in pre-normalized form.
 -/
 
-import tactic.omega.nat.preterm 
+import tactic.omega.nat.preterm
 
 namespace omega
 
-namespace nat 
+namespace nat
 
 @[derive has_reflect]
-inductive form 
+inductive form
 | eq  : preterm → preterm → form
 | le  : preterm → preterm → form
 | not : form → form
 | or  : form → form → form
 | and : form → form → form
 
-local notation x `=*` y := form.eq x y
-local notation x `≤*` y := form.le x y
-local notation `¬*` p   := form.not p
-local notation p `∨*` q := form.or p q
-local notation p `∧*` q := form.and p q
+local notation x ` =* ` y := form.eq x y
+local notation x ` ≤* ` y := form.le x y
+local notation `¬* ` p   := form.not p
+local notation p ` ∨* ` q := form.or p q
+local notation p ` ∧* ` q := form.and p q
 
 namespace form
 
-@[simp] def holds (v : nat → nat) : form → Prop 
+@[simp] def holds (v : nat → nat) : form → Prop
 | (t =* s) := t.val v = s.val v
 | (t ≤* s) := t.val v ≤ s.val v
 | (¬* p)   := ¬ p.holds
@@ -37,27 +37,27 @@ namespace form
 
 end form
 
-@[simp] def univ_close (p : form) : (nat → nat) → nat → Prop 
+@[simp] def univ_close (p : form) : (nat → nat) → nat → Prop
 | v 0     := p.holds v
-| v (k+1) := ∀ i : nat, univ_close (update_zero i v) k 
+| v (k+1) := ∀ i : nat, univ_close (update_zero i v) k
 
 namespace form
 
-def neg_free : form → Prop 
+def neg_free : form → Prop
 | (t =* s) := true
 | (t ≤* s) := true
 | (p ∨* q) := neg_free p ∧ neg_free q
 | (p ∧* q) := neg_free p ∧ neg_free q
 | _        := false
 
-def sub_free : form → Prop 
+def sub_free : form → Prop
 | (t =* s) := t.sub_free ∧ s.sub_free
 | (t ≤* s) := t.sub_free ∧ s.sub_free
 | (¬* p)   := p.sub_free
 | (p ∨* q) := p.sub_free ∧ q.sub_free
 | (p ∧* q) := p.sub_free ∧ q.sub_free
 
-def fresh_index : form → nat 
+def fresh_index : form → nat
 | (t =* s) := max t.fresh_index s.fresh_index
 | (t ≤* s) := max t.fresh_index s.fresh_index
 | (¬* p)   := p.fresh_index
@@ -65,18 +65,18 @@ def fresh_index : form → nat
 | (p ∧* q) := max p.fresh_index q.fresh_index
 
 def holds_constant {v w : nat → nat} :
-  ∀ p : form, 
-  ( (∀ x < p.fresh_index, v x = w x) → 
-    (p.holds v ↔ p.holds w) ) 
-| (t =* s) h1 := 
+  ∀ p : form,
+  ( (∀ x < p.fresh_index, v x = w x) →
+    (p.holds v ↔ p.holds w) )
+| (t =* s) h1 :=
   begin
-    simp only [holds], 
+    simp only [holds],
     apply pred_mono_2;
     apply preterm.val_constant;
     intros x h2; apply h1 _ (lt_of_lt_of_le h2 _),
     apply le_max_left, apply le_max_right
   end
-| (t ≤* s) h1 := 
+| (t ≤* s) h1 :=
   begin
     simp only [holds],
     apply pred_mono_2;
@@ -84,38 +84,38 @@ def holds_constant {v w : nat → nat} :
     intros x h2; apply h1 _ (lt_of_lt_of_le h2 _),
     apply le_max_left, apply le_max_right
   end
-| (¬* p)   h1 := 
+| (¬* p)   h1 :=
   begin
     apply not_iff_not_of_iff,
     apply holds_constant p h1
   end
-| (p ∨* q) h1 := 
+| (p ∨* q) h1 :=
   begin
-    simp only [holds], 
+    simp only [holds],
     apply pred_mono_2';
     apply holds_constant;
     intros x h2; apply h1 _ (lt_of_lt_of_le h2 _),
     apply le_max_left, apply le_max_right
   end
-| (p ∧* q) h1 := 
+| (p ∧* q) h1 :=
   begin
-    simp only [holds], 
+    simp only [holds],
     apply pred_mono_2';
     apply holds_constant;
     intros x h2; apply h1 _ (lt_of_lt_of_le h2 _),
     apply le_max_left, apply le_max_right
   end
 
-def valid (p : form) : Prop := 
+def valid (p : form) : Prop :=
 ∀ v, holds v p
 
-def sat (p : form) : Prop := 
+def sat (p : form) : Prop :=
 ∃ v, holds v p
 
-def implies (p q : form) : Prop := 
+def implies (p q : form) : Prop :=
 ∀ v, (holds v p → holds v q)
 
-def equiv (p q : form) : Prop := 
+def equiv (p q : form) : Prop :=
 ∀ v, (holds v p ↔ holds v q)
 
 lemma sat_of_implies_of_sat {p q : form} :
@@ -134,32 +134,32 @@ end
 
 def unsat (p : form) : Prop := ¬ sat p
 
-def repr : form → string 
+def repr : form → string
 | (t =* s) := "(" ++ t.repr ++ " = " ++ s.repr ++ ")"
 | (t ≤* s) := "(" ++ t.repr ++ " ≤ " ++ s.repr ++ ")"
 | (¬* p)   := "¬" ++ p.repr
-| (p ∨* q) := "(" ++ p.repr ++ " ∨  " ++ q.repr ++ ")"
+| (p ∨* q) := "(" ++ p.repr ++ " ∨ " ++ q.repr ++ ")"
 | (p ∧* q) := "(" ++ p.repr ++ " ∧ " ++ q.repr ++ ")"
 
-instance has_repr : has_repr form := ⟨repr⟩ 
-meta instance has_to_format : has_to_format form := ⟨λ x, x.repr⟩ 
+instance has_repr : has_repr form := ⟨repr⟩
+meta instance has_to_format : has_to_format form := ⟨λ x, x.repr⟩
 
 end form
 
-lemma univ_close_of_valid {p : form} : 
+lemma univ_close_of_valid {p : form} :
   ∀ {m : nat} {v : nat → nat}, p.valid → univ_close p v m
-| 0 v h1     := h1 _ 
+| 0 v h1     := h1 _
 | (m+1) v h1 := λ i, univ_close_of_valid h1
 
-lemma valid_of_unsat_not {p : form} : (¬*p).unsat → p.valid := 
+lemma valid_of_unsat_not {p : form} : (¬*p).unsat → p.valid :=
 begin
-  simp only [form.sat, form.unsat, form.valid, form.holds], 
+  simp only [form.sat, form.unsat, form.valid, form.holds],
   rw classical.not_exists_not, intro h, assumption
 end
 
-meta def form.induce (t : tactic unit := tactic.skip) : tactic unit := 
+meta def form.induce (t : tactic unit := tactic.skip) : tactic unit :=
 `[ intro p, induction p with t s t s p ih p q ihp ihq p q ihp ihq; t ]
 
 end nat
 
-end omega
\ No newline at end of file
+end omega
diff --git a/src/tactic/omega/nat/main.lean b/src/tactic/omega/nat/main.lean
index f0db5f2468347..1e127e238be58 100644
--- a/src/tactic/omega/nat/main.lean
+++ b/src/tactic/omega/nat/main.lean
@@ -10,25 +10,25 @@ import tactic.omega.prove_unsats
 import tactic.omega.nat.dnf
 import tactic.omega.nat.neg_elim
 
-open tactic 
+open tactic
 
 namespace omega
 namespace nat
 
 local notation `&` k    := preterm.cst k
-local infix `**`  : 300 := preterm.var 
-local notation t `+*` s := preterm.add t s
-local notation t `-*` s := preterm.sub t s
-
-local notation x `=*` y := form.eq x y
-local notation x `≤*` y := form.le x y
-local notation `¬*` p   := form.not p
-local notation p `∨*` q := form.or p q
-local notation p `∧*` q := form.and p q
-
-   
-run_cmd mk_simp_attr `sugar_nat 
-attribute [sugar_nat] 
+local infix ` ** ` : 300 := preterm.var
+local notation t ` +* ` s := preterm.add t s
+local notation t ` -* ` s := preterm.sub t s
+
+local notation x ` =* ` y := form.eq x y
+local notation x ` ≤* ` y := form.le x y
+local notation `¬* ` p   := form.not p
+local notation p ` ∨* ` q := form.or p q
+local notation p ` ∧* ` q := form.and p q
+
+
+run_cmd mk_simp_attr `sugar_nat
+attribute [sugar_nat]
   not_le not_lt
   nat.lt_iff_add_one_le
   nat.succ_eq_add_one
@@ -41,64 +41,64 @@ attribute [sugar_nat]
 meta def desugar := `[try {simp only with sugar_nat}]
 
 lemma univ_close_of_unsat_neg_elim_not (m) (p : form) :
-  (neg_elim (¬* p)).unsat → univ_close p (λ _, 0) m :=  
+  (neg_elim (¬* p)).unsat → univ_close p (λ _, 0) m :=
 begin
   intro h1, apply univ_close_of_valid,
   apply valid_of_unsat_not, intro h2, apply h1,
   apply form.sat_of_implies_of_sat implies_neg_elim h2,
 end
 
-meta def preterm.prove_sub_free : preterm → tactic expr 
+meta def preterm.prove_sub_free : preterm → tactic expr
 | (& m)    := return `(trivial)
 | (m ** n) := return `(trivial)
-| (t +* s) := 
+| (t +* s) :=
   do x ← preterm.prove_sub_free t,
      y ← preterm.prove_sub_free s,
-     return `(@and.intro (preterm.sub_free %%`(t)) 
-       (preterm.sub_free %%`(s)) %%x %%y) 
+     return `(@and.intro (preterm.sub_free %%`(t))
+       (preterm.sub_free %%`(s)) %%x %%y)
 | (_ -* _) := failed
 
-meta def prove_neg_free : form → tactic expr 
+meta def prove_neg_free : form → tactic expr
 | (t =* s) := return `(trivial)
 | (t ≤* s) := return `(trivial)
-| (p ∨* q) := 
+| (p ∨* q) :=
   do x ← prove_neg_free p,
      y ← prove_neg_free q,
-     return `(@and.intro (form.neg_free %%`(p)) 
-       (form.neg_free %%`(q)) %%x %%y) 
-| (p ∧* q) := 
+     return `(@and.intro (form.neg_free %%`(p))
+       (form.neg_free %%`(q)) %%x %%y)
+| (p ∧* q) :=
   do x ← prove_neg_free p,
      y ← prove_neg_free q,
-     return `(@and.intro (form.neg_free %%`(p)) 
-       (form.neg_free %%`(q)) %%x %%y) 
+     return `(@and.intro (form.neg_free %%`(p))
+       (form.neg_free %%`(q)) %%x %%y)
 | _        := failed
 
-meta def prove_sub_free : form → tactic expr 
-| (t =* s) := 
+meta def prove_sub_free : form → tactic expr
+| (t =* s) :=
   do x ← preterm.prove_sub_free t,
      y ← preterm.prove_sub_free s,
-     return `(@and.intro (preterm.sub_free %%`(t)) 
-       (preterm.sub_free %%`(s)) %%x %%y) 
-| (t ≤* s) := 
+     return `(@and.intro (preterm.sub_free %%`(t))
+       (preterm.sub_free %%`(s)) %%x %%y)
+| (t ≤* s) :=
   do x ← preterm.prove_sub_free t,
      y ← preterm.prove_sub_free s,
-     return `(@and.intro (preterm.sub_free %%`(t)) 
-       (preterm.sub_free %%`(s)) %%x %%y) 
+     return `(@and.intro (preterm.sub_free %%`(t))
+       (preterm.sub_free %%`(s)) %%x %%y)
 | (¬*p) := prove_sub_free p
-| (p ∨* q) := 
+| (p ∨* q) :=
   do x ← prove_sub_free p,
      y ← prove_sub_free q,
-     return `(@and.intro (form.sub_free %%`(p)) 
-       (form.sub_free %%`(q)) %%x %%y) 
-| (p ∧* q) := 
+     return `(@and.intro (form.sub_free %%`(p))
+       (form.sub_free %%`(q)) %%x %%y)
+| (p ∧* q) :=
   do x ← prove_sub_free p,
      y ← prove_sub_free q,
-     return `(@and.intro (form.sub_free %%`(p)) 
-       (form.sub_free %%`(q)) %%x %%y) 
+     return `(@and.intro (form.sub_free %%`(p))
+       (form.sub_free %%`(q)) %%x %%y)
 
 /- Given a p : form, return the expr of a term t : p.unsat,
    where p is subtraction- and negation-free. -/
-meta def prove_unsat_sub_free (p : form) : tactic expr :=  
+meta def prove_unsat_sub_free (p : form) : tactic expr :=
 do x ← prove_neg_free p,
    y ← prove_sub_free p,
    z ← prove_unsats (dnf p),
@@ -106,65 +106,65 @@ do x ← prove_neg_free p,
 
 /- Given a p : form, return the expr of a term t : p.unsat,
    where p is negation-free. -/
-meta def prove_unsat_neg_free : form → tactic expr | p := 
-match p.sub_terms with 
+meta def prove_unsat_neg_free : form → tactic expr | p :=
+match p.sub_terms with
 | none         := prove_unsat_sub_free p
-| (some (t,s)) := 
-  do x ← prove_unsat_neg_free (sub_elim t s p), 
+| (some (t,s)) :=
+  do x ← prove_unsat_neg_free (sub_elim t s p),
      return `(unsat_of_unsat_sub_elim %%`(t) %%`(s) %%`(p) %%x)
 end
 
-/- Given a (m : nat) and (p : form), 
+/- Given a (m : nat) and (p : form),
    return the expr of (t : univ_close m p) -/
-meta def prove_univ_close (m : nat) (p : form) : tactic expr := 
-do x ← prove_unsat_neg_free (neg_elim (¬*p)), 
+meta def prove_univ_close (m : nat) (p : form) : tactic expr :=
+do x ← prove_unsat_neg_free (neg_elim (¬*p)),
    to_expr ``(univ_close_of_unsat_neg_elim_not %%`(m) %%`(p) %%x)
 
-meta def to_preterm : expr → tactic preterm 
+meta def to_preterm : expr → tactic preterm
 | (expr.var k) := return (preterm.var 1 k)
-| `(%%(expr.var k) * %%mx) := 
-  do m ← eval_expr nat mx, 
+| `(%%(expr.var k) * %%mx) :=
+  do m ← eval_expr nat mx,
      return (preterm.var m k)
-| `(%%t1x + %%t2x) := 
-  do t1 ← to_preterm t1x, 
-     t2 ← to_preterm t2x, 
+| `(%%t1x + %%t2x) :=
+  do t1 ← to_preterm t1x,
+     t2 ← to_preterm t2x,
      return (preterm.add t1 t2)
-| `(%%t1x - %%t2x) := 
-  do t1 ← to_preterm t1x, 
-     t2 ← to_preterm t2x, 
+| `(%%t1x - %%t2x) :=
+  do t1 ← to_preterm t1x,
+     t2 ← to_preterm t2x,
      return (preterm.sub t1 t2)
-| mx := 
+| mx :=
   do m ← eval_expr nat mx,
      return (preterm.cst m)
 
-meta def to_form_core : expr → tactic form 
-| `(%%tx1 = %%tx2) := 
-  do t1 ← to_preterm tx1, 
-     t2 ← to_preterm tx2, 
+meta def to_form_core : expr → tactic form
+| `(%%tx1 = %%tx2) :=
+  do t1 ← to_preterm tx1,
+     t2 ← to_preterm tx2,
      return (t1 =* t2)
-| `(%%tx1 ≤ %%tx2) := 
-  do t1 ← to_preterm tx1, 
-     t2 ← to_preterm tx2, 
+| `(%%tx1 ≤ %%tx2) :=
+  do t1 ← to_preterm tx1,
+     t2 ← to_preterm tx2,
      return (t1 ≤* t2)
 | `(¬ %%px) := do p ← to_form_core px, return (¬* p)
-| `(%%px ∨ %%qx) := 
-  do p ← to_form_core px, 
-     q ← to_form_core qx, 
+| `(%%px ∨ %%qx) :=
+  do p ← to_form_core px,
+     q ← to_form_core qx,
      return (p ∨* q)
-| `(%%px ∧ %%qx) := 
-  do p ← to_form_core px, 
-     q ← to_form_core qx, 
+| `(%%px ∧ %%qx) :=
+  do p ← to_form_core px,
+     q ← to_form_core qx,
      return (p ∧* q)
 | `(_ → %%px) := to_form_core px
 | _ := failed
 
-meta def to_form : nat → expr → tactic (form × nat) 
+meta def to_form : nat → expr → tactic (form × nat)
 | m `(_ → %%px) := to_form (m+1) px
 | m x := do p ← to_form_core x, return (p,m)
 
 meta def prove_lna : tactic expr :=
 do (p,m) ← target >>= to_form 0,
-   prove_univ_close m p 
+   prove_univ_close m p
 
 end nat
 end omega
@@ -172,4 +172,4 @@ end omega
 open omega.nat
 
 meta def omega_nat : tactic unit :=
-desugar >> prove_lna >>= apply >> skip
\ No newline at end of file
+desugar >> prove_lna >>= apply >> skip
diff --git a/src/tactic/omega/nat/neg_elim.lean b/src/tactic/omega/nat/neg_elim.lean
index af9eac1f98d9b..206b33915667d 100644
--- a/src/tactic/omega/nat/neg_elim.lean
+++ b/src/tactic/omega/nat/neg_elim.lean
@@ -11,34 +11,34 @@ import tactic.omega.nat.form
 namespace omega
 namespace nat
 
-local notation x `=*` y := form.eq x y
-local notation x `≤*` y := form.le x y
-local notation `¬*` p   := form.not p
-local notation p `∨*` q := form.or p q
-local notation p `∧*` q := form.and p q
+local notation x ` =* ` y := form.eq x y
+local notation x ` ≤* ` y := form.le x y
+local notation `¬* ` p   := form.not p
+local notation p ` ∨* ` q := form.or p q
+local notation p ` ∧* ` q := form.and p q
 
-@[simp] def push_neg : form → form 
+@[simp] def push_neg : form → form
 | (p ∨* q) := (push_neg p) ∧* (push_neg q)
 | (p ∧* q) := (push_neg p) ∨* (push_neg q)
 | (¬*p)    := p
 | p        := ¬* p
 
-lemma push_neg_equiv : 
+lemma push_neg_equiv :
   ∀ {p : form}, form.equiv (push_neg p) (¬* p) :=
 begin
-  form.induce `[intros v; try {refl}], 
+  form.induce `[intros v; try {refl}],
   { simp only [classical.not_not, form.holds, push_neg] },
   { simp only [form.holds, push_neg, not_or_distrib, ihp v, ihq v] },
   { simp only [form.holds, push_neg, classical.not_and_distrib, ihp v, ihq v] }
 end
 
-def nnf : form → form 
+def nnf : form → form
 | (¬* p)   := push_neg (nnf p)
 | (p ∨* q) := (nnf p) ∨* (nnf q)
 | (p ∧* q) := (nnf p) ∧* (nnf q)
 | a        := a
 
-def is_nnf : form → Prop 
+def is_nnf : form → Prop
 | (t =* s) := true
 | (t ≤* s) := true
 | ¬*(t =* s) := true
@@ -55,7 +55,7 @@ begin
   { cases h1, constructor; [{apply ihp}, {apply ihq}]; assumption }
 end
 
-lemma is_nnf_nnf : ∀ p : form, is_nnf (nnf p) := 
+lemma is_nnf_nnf : ∀ p : form, is_nnf (nnf p) :=
 begin
   form.induce `[try {trivial}],
   { apply is_nnf_push_neg _ ih },
@@ -65,21 +65,21 @@ end
 
 lemma nnf_equiv : ∀ {p : form}, form.equiv (nnf p) p :=
 begin
-  form.induce `[intros v; try {refl}; simp only [nnf]], 
+  form.induce `[intros v; try {refl}; simp only [nnf]],
   { rw push_neg_equiv,
     apply not_iff_not_of_iff, apply ih },
   { apply pred_mono_2' (ihp v) (ihq v) },
   { apply pred_mono_2' (ihp v) (ihq v) }
 end
 
-@[simp] def neg_elim_core : form → form 
+@[simp] def neg_elim_core : form → form
 | (¬* (t =* s)) := (t.add_one ≤* s) ∨* (s.add_one ≤* t)
 | (¬* (t ≤* s)) := s.add_one ≤* t
 | (p ∨* q) := (neg_elim_core p) ∨* (neg_elim_core q)
 | (p ∧* q) := (neg_elim_core p) ∧* (neg_elim_core q)
 | p        := p
 
-lemma neg_free_neg_elim_core : ∀ p, is_nnf p → (neg_elim_core p).neg_free := 
+lemma neg_free_neg_elim_core : ∀ p, is_nnf p → (neg_elim_core p).neg_free :=
 begin
   form.induce `[intro h1, try {simp only [neg_free, neg_elim_core]}, try {trivial}],
   { cases p; try {cases h1}; try {trivial},
@@ -88,35 +88,35 @@ begin
   { cases h1, constructor; [{apply ihp}, {apply ihq}]; assumption }
 end
 
-lemma le_and_le_iff_eq {α : Type} [partial_order α] {a b : α} : 
-  (a ≤ b ∧ b ≤ a) ↔ a = b := 
+lemma le_and_le_iff_eq {α : Type} [partial_order α] {a b : α} :
+  (a ≤ b ∧ b ≤ a) ↔ a = b :=
 begin
   constructor; intro h1,
   { cases h1, apply le_antisymm; assumption },
   { constructor; apply le_of_eq; rw h1  }
 end
 
-lemma implies_neg_elim_core : ∀ {p : form}, 
+lemma implies_neg_elim_core : ∀ {p : form},
   form.implies p (neg_elim_core p) :=
 begin
   form.induce `[intros v h, try {apply h}],
   { cases p with t s t s; try {apply h},
-    { have : preterm.val v (preterm.add_one t) ≤ preterm.val v s ∨ 
+    { have : preterm.val v (preterm.add_one t) ≤ preterm.val v s ∨
              preterm.val v (preterm.add_one s) ≤ preterm.val v t,
-      { rw or.comm, 
-        simpa only [form.holds, le_and_le_iff_eq.symm, 
+      { rw or.comm,
+        simpa only [form.holds, le_and_le_iff_eq.symm,
           classical.not_and_distrib, not_le] using h },
       simpa only [form.holds, neg_elim_core, int.add_one_le_iff] },
     simpa only [form.holds, not_le, int.add_one_le_iff] using h },
-  { simp only [neg_elim_core], cases h; 
-    [{left, apply ihp}, {right, apply ihq}]; 
-    assumption }, 
-  apply and.imp (ihp _) (ihq _) h 
+  { simp only [neg_elim_core], cases h;
+    [{left, apply ihp}, {right, apply ihq}];
+    assumption },
+  apply and.imp (ihp _) (ihq _) h
 end
 
 def neg_elim : form → form := neg_elim_core ∘ nnf
 
-lemma neg_free_neg_elim {p : form} : (neg_elim p).neg_free := 
+lemma neg_free_neg_elim {p : form} : (neg_elim p).neg_free :=
 neg_free_neg_elim_core _ (is_nnf_nnf _)
 
 lemma implies_neg_elim {p : form} : form.implies p (neg_elim p) :=
@@ -127,4 +127,4 @@ end
 
 end nat
 
-end omega
\ No newline at end of file
+end omega
diff --git a/src/tactic/omega/nat/preterm.lean b/src/tactic/omega/nat/preterm.lean
index 45c73eb3a8b14..3deb73d633840 100644
--- a/src/tactic/omega/nat/preterm.lean
+++ b/src/tactic/omega/nat/preterm.lean
@@ -11,33 +11,33 @@ import tactic.omega.term
 open tactic
 
 namespace omega
-namespace nat 
+namespace nat
 
 @[derive has_reflect, derive decidable_eq]
 inductive preterm : Type
-| cst : nat → preterm 
+| cst : nat → preterm
 | var : nat → nat → preterm
-| add : preterm → preterm → preterm 
-| sub : preterm → preterm → preterm 
+| add : preterm → preterm → preterm
+| sub : preterm → preterm → preterm
 
 local notation `&` k := preterm.cst k
-local infix `**` : 300 := preterm.var 
-local notation t `+*` s := preterm.add t s
-local notation t `-*` s := preterm.sub t s
+local infix ` ** ` : 300 := preterm.var
+local notation t ` +* ` s := preterm.add t s
+local notation t ` -* ` s := preterm.sub t s
 
-namespace preterm 
+namespace preterm
 
-meta def induce (tac : tactic unit := tactic.skip) : tactic unit := 
+meta def induce (tac : tactic unit := tactic.skip) : tactic unit :=
 `[ intro t, induction t with m m n t s iht ihs t s iht ihs; tac]
 
-def val (v : nat → nat) : preterm → nat 
+def val (v : nat → nat) : preterm → nat
 | (& i) := i
-| (i ** n) := 
-  if i = 1 
+| (i ** n) :=
+  if i = 1
   then v n
   else (v n) * i
-| (t1 +* t2) := t1.val + t2.val 
-| (t1 -* t2) := t1.val - t2.val 
+| (t1 +* t2) := t1.val + t2.val
+| (t1 -* t2) := t1.val - t2.val
 
 @[simp] lemma val_const {v : nat → nat} {m : nat} :
   (& m).val v = m := rfl
@@ -47,51 +47,51 @@ def val (v : nat → nat) : preterm → nat
 begin
   simp only [val], by_cases h1 : m = 1,
   rw [if_pos h1, h1, one_mul],
-  rw [if_neg h1, mul_comm], 
+  rw [if_neg h1, mul_comm],
 end
 
-@[simp] lemma val_add {v : nat → nat} {t s : preterm} : 
+@[simp] lemma val_add {v : nat → nat} {t s : preterm} :
   (t +* s).val v = t.val v + s.val v := rfl
-  
-@[simp] lemma val_sub {v : nat → nat} {t s : preterm} : 
+
+@[simp] lemma val_sub {v : nat → nat} {t s : preterm} :
   (t -* s).val v = t.val v - s.val v := rfl
 
-def fresh_index : preterm → nat 
+def fresh_index : preterm → nat
 | (& _)      := 0
 | (i ** n)   := n + 1
-| (t1 +* t2) := max t1.fresh_index t2.fresh_index 
-| (t1 -* t2) := max t1.fresh_index t2.fresh_index 
+| (t1 +* t2) := max t1.fresh_index t2.fresh_index
+| (t1 -* t2) := max t1.fresh_index t2.fresh_index
 
 def val_constant (v w : nat → nat) :
-  ∀ t : preterm, (∀ x < t.fresh_index, v x = w x) → 
-  t.val v = t.val w 
-| (& n)      h1 := rfl 
-| (m ** n)   h1 := 
+  ∀ t : preterm, (∀ x < t.fresh_index, v x = w x) →
+  t.val v = t.val w
+| (& n)      h1 := rfl
+| (m ** n)   h1 :=
   begin
-    simp only [val_var], 
+    simp only [val_var],
     apply congr_arg (λ y, m * y),
-    apply h1 _ (lt_add_one _) 
-  end 
-| (t +* s) h1 := 
+    apply h1 _ (lt_add_one _)
+  end
+| (t +* s) h1 :=
   begin
-    simp only [val_add], 
-    have ht := val_constant t 
+    simp only [val_add],
+    have ht := val_constant t
       (λ x hx, h1 _ (lt_of_lt_of_le hx (le_max_left _ _))),
-    have hs := val_constant s 
+    have hs := val_constant s
       (λ x hx, h1 _ (lt_of_lt_of_le hx (le_max_right _ _))),
     rw [ht, hs]
-  end 
-| (t -* s) h1 := 
+  end
+| (t -* s) h1 :=
   begin
     simp only [val_sub],
-    have ht := val_constant t 
+    have ht := val_constant t
       (λ x hx, h1 _ (lt_of_lt_of_le hx (le_max_left _ _))),
-    have hs := val_constant s 
+    have hs := val_constant s
       (λ x hx, h1 _ (lt_of_lt_of_le hx (le_max_right _ _))),
     rw [ht, hs]
-  end 
+  end
 
-def repr : preterm → string 
+def repr : preterm → string
 | (& i)      := i.repr
 | (i ** n)   := i.repr ++ "*x" ++ n.repr
 | (t1 +* t2) := "(" ++ t1.repr ++ " + " ++ t2.repr ++ ")"
@@ -99,7 +99,7 @@ def repr : preterm → string
 
 @[simp] def add_one (t : preterm) : preterm := t +* (&1)
 
-def sub_free : preterm → Prop 
+def sub_free : preterm → Prop
 | (& m)    := true
 | (m ** n) := true
 | (t +* s) := t.sub_free ∧ s.sub_free
@@ -107,27 +107,27 @@ def sub_free : preterm → Prop
 
 end preterm
 
-local notation as `{` m `↦` a `}` := list.func.set a as m
+local notation as ` {` m ` ↦ ` a `}` := list.func.set a as m
 
-@[simp] def canonize : preterm → term 
-| (& m)    := ⟨↑m, []⟩  
-| (m ** n) := ⟨0, [] {n ↦ ↑m}⟩ 
+@[simp] def canonize : preterm → term
+| (& m)    := ⟨↑m, []⟩
+| (m ** n) := ⟨0, [] {n ↦ ↑m}⟩
 | (t +* s) := term.add (canonize t) (canonize s)
-| (_ -* _) := ⟨0, []⟩ 
+| (_ -* _) := ⟨0, []⟩
 
-@[simp] lemma val_canonize {v : nat → nat} : 
-  ∀ {t : preterm}, t.sub_free → 
+@[simp] lemma val_canonize {v : nat → nat} :
+  ∀ {t : preterm}, t.sub_free →
   (canonize t).val (λ x, ↑(v x)) = t.val v
-| (& i) h1 := 
-  by simp only [canonize, preterm.val_const, 
+| (& i) h1 :=
+  by simp only [canonize, preterm.val_const,
      term.val, coeffs.val_nil, add_zero]
-| (i ** n) h1 := 
+| (i ** n) h1 :=
   by simp only [preterm.val_var, coeffs.val_set,
       term.val, zero_add, int.coe_nat_mul, canonize]
-| (t +* s) h1 := 
-  by simp only [val_canonize h1.left, 
+| (t +* s) h1 :=
+  by simp only [val_canonize h1.left,
      val_canonize h1.right, int.coe_nat_add,
-     canonize, term.val_add, preterm.val_add] 
+     canonize, term.val_add, preterm.val_add]
 
 end nat
 
diff --git a/src/tactic/omega/nat/sub_elim.lean b/src/tactic/omega/nat/sub_elim.lean
index b3fc6b2f6b865..95368aeef2718 100644
--- a/src/tactic/omega/nat/sub_elim.lean
+++ b/src/tactic/omega/nat/sub_elim.lean
@@ -14,15 +14,15 @@ namespace omega
 namespace nat
 
 local notation `&` k    := preterm.cst k
-local infix `**`  : 300 := preterm.var 
-local notation t `+*` s := preterm.add t s
-local notation t `-*` s := preterm.sub t s
+local infix ` ** ` : 300 := preterm.var
+local notation t ` +* ` s := preterm.add t s
+local notation t ` -* ` s := preterm.sub t s
 
-local notation x `=*` y := form.eq x y
-local notation x `≤*` y := form.le x y
-local notation `¬*` p   := form.not p
-local notation p `∨*` q := form.or p q
-local notation p `∧*` q := form.and p q
+local notation x ` =* ` y := form.eq x y
+local notation x ` ≤* ` y := form.le x y
+local notation `¬* ` p   := form.not p
+local notation p ` ∨* ` q := form.or p q
+local notation p ` ∧* ` q := form.and p q
 
 namespace preterm
 
@@ -47,7 +47,7 @@ lemma val_sub_subst {k : nat} {x y : preterm} {v : nat → nat} :
 | (m ** n) h1 :=
   begin
     have h2 : n ≠ k := ne_of_lt h1,
-    simp only [sub_subst, preterm.val], 
+    simp only [sub_subst, preterm.val],
     rw update_eq_of_ne _ h2,
  end
 | (t +* s) h1 :=
@@ -62,7 +62,7 @@ lemma val_sub_subst {k : nat} {x y : preterm} {v : nat → nat} :
     by_cases h2 : t = x ∧ s = y,
     { rw if_pos h2, simp only [val_var, one_mul],
       rw [update_eq, h2.left, h2.right] },
-    { rw if_neg h2, 
+    { rw if_neg h2,
       simp only [val_sub, sub_subst],
       apply fun_mono_2;
       apply val_sub_subst (le_trans _ h1),
@@ -95,7 +95,7 @@ def is_diff (t s : preterm) (k : nat) : form :=
 lemma holds_is_diff {t s : preterm} {k : nat} {v : nat → nat} :
   v k = t.val v - s.val v → (is_diff t s k).holds v :=
 begin
-  intro h1, 
+  intro h1,
   simp only [form.holds, is_diff, if_pos (eq.refl 1),
     preterm.val_add, preterm.val_var, preterm.val_const],
   by_cases h2 : t.val v ≤ s.val v,
@@ -119,14 +119,14 @@ lemma sub_subst_equiv {k : nat} {x y : preterm} {v : nat → nat} :
     (update k (x.val v - y.val v) v) ↔ (p.holds v))
 | (t =* s) h1 :=
   begin
-    simp only [form.holds, form.sub_subst], 
+    simp only [form.holds, form.sub_subst],
     apply pred_mono_2;
     apply preterm.val_sub_subst (le_trans _ h1),
     apply le_max_left, apply le_max_right
   end
 | (t ≤* s) h1 :=
   begin
-    simp only [form.holds, form.sub_subst], 
+    simp only [form.holds, form.sub_subst],
     apply pred_mono_2;
     apply preterm.val_sub_subst (le_trans _ h1),
     apply le_max_left, apply le_max_right
@@ -135,14 +135,14 @@ lemma sub_subst_equiv {k : nat} {x y : preterm} {v : nat → nat} :
   by { apply not_iff_not_of_iff, apply sub_subst_equiv p h1 }
 | (p ∨* q) h1 :=
   begin
-    simp only [form.holds, form.sub_subst], 
+    simp only [form.holds, form.sub_subst],
     apply pred_mono_2; apply propext;
     apply sub_subst_equiv _ (le_trans _ h1),
     apply le_max_left, apply le_max_right
   end
 | (p ∧* q) h1 :=
   begin
-    simp only [form.holds, form.sub_subst], 
+    simp only [form.holds, form.sub_subst],
     apply pred_mono_2; apply propext;
     apply sub_subst_equiv _ (le_trans _ h1),
     apply le_max_left, apply le_max_right
diff --git a/src/tactic/omega/term.lean b/src/tactic/omega/term.lean
index 00254797b4edb..1b56e9e3c781b 100644
--- a/src/tactic/omega/term.lean
+++ b/src/tactic/omega/term.lean
@@ -8,7 +8,7 @@ Normalized linear integer arithmetic terms.
 
 import tactic.omega.coeffs
 
-namespace omega 
+namespace omega
 
 def term : Type := int × list int
 
@@ -35,15 +35,15 @@ namespace term
 lemma val_neg {v : nat → int} {t : term} :
 (neg t).val v = -(t.val v) :=
 begin
-  cases t with b as, 
-  simp only [val, neg_add, neg, val, coeffs.val_neg] 
+  cases t with b as,
+  simp only [val, neg_add, neg, val, coeffs.val_neg]
 end
 
 @[simp] lemma val_sub {v : nat → int} {t1 t2 : term} :
 (sub t1 t2).val v = t1.val v - t2.val v :=
 begin
   cases t1, cases t2,
-  simp only [add_assoc, coeffs.val_sub, neg_add_rev, 
+  simp only [add_assoc, coeffs.val_sub, neg_add_rev,
     val, sub, add_comm, add_left_comm, sub_eq_add_neg]
 end
 
@@ -51,7 +51,7 @@ end
 (add t1 t2).val v = t1.val v + t2.val v :=
 begin
   cases t1, cases t2,
-  simp only [coeffs.val_add, add, 
+  simp only [coeffs.val_add, add,
     val, add_comm, add_left_comm]
 end
 
@@ -75,10 +75,16 @@ end
 
 def fresh_index (t : term) : nat := t.snd.length
 
+def to_string (t : term) : string :=
+t.2.enum.foldr (λ ⟨i, n⟩ r,
+  to_string n ++ " * x" ++ to_string i ++ " + " ++ r) (to_string t.1)
+
+instance : has_to_string term := ⟨to_string⟩
+
 end term
 
 def terms.fresh_index : list term → nat
 | []      := 0
 | (t::ts) := max t.fresh_index (terms.fresh_index ts)
 
-end omega
\ No newline at end of file
+end omega
diff --git a/test/omega.lean b/test/omega.lean
index 9dd58ab966fda..18dc49c54f41b 100644
--- a/test/omega.lean
+++ b/test/omega.lean
@@ -1,5 +1,5 @@
-/- 
-Test cases for omega. Most of the examples are from John Harrison's 
+/-
+Test cases for omega. Most of the examples are from John Harrison's
 Handbook of Practical Logic and Automated Reasoning.
 -/
 
@@ -33,13 +33,13 @@ example (x y z : nat) : (x ≤ y) → (z > y) → (x - z = 0) := by omega
 example (x y z : nat) : x - 5 > 122 → y ≤ 127 → y < x := by omega
 example : ∀ (x y : nat), x ≤ y ↔ x - y = 0 := by omega
 
-/- 
-Use `omega manual` to disable automatic reverts, 
-and `omega int` or `omega nat` to specify the domain. 
+/-
+Use `omega manual` to disable automatic reverts,
+and `omega int` or `omega nat` to specify the domain.
 -/
 example (i : int) (n : nat) (h1 : n = 0) (h2 : i < i) : false := by omega int
 example (i : int) (n : nat) (h1 : i = 0) (h2 : n < n) : false := by omega nat
-example (x y z w : int) (h1 : 3 * y ≥ x) (h2 : z > 19 * w) : 3 * x ≤ 9 * y := 
+example (x y z w : int) (h1 : 3 * y ≥ x) (h2 : z > 19 * w) : 3 * x ≤ 9 * y :=
 by {revert h1 x y, omega manual}
-example (n : nat) (h1 : n < 34) (i : int) (h2 : i * 9 = -72) : i = -8 := 
+example (n : nat) (h1 : n < 34) (i : int) (h2 : i * 9 = -72) : i = -8 :=
 by {revert h2 i, omega manual int}