diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 154214d6f5..f26a80a60c 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -294,19 +294,17 @@ class inductive Decidable (p : Prop)
 | isFalse (h : ¬p) : Decidable
 | isTrue  (h : p) : Decidable
 
-@[reducible] def DecidablePred {α : Sort u} (r : α → Prop) :=
+abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
 ∀ (a : α), Decidable (r a)
 
-@[reducible] def DecidableRel {α : Sort u} (r : α → α → Prop) :=
+abbrev DecidableRel {α : Sort u} (r : α → α → Prop) :=
 ∀ (a b : α), Decidable (r a b)
 
-class DecidableEq (α : Sort u) :=
-{decEq : ∀ (a b : α), Decidable (a = b)}
+abbrev DecidableEq (α : Sort u) :=
+∀ (a b : α), Decidable (a = b)
 
-export DecidableEq (decEq)
-
-@[inline] instance decidableOfDecidableEq {α : Sort u} (a b : α) [DecidableEq α] : Decidable (a = b) :=
-decEq a b
+def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) :=
+s a b
 
 inductive Option (α : Type u)
 | none {} : Option
@@ -953,11 +951,11 @@ theorem Bool.falseNeTrue (h : false = true) : False :=
 Bool.noConfusion h
 
 instance : DecidableEq Bool :=
-{decEq := fun a b => match a, b with
+fun a b => match a, b with
  | false, false => isTrue rfl
  | false, true  => isFalse Bool.falseNeTrue
  | true, false  => isFalse (Ne.symm Bool.falseNeTrue)
- | true, true   => isTrue rfl}
+ | true, true   => isTrue rfl
 
 /- if-then-else expression theorems -/
 
@@ -1181,9 +1179,9 @@ instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p
 ⟨⟨a, h⟩⟩
 
 instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
-{decEq := fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
+fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
   if h : a = b then isTrue (Subtype.eq h)
-  else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))}
+  else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))
 end Subtype
 
 /- Sum -/
@@ -1198,7 +1196,7 @@ instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) :=
 ⟨Sum.inr (arbitrary β)⟩
 
 instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) :=
-{decEq := fun a b =>
+fun a b =>
  match a, b with
  | (Sum.inl a), (Sum.inl b) =>
    if h : a = b then isTrue (h ▸ rfl)
@@ -1207,7 +1205,7 @@ instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : Decidab
    if h : a = b then isTrue (h ▸ rfl)
    else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h))
  | (Sum.inr a), (Sum.inl b) => isFalse (fun h => Sum.noConfusion h)
- | (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h)}
+ | (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h)
 end
 
 /- Product -/
@@ -1219,13 +1217,13 @@ instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
 ⟨(arbitrary α, arbitrary β)⟩
 
 instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
-{decEq := fun ⟨a, b⟩ ⟨a', b'⟩ =>
+fun ⟨a, b⟩ ⟨a', b'⟩ =>
   match (decEq a a') with
   | (isTrue e₁) =>
     match (decEq b b') with
     | (isTrue e₂)  => isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
     | (isFalse n₂) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂))
-  | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))}
+  | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))
 
 instance [HasBeq α] [HasBeq β] : HasBeq (α × β) :=
 ⟨fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂⟩
@@ -1284,7 +1282,7 @@ instance : Inhabited PUnit :=
 ⟨⟨⟩⟩
 
 instance : DecidableEq PUnit :=
-{decEq := fun a b => isTrue (punitEq a b)}
+fun a b => isTrue (punitEq a b)
 
 /- Setoid -/
 
@@ -1560,12 +1558,12 @@ EqvGen.recOn H
 end
 
 instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
-{decEq := fun (q₁ q₂ : Quotient s) =>
+fun (q₁ q₂ : Quotient s) =>
   Quotient.recOnSubsingleton₂ q₁ q₂
     (fun a₁ a₂ =>
       match (d a₁ a₂) with
       | (isTrue h₁)  => isTrue (Quotient.sound h₁)
-      | (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂))}
+      | (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂))
 
 /- Function extensionality -/
 
@@ -1706,7 +1704,7 @@ noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
 ⟨propDecidable a⟩
 
 noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
-{decEq := fun x y => propDecidable (x = y)}
+fun x y => propDecidable (x = y)
 
 noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
 match (propDecidable (Nonempty α)) with
diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean
index edddab916b..abbf81ce66 100644
--- a/src/Init/Data/Char/Basic.lean
+++ b/src/Init/Data/Char/Basic.lean
@@ -63,8 +63,7 @@ theorem vneOfNe {c d : Char} (h : c ≠ d) : c.val ≠ d.val :=
 fun h' => absurd (eqOfVeq h') h
 
 instance : DecidableEq Char :=
-{decEq := fun i j => decidableOfDecidableOfIff
-  (decEq i.val j.val) ⟨Char.eqOfVeq, Char.veqOfEq⟩}
+fun i j => decidableOfDecidableOfIff (decEq i.val j.val) ⟨Char.eqOfVeq, Char.veqOfEq⟩
 
 instance : Inhabited Char :=
 ⟨'A'⟩
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index e115b16e32..2e7efb4a56 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -103,5 +103,4 @@ end Fin
 open Fin
 
 instance (n : Nat) : DecidableEq (Fin n) :=
-{decEq := fun i j => decidableOfDecidableOfIff
-  (decEq i.val j.val) ⟨eqOfVeq, veqOfEq⟩}
+fun i j => decidableOfDecidableOfIff (decEq i.val j.val) ⟨eqOfVeq, veqOfEq⟩
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index 2709544694..25dee66589 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -96,7 +96,7 @@ match a, b with
  | negSucc a, ofNat b => isFalse $ fun h => Int.noConfusion h
 
 instance Int.DecidableEq : DecidableEq Int :=
-{decEq := Int.decEq}
+Int.decEq
 
 @[extern "lean_int_dec_nonneg"]
 private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index a9e50cd84f..05a84824a3 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -30,7 +30,7 @@ protected def hasDecEq [DecidableEq α] : ∀ (a b : List α), Decidable (a = b)
   | isFalse nab => isFalse (fun h => List.noConfusion h (fun hab _ => absurd hab nab))
 
 instance [DecidableEq α] : DecidableEq (List α) :=
-{decEq := List.hasDecEq}
+List.hasDecEq
 
 def reverseAux : List α → List α → List α
 | [],   r => r
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index 3a6e5c3381..84dce91155 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -40,7 +40,7 @@ if h : beq n m = true then isTrue (eqOfBeqEqTt h)
 else isFalse (neOfBeqEqFf (eqFalseOfNeTrue h))
 
 @[inline] instance : DecidableEq Nat :=
-{decEq := Nat.decEq}
+Nat.decEq
 
 @[extern "lean_nat_dec_le"]
 def ble : Nat → Nat → Bool
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index 64f6b9aad6..4949dcde36 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -75,14 +75,14 @@ instance (α : Type u) : Inhabited (Option α) :=
 ⟨none⟩
 
 instance {α : Type u} [DecidableEq α] : DecidableEq (Option α) :=
-{decEq := fun a b => match a, b with
+fun a b => match a, b with
  | none,      none      => isTrue rfl
  | none,      (some v₂) => isFalse (fun h => Option.noConfusion h)
  | (some v₁), none      => isFalse (fun h => Option.noConfusion h)
  | (some v₁), (some v₂) =>
    match decEq v₁ v₂ with
    | (isTrue e)  => isTrue (congrArg (@some α) e)
-   | (isFalse n) => isFalse (fun h => Option.noConfusion h (fun e => absurd e n))}
+   | (isFalse n) => isFalse (fun h => Option.noConfusion h (fun e => absurd e n))
 
 instance {α : Type u} [HasBeq α] : HasBeq (Option α) :=
 ⟨fun a b => match a, b with
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 15b4c3e384..6a6635d263 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -28,7 +28,7 @@ match s₁, s₂ with
  else isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h))
 
 instance : DecidableEq String :=
-{decEq := String.decEq}
+String.decEq
 
 def List.asString (s : List Char) : String :=
 ⟨s⟩
diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean
index f664d20ca0..8bb0a3d14f 100644
--- a/src/Init/Data/UInt.lean
+++ b/src/Init/Data/UInt.lean
@@ -64,7 +64,7 @@ def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
 UInt8.casesOn a $ fun n => UInt8.casesOn b $ fun m =>
   inferInstanceAs (Decidable (n <= m))
 
-instance : DecidableEq UInt8 := {decEq := UInt8.decEq}
+instance : DecidableEq UInt8 := UInt8.decEq
 instance UInt8.hasDecidableLt (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
 instance UInt8.hasDecidableLe (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
 
@@ -123,7 +123,7 @@ def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
 UInt16.casesOn a $ fun n => UInt16.casesOn b $ fun m =>
   inferInstanceAs (Decidable (n <= m))
 
-instance : DecidableEq UInt16 := {decEq := UInt16.decEq}
+instance : DecidableEq UInt16 := UInt16.decEq
 instance UInt16.hasDecidableLt (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
 instance UInt16.hasDecidableLe (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
 
@@ -182,7 +182,7 @@ def UInt32.decLe (a b : UInt32) : Decidable (a ≤ b) :=
 UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
   inferInstanceAs (Decidable (n <= m))
 
-instance : DecidableEq UInt32 := {decEq := UInt32.decEq}
+instance : DecidableEq UInt32 := UInt32.decEq
 instance UInt32.hasDecidableLt (a b : UInt32) : Decidable (a < b) := UInt32.decLt a b
 instance UInt32.hasDecidableLe (a b : UInt32) : Decidable (a ≤ b) := UInt32.decLe a b
 
@@ -258,7 +258,7 @@ def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
 UInt64.casesOn a $ fun n => UInt64.casesOn b $ fun m =>
   inferInstanceAs (Decidable (n <= m))
 
-instance : DecidableEq UInt64 := {decEq := UInt64.decEq}
+instance : DecidableEq UInt64 := UInt64.decEq
 instance UInt64.hasDecidableLt (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
 instance UInt64.hasDecidableLe (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 
@@ -332,7 +332,7 @@ def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
 USize.casesOn a $ fun n => USize.casesOn b $ fun m =>
   inferInstanceAs (Decidable (n <= m))
 
-instance : DecidableEq USize := {decEq := USize.decEq}
+instance : DecidableEq USize := USize.decEq
 instance USize.hasDecidableLt (a b : USize) : Decidable (a < b) := USize.decLt a b
 instance USize.hasDecidableLe (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
 
diff --git a/src/Init/Lean/Position.lean b/src/Init/Lean/Position.lean
index e6f164e052..534c4ef687 100644
--- a/src/Init/Lean/Position.lean
+++ b/src/Init/Lean/Position.lean
@@ -16,11 +16,11 @@ structure Position :=
 
 namespace Position
 instance : DecidableEq Position :=
-{decEq := fun ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ =>
+fun ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ =>
   if h₁ : l₁ = l₂ then
   if h₂ : c₁ = c₂ then isTrue (Eq.recOn h₁ (Eq.recOn h₂ rfl))
   else isFalse (fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₂ h₂))
-  else isFalse (fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₁ h₁))}
+  else isFalse (fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₁ h₁))
 
 protected def lt : Position → Position → Bool
 | ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ => (l₁, c₁) < (l₂, c₂)