refactor(*): change priority of \simeq (#1210)

* change priority of \simeq

Also change priority of similar notations
Remove many unnecessary parentheses

* lower precedence on order_embedding and similar

also add parentheses in 1 place where they were needed

* spacing

* add parenthesis

Author: fpvandoorn

src/algebra/gcd_domain.lean

@@ -576,7 +576,7 @@ lemma nat.prime_iff_prime_int {p : ℕ} : p.prime ↔ _root_.prime (p : ℤ) :=
       mt is_unit_nat.1 $ λ h, by simpa [h, not_prime_one] using hp,
     λ a b, by simpa only [int.coe_nat_dvd, (int.coe_nat_mul _ _).symm] using hp.2.2 a b⟩⟩
 
-def associates_int_equiv_nat : (associates ℤ) ≃ ℕ :=
+def associates_int_equiv_nat : associates ℤ ≃ ℕ :=
 begin
   refine ⟨λz, z.out.nat_abs, λn, associates.mk n, _, _⟩,
   { refine (assume a, quotient.induction_on' a $ assume a,

src/category_theory/endomorphism.lean

@@ -63,7 +63,7 @@ by refine { one := iso.refl X,
             inv := iso.symm,
             mul := flip iso.trans, .. } ; dunfold flip; obviously
 
-def units_End_eqv_Aut : (units (End X)) ≃* Aut X :=
+def units_End_eqv_Aut : units (End X) ≃* Aut X :=
 { to_fun := λ f, ⟨f.1, f.2, f.4, f.3⟩,
   inv_fun := λ f, ⟨f.1, f.2, f.4, f.3⟩,
   left_inv := λ ⟨f₁, f₂, f₃, f₄⟩, rfl,

src/data/equiv/algebra.lean

@@ -210,8 +210,8 @@ attribute [to_additive add_equiv.mk] mul_equiv.mk
 attribute [to_additive add_equiv.to_equiv] mul_equiv.to_equiv
 attribute [to_additive add_equiv.hom] mul_equiv.hom
 
-infix ` ≃* `:50 := mul_equiv
-infix ` ≃+ `:50 := add_equiv
+infix ` ≃* `:25 := mul_equiv
+infix ` ≃+ `:25 := add_equiv
 
 namespace mul_equiv
 
@@ -276,7 +276,7 @@ end units
 structure ring_equiv (α β : Type*) [ring α] [ring β] extends α ≃ β :=
 (hom : is_ring_hom to_fun)
 
-infix ` ≃r `:50 := ring_equiv
+infix ` ≃r `:25 := ring_equiv
 
 namespace ring_equiv
 

src/data/equiv/basic.lean

@@ -108,7 +108,7 @@ instance ulift : denumerable (ulift α) := of_equiv _ equiv.ulift
 
 instance plift : denumerable (plift α) := of_equiv _ equiv.plift
 
-def pair : (α × α) ≃ α := equiv₂ _ _
+def pair : α × α ≃ α := equiv₂ _ _
 
 end
 end denumerable

src/data/equiv/denumerable.lean

@@ -25,7 +25,7 @@ def fin_two_equiv : fin 2 ≃ bool :=
   end,
   assume b, match b with tt := rfl | ff := rfl end⟩
 
-def sum_fin_sum_equiv : (fin m ⊕ fin n) ≃ fin (m + n) :=
+def sum_fin_sum_equiv : fin m ⊕ fin n ≃ fin (m + n) :=
 { to_fun := λ x, sum.rec_on x
     (λ y, ⟨y.1, nat.lt_of_lt_of_le y.2 $ nat.le_add_right m n⟩)
     (λ y, ⟨m + y.1, nat.add_lt_add_left y.2 m⟩),
@@ -46,7 +46,7 @@ def sum_fin_sum_equiv : (fin m ⊕ fin n) ≃ fin (m + n) :=
     { dsimp, rw [dif_neg H], simp [fin.ext_iff, nat.add_sub_of_le (le_of_not_gt H)] }
   end }
 
-def fin_prod_fin_equiv : (fin m × fin n) ≃ fin (m * n) :=
+def fin_prod_fin_equiv : fin m × fin n ≃ fin (m * n) :=
 { to_fun := λ x, ⟨x.2.1 + n * x.1.1,
     calc x.2.1 + n * x.1.1 + 1
         = x.1.1 * n + x.2.1 + 1 : by ac_refl

src/data/equiv/fin.lean

@@ -12,27 +12,27 @@ open nat
 
 namespace equiv
 
-@[simp] def nat_prod_nat_equiv_nat : (ℕ × ℕ) ≃ ℕ :=
+@[simp] def nat_prod_nat_equiv_nat : ℕ × ℕ ≃ ℕ :=
 ⟨λ p, nat.mkpair p.1 p.2,
  nat.unpair,
  λ p, begin cases p, apply nat.unpair_mkpair end,
  nat.mkpair_unpair⟩
 
-@[simp] def bool_prod_nat_equiv_nat : (bool × ℕ) ≃ ℕ :=
+@[simp] def bool_prod_nat_equiv_nat : bool × ℕ ≃ ℕ :=
 ⟨λ ⟨b, n⟩, bit b n, bodd_div2,
  λ ⟨b, n⟩, by simp [bool_prod_nat_equiv_nat._match_1, bodd_bit, div2_bit],
  λ n, by simp [bool_prod_nat_equiv_nat._match_1, bit_decomp]⟩
 
-@[simp] def nat_sum_nat_equiv_nat : (ℕ ⊕ ℕ) ≃ ℕ :=
+@[simp] def nat_sum_nat_equiv_nat : ℕ ⊕ ℕ ≃ ℕ :=
 (bool_prod_equiv_sum ℕ).symm.trans bool_prod_nat_equiv_nat
 
 def int_equiv_nat : ℤ ≃ ℕ :=
 int_equiv_nat_sum_nat.trans nat_sum_nat_equiv_nat
 
-def prod_equiv_of_equiv_nat {α : Sort*} (e : α ≃ ℕ) : (α × α) ≃ α :=
-calc (α × α) ≃ (ℕ × ℕ) : prod_congr e e
-        ...  ≃ ℕ       : nat_prod_nat_equiv_nat
-        ...  ≃ α       : e.symm
+def prod_equiv_of_equiv_nat {α : Sort*} (e : α ≃ ℕ) : α × α ≃ α :=
+calc α × α ≃ ℕ × ℕ : prod_congr e e
+      ...  ≃ ℕ     : nat_prod_nat_equiv_nat
+      ...  ≃ α     : e.symm
 
 def pnat_equiv_nat : ℕ+ ≃ ℕ :=
 ⟨λ n, pred n.1, succ_pnat,

src/data/equiv/nat.lean

@@ -1081,7 +1081,7 @@ by_contradiction (mt multiset.count_eq_zero.2 H)
   of_multiset m a = m.count a :=
 rfl
 
-def equiv_multiset [decidable_eq α] : (α →₀ ℕ) ≃ (multiset α) :=
+def equiv_multiset [decidable_eq α] : (α →₀ ℕ) ≃ multiset α :=
 ⟨ to_multiset, of_multiset,
 assume f, finsupp.ext $ λ a, by rw [of_multiset_apply, count_to_multiset],
 assume m, multiset.ext.2 $ λ a, by rw [count_to_multiset, of_multiset_apply] ⟩

src/data/finsupp.lean

@@ -60,7 +60,7 @@ end sorted
 section sort
 universe variable uu
 parameters {α : Type uu} (r : α → α → Prop) [decidable_rel r]
-local infix `≼` : 50 := r
+local infix ` ≼ ` : 50 := r
 
 /- insertion sort -/
 

src/data/list/sort.lean

@@ -221,7 +221,7 @@ attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_1.eq
 attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_2.equations._eqn_1] left_coset_equiv_subgroup._match_2.equations._eqn_1
 
 noncomputable def group_equiv_quotient_times_subgroup (hs : is_subgroup s) :
-  α ≃ (quotient s × s) :=
+  α ≃ quotient s × s :=
 calc α ≃ Σ L : quotient s, {x : α // (x : quotient s)= L} :
   equiv.equiv_fib quotient_group.mk
     ... ≃ Σ L : quotient s, left_coset (quotient.out' L) s :
@@ -232,7 +232,7 @@ calc α ≃ Σ L : quotient s, {x : α // (x : quotient s)= L} :
     end)
     ... ≃ Σ L : quotient s, s :
   equiv.sigma_congr_right (λ L, left_coset_equiv_subgroup _)
-    ... ≃ (quotient s × s) :
+    ... ≃ quotient s × s :
   equiv.sigma_equiv_prod _ _
 attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup._proof_2] group_equiv_quotient_times_subgroup._proof_2
 attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup._proof_1] group_equiv_quotient_times_subgroup._proof_1
@@ -246,7 +246,7 @@ namespace quotient_group
 variables [group α]
 
 noncomputable def preimage_mk_equiv_subgroup_times_set
-  (s : set α) [is_subgroup s] (t : set (quotient s)) : quotient_group.mk ⁻¹' t ≃ (s × t) :=
+  (s : set α) [is_subgroup s] (t : set (quotient s)) : quotient_group.mk ⁻¹' t ≃ s × t :=
 have h : ∀ {x : quotient s} {a : α}, x ∈ t → a ∈ s →
   (quotient.mk' (quotient.out' x * a) : quotient s) = quotient.mk' (quotient.out' x) :=
     λ x a hx ha, quotient.sound' (show (quotient.out' x * a)⁻¹ * quotient.out' x ∈ s,