chore(library): remove some unnecessary parentheses

library/algebra/ordered_group.lean

@@ -520,7 +520,7 @@ section
           have H3 : abs (b + a) ≤ abs b + abs a,
           begin
             rewrite add.comm at H1,
-            exact (aux1 H1 H2)
+            exact aux1 H1 H2
           end,
           rewrite [add.comm, {abs a + _}add.comm],
           exact H3

library/data/examples/notencodable.lean

@@ -32,11 +32,11 @@ private definition v : nat := encode_fun f
 
 private lemma f_eq : succ (f v) = f v :=
 begin
-  change (succ (f v) =
-          match decode_fun (encode_fun f) with
-          | some g := succ (g v)
-          | none   := 0
-          end),
+  change succ (f v) =
+         match decode_fun (encode_fun f) with
+         | some g := succ (g v)
+         | none   := 0
+         end,
   rewrite encodek_fun
 end
 end

library/data/int/basic.lean

@@ -372,7 +372,7 @@ begin
   apply equiv.trans,
   apply repr_add,
   apply equiv.symm,
-  apply (eq.subst (padd_comm (repr b) (repr a))),
+  apply eq.subst (padd_comm (repr b) (repr a)),
   apply repr_add
 end
 
@@ -385,7 +385,7 @@ begin
   apply eq_of_repr_equiv_repr,
   apply equiv.trans,
   apply H1,
-  apply (eq.subst ((padd_assoc _ _ _)⁻¹)),
+  apply eq.subst (padd_assoc _ _ _)⁻¹,
   apply equiv.symm,
   apply H2
 end

library/data/list/comb.lean

@@ -135,9 +135,9 @@ section foldl_eq_foldr
   | a b  nil    := Hcomm a b
   | a b  (c::l) :=
     begin
-      change (foldl f (f (f a b) c) l = f b (foldl f (f a c) l)),
+      change foldl f (f (f a b) c) l = f b (foldl f (f a c) l),
       rewrite -foldl_eq_of_comm_of_assoc,
-      change (foldl f (f (f a b) c) l = foldl f (f (f a c) b) l),
+      change foldl f (f (f a b) c) l = foldl f (f (f a c) b) l,
       have H₁ : f (f a b) c = f (f a c) b, by rewrite [Hassoc, Hassoc, Hcomm b c],
       rewrite H₁
     end
@@ -148,7 +148,7 @@ section foldl_eq_foldr
     begin
       rewrite foldl_eq_of_comm_of_assoc,
       esimp,
-      change (f b (foldl f a l) = f b (foldr f a l)),
+      change f b (foldl f a l) = f b (foldr f a l),
       rewrite foldl_eq_foldr
     end
 end foldl_eq_foldr
@@ -259,7 +259,7 @@ theorem zip_unzip : ∀ (l : list (A × B)), zip (pr₁ (unzip l)) (pr₂ (unzip
     rewrite unzip_cons,
     have r : zip (pr₁ (unzip l)) (pr₂ (unzip l)) = l, from zip_unzip l,
     revert r,
-    apply (prod.cases_on (unzip l)),
+    apply prod.cases_on (unzip l),
     intros [la, lb, r],
     rewrite -r
   end

library/data/list/perm.lean

@@ -270,9 +270,9 @@ match l₂ with
 | []   := λ e h₁ h₂, list.no_confusion e (λ e₁ e₂, h₁ rfl e₁ e₂)
 | h::t := λ e h₁ h₂,
   begin
-    apply (list.no_confusion e), intros [e₁, e₂],
+    apply list.no_confusion e, intros [e₁, e₂],
     rewrite e₁ at h₂,
-    exact (h₂ t rfl e₂)
+    exact h₂ t rfl e₂
   end
 end
 
@@ -289,17 +289,17 @@ match l₂ with
 | [h₁] := λ e H₁ H₂ H₃,
   begin
     rewrite [append_cons at e, append_nil_left at e],
-    apply (list.no_confusion e), intros [a_eq_h₁, rest],
-    apply (list.no_confusion rest), intros [b_eq_c, l₁_eq_l₃],
+    apply list.no_confusion e, intros [a_eq_h₁, rest],
+    apply list.no_confusion rest, intros [b_eq_c, l₁_eq_l₃],
     rewrite [a_eq_h₁ at H₂, b_eq_c at H₂, l₁_eq_l₃ at H₂],
-    exact (H₂ rfl rfl rfl)
+    exact H₂ rfl rfl rfl
   end
 | h₁::h₂::t₂ := λ e H₁ H₂ H₃,
   begin
-    apply (list.no_confusion e),    intros [a_eq_h₁, rest],
-    apply (list.no_confusion rest), intros [b_eq_h₂, l₁_eq],
+    apply list.no_confusion e,    intros [a_eq_h₁, rest],
+    apply list.no_confusion rest, intros [b_eq_h₂, l₁_eq],
     rewrite [a_eq_h₁ at H₃, b_eq_h₂ at H₃],
-    exact (H₃ t₂ rfl l₁_eq)
+    exact H₃ t₂ rfl l₁_eq
   end
 end
 
@@ -546,7 +546,7 @@ assume p, perm_induction_on p
             begin
               rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_mem yinxt₂,
                        erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_not_mem nxint₂, xeqy],
-              exact (skip y r)
+              exact skip y r
             end)
           (λ xney : x ≠ y,
             have xint₁     : x ∈ t₁, from or_resolve_right xinyt₁ xney,
@@ -558,7 +558,7 @@ assume p, perm_induction_on p
             begin
               rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_not_mem nyinxt₂,
                        erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_mem xint₂],
-              exact (skip y r)
+              exact skip y r
             end)))
     (λ nxinyt₁ : x ∉ y::t₁,
       have   xney    : x ≠ y,  from not_eq_of_not_mem nxinyt₁,
@@ -571,7 +571,7 @@ assume p, perm_induction_on p
           begin
             rewrite [erase_dup_cons_of_not_mem nxinyt₁, erase_dup_cons_of_mem yinxt₂,
                      erase_dup_cons_of_mem yint₁, erase_dup_cons_of_not_mem nxint₂],
-            exact (skip x r)
+            exact skip x r
           end)
         (λ nyint₁ : y ∉ t₁,
           assert nyinxt₂ : y ∉ x::t₂, from
@@ -581,7 +581,7 @@ assume p, perm_induction_on p
           begin
             rewrite [erase_dup_cons_of_not_mem nxinyt₁, erase_dup_cons_of_not_mem nyinxt₂,
                      erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_not_mem nxint₂],
-            exact (xswap x y r)
+            exact xswap x y r
           end)))
   (λ t₁ t₂ t₃ p₁ p₂ r₁ r₂, trans r₁ r₂)
 

library/init/funext.lean

@@ -55,7 +55,7 @@ section
   assume H, calc
      f₁ = extfun_app ⟦f₁⟧ : rfl
     ... = extfun_app ⟦f₂⟧ : {sound H}
-    ... = f₂             : rfl
+    ... = f₂              : rfl
 end
 
 open function.equiv_notation