diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 0137e9a058..63a238332e 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -442,13 +442,13 @@ instance : Inhabited True where
   default := trivial
 
 instance : Inhabited NonScalar where
-  default := ⟨arbitrary _⟩
+  default := ⟨arbitrary⟩
 
 instance : Inhabited PNonScalar.{u} where
-  default := ⟨arbitrary _⟩
+  default := ⟨arbitrary⟩
 
 instance {α} [Inhabited α] : Inhabited (ForInStep α) where
-  default := ForInStep.done (arbitrary _)
+  default := ForInStep.done (arbitrary)
 
 class inductive Nonempty (α : Sort u) : Prop :=
   | intro (val : α) : Nonempty α
@@ -457,7 +457,7 @@ protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂
   h₂ h₁.1
 
 instance {α : Sort u} [Inhabited α] : Nonempty α where
-  val := arbitrary α
+  val := arbitrary
 
 theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
   | ⟨w, h⟩ => ⟨w⟩
@@ -548,10 +548,10 @@ section
 variables {α : Type u} {β : Type v}
 
 instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) where
-  default := Sum.inl (arbitrary α)
+  default := Sum.inl arbitrary
 
 instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) where
-  default := Sum.inr (arbitrary β)
+  default := Sum.inr arbitrary
 
 instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
   match a, b with
@@ -572,7 +572,7 @@ section
 variables {α : Type u} {β : Type v}
 
 instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
-  default := (arbitrary α, arbitrary β)
+  default := (arbitrary, arbitrary)
 
 instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
   fun ⟨a, b⟩ ⟨a', b'⟩ =>
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index b053277356..a333445404 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -118,7 +118,7 @@ def modifyM [Monad m] [Inhabited α] (a : Array α) (i : Nat) (f : α → m α)
   if h : i < a.size then
     let idx : Fin a.size := ⟨i, h⟩
     let v                := a.get idx
-    let a'               := a.set idx (arbitrary α)
+    let a'               := a.set idx arbitrary
     let v ← f v
     pure <| a'.set (sizeSetEq a .. ▸ idx) v
   else
@@ -250,7 +250,7 @@ unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
   let rec @[specialize] map (i : USize) (r : Array NonScalar) : m (Array PNonScalar.{v}) := do
     if i < sz then
      let v    := r.uget i lcProof
-     let r    := r.uset i (arbitrary _) lcProof
+     let r    := r.uset i arbitrary lcProof
      let vNew ← f (unsafeCast v)
      map (i+1) (r.uset i (unsafeCast vNew) lcProof)
     else
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index fbf6b5a26b..ab7f3d2ff7 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -47,7 +47,7 @@ def toList (s : String) : List Char :=
   s.data
 
 private def utf8GetAux : List Char → Pos → Pos → Char
-  | [],    i, p => arbitrary Char
+  | [],    i, p => arbitrary
   | c::cs, i, p => if i = p then c else utf8GetAux cs (i + csize c) p
 
 @[extern "lean_string_utf8_get"]
diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean
index 77f4e0fbff..17b45bbe6f 100644
--- a/src/Init/Data/UInt.lean
+++ b/src/Init/Data/UInt.lean
@@ -145,9 +145,9 @@ instance : ModN UInt32      := ⟨UInt32.modn⟩
 instance : Div UInt32       := ⟨UInt32.div⟩
 
 @[extern c inline "#1 << #2"]
-constant UInt32.shiftLeft (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
+constant UInt32.shiftLeft (a b : UInt32) : UInt32
 @[extern c inline "#1 >> #2"]
-constant UInt32.shiftRight (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
+constant UInt32.shiftRight (a b : UInt32) : UInt32
 
 @[extern "lean_uint64_of_nat"]
 def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨Fin.ofNat n⟩
@@ -183,9 +183,9 @@ def UInt32.toUInt64 (a : UInt32) : UInt64 := a.toNat.toUInt64
 
 -- TODO(Leo): give reference implementation for shiftLeft and shiftRight, and define them for other UInt types
 @[extern c inline "#1 << #2"]
-constant UInt64.shiftLeft (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64
+constant UInt64.shiftLeft (a b : UInt64) : UInt64
 @[extern c inline "#1 >> #2"]
-constant UInt64.shiftRight (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64
+constant UInt64.shiftRight (a b : UInt64) : UInt64
 
 instance : OfNat UInt64     := ⟨UInt64.ofNat⟩
 instance : Add UInt64       := ⟨UInt64.add⟩
@@ -248,9 +248,9 @@ def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
 
 -- TODO(Leo): give reference implementation for shiftLeft and shiftRight, and define them for other UInt types
 @[extern c inline "#1 << #2"]
-constant USize.shiftLeft (a b : USize) : USize := (arbitrary Nat).toUSize
+constant USize.shiftLeft (a b : USize) : USize
 @[extern c inline "#1 >> #2"]
-constant USize.shiftRight (a b : USize) : USize := (arbitrary Nat).toUSize
+constant USize.shiftRight (a b : USize) : USize
 def USize.lt (a b : USize) : Prop := a.val < b.val
 def USize.le (a b : USize) : Prop := a.val ≤ b.val
 
diff --git a/src/Init/Fix.lean b/src/Init/Fix.lean
index c626917df3..6d219c7cb7 100644
--- a/src/Init/Fix.lean
+++ b/src/Init/Fix.lean
@@ -19,10 +19,10 @@ def fixCore1 {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α
   fixCore1 base rec
 
 @[inline] def fix1 {α β : Type u} [Inhabited β] (rec : (α → β) → α → β) : α → β :=
-  fixCore1 (fun _ => arbitrary β) rec
+  fixCore1 (fun _ => arbitrary) rec
 
 @[inline] def fix {α β : Type u} [Inhabited β] (rec : (α → β) → α → β) : α → β :=
-  fixCore1 (fun _ => arbitrary β) rec
+  fixCore1 (fun _ => arbitrary) rec
 
 def bfix2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : Nat → α₁ → α₂ → β
   | 0,   a₁, a₂ => base a₁ a₂
@@ -33,7 +33,7 @@ def fixCore2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (
   bfix2 base rec USize.size
 
 @[inline] def fix2 {α₁ α₂ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
-  fixCore2 (fun _ _ => arbitrary β) rec
+  fixCore2 (fun _ _ => arbitrary) rec
 
 def bfix3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : Nat → α₁ → α₂ → α₃ → β
   | 0,   a₁, a₂, a₃ => base a₁ a₂ a₃
@@ -44,7 +44,7 @@ def fixCore3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ 
   bfix3 base rec USize.size
 
 @[inline] def fix3 {α₁ α₂ α₃ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
-  fixCore3 (fun _ _ _ => arbitrary β) rec
+  fixCore3 (fun _ _ _ => arbitrary) rec
 
 def bfix4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : Nat → α₁ → α₂ → α₃ → α₄ → β
   | 0,   a₁, a₂, a₃, a₄ => base a₁ a₂ a₃ a₄
@@ -55,7 +55,7 @@ def fixCore4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → 
   bfix4 base rec USize.size
 
 @[inline] def fix4 {α₁ α₂ α₃ α₄ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
-fixCore4 (fun _ _ _ _ => arbitrary β) rec
+fixCore4 (fun _ _ _ _ => arbitrary) rec
 
 def bfix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → β
   | 0,   a₁, a₂, a₃, a₄, a₅ => base a₁ a₂ a₃ a₄ a₅
@@ -66,7 +66,7 @@ def fixCore5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂
   bfix5 base rec USize.size
 
 @[inline] def fix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
-  fixCore5 (fun _ _ _ _ _ => arbitrary β) rec
+  fixCore5 (fun _ _ _ _ _ => arbitrary) rec
 
 def bfix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β
   | 0,   a₁, a₂, a₃, a₄, a₅, a₆ => base a₁ a₂ a₃ a₄ a₅ a₆
@@ -77,4 +77,4 @@ def fixCore6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ →
   bfix6 base rec USize.size
 
 @[inline] def fix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
-  fixCore6 (fun _ _ _ _ _ _ => arbitrary β) rec
+  fixCore6 (fun _ _ _ _ _ _ => arbitrary) rec
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 3a3028457c..8041380948 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -186,17 +186,17 @@ theorem neTrueOfEqFalse : {b : Bool} → Eq b false → Not (Eq b true)
 class Inhabited (α : Sort u) where
   mk {} :: (default : α)
 
-constant arbitrary (α : Sort u) [s : Inhabited α] : α :=
-  @Inhabited.default α s
+constant arbitrary [Inhabited α] : α :=
+  Inhabited.default
 
 instance : Inhabited (Sort u) where
   default := PUnit
 
 instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
-  default := fun _ => arbitrary β
+  default := fun _ => arbitrary
 
 instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) where
-  default := fun a => arbitrary (β a)
+  default := fun _ => arbitrary
 
 /-- Universe lifting operation from Sort to Type -/
 structure PLift (α : Sort u) : Type u where
@@ -981,7 +981,7 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
 /- "Comfortable" version of `fget`. It performs a bound check at runtime. -/
 @[extern "lean_array_get"]
 def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
-  dite (Less i a.size) (fun h => a.get ⟨i, h⟩) (fun _ => arbitrary α)
+  dite (Less i a.size) (fun h => a.get ⟨i, h⟩) (fun _ => arbitrary)
 
 def Array.getOp {α : Type u} [Inhabited α] (self : Array α) (idx : Nat) : α :=
   self.get! idx
@@ -1040,7 +1040,7 @@ instance {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m 
   default := pure
 
 instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) where
-  default := pure (arbitrary _)
+  default := pure arbitrary
 
 /-- A Function for lifting a computation from an inner Monad to an outer Monad.
     Like [MonadTrans](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html),
@@ -1092,7 +1092,7 @@ inductive Except (ε : Type u) (α : Type v) where
 attribute [unbox] Except
 
 instance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) where
-  default := Except.error (arbitrary ε)
+  default := Except.error arbitrary
 
 /-- An implementation of [MonadError](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError) -/
 class MonadExceptOf (ε : Type u) (m : Type v → Type w) where
@@ -1132,7 +1132,7 @@ def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v)
   ρ → m α
 
 instance (ρ : Type u) (m : Type u → Type v) (α : Type u) [Inhabited (m α)] : Inhabited (ReaderT ρ m α) where
-  default := fun _ => arbitrary _
+  default := fun _ => arbitrary
 
 @[inline] def ReaderT.run {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) : m α :=
   x r
@@ -1293,7 +1293,7 @@ inductive Result (ε σ α : Type u) where
 variables {ε σ α : Type u}
 
 instance [Inhabited ε] [Inhabited σ] : Inhabited (Result ε σ α) where
-  default := Result.error (arbitrary _) (arbitrary _)
+  default := Result.error arbitrary arbitrary
 
 end EStateM
 
@@ -1304,8 +1304,8 @@ namespace EStateM
 
 variables {ε σ α β : Type u}
 
-instance [Inhabited ε] : Inhabited (EStateM ε σ α) := ⟨fun s =>
-  Result.error (arbitrary ε) s⟩
+instance [Inhabited ε] : Inhabited (EStateM ε σ α) where
+  default := fun s => Result.error arbitrary s
 
 @[inline] protected def pure (a : α) : EStateM ε σ α := fun s =>
   Result.ok a s
@@ -1677,7 +1677,7 @@ structure MacroScopesView where
   scopes     : List MacroScope
 
 instance : Inhabited MacroScopesView where
-  default := ⟨arbitrary _, arbitrary _, arbitrary _, arbitrary _⟩
+  default := ⟨arbitrary, arbitrary, arbitrary, arbitrary⟩
 
 def MacroScopesView.review (view : MacroScopesView) : Name :=
   match view.scopes with
diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean
index 7db8f00502..232da595cb 100644
--- a/src/Init/System/ST.lean
+++ b/src/Init/System/ST.lean
@@ -45,8 +45,8 @@ constant RefPointed : PointedType.{0}
 structure Ref (σ : Type) (α : Type) : Type :=
   (ref : RefPointed.type) (h : Nonempty α)
 
-instance {σ α} [Inhabited α] : Inhabited (Ref σ α) :=
-  ⟨{ ref := RefPointed.val, h := Nonempty.intro <| arbitrary _}⟩
+instance {σ α} [Inhabited α] : Inhabited (Ref σ α) where
+  default := { ref := RefPointed.val, h := Nonempty.intro arbitrary }
 
 namespace Prim
 
@@ -54,7 +54,7 @@ set_option pp.all true
 /- Auxiliary definition for showing that `ST σ α` is inhabited when we have a `Ref σ α` -/
 private noncomputable def inhabitedFromRef {σ α} (r : Ref σ α) : ST σ α :=
   let inh : Inhabited α := Classical.inhabitedOfNonempty r.h
-  pure <| arbitrary α
+  pure arbitrary
 
 @[extern "lean_st_mk_ref"]
 constant mkRef {σ α} (a : α) : ST σ (Ref σ α) := pure { ref := RefPointed.val, h := Nonempty.intro a }
diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 03a6dd723a..24c10d1bb7 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -44,7 +44,7 @@ structure AttributeImpl extends AttributeImplCore :=
   (add (decl : Name) (args : Syntax) (persistent : Bool) : AttrM Unit)
 
 instance : Inhabited AttributeImpl :=
-  ⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure () }⟩
+  ⟨{ name := arbitrary, descr := arbitrary, add := fun env _ _ _ => pure () }⟩
 
 open Std (PersistentHashMap)
 
@@ -224,7 +224,7 @@ def registerTagAttribute (name : Name) (descr : String) (validate : Name → Att
 
 namespace TagAttribute
 
-instance : Inhabited TagAttribute := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
+instance : Inhabited TagAttribute := ⟨{ attr := arbitrary, ext := arbitrary }⟩
 
 def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool :=
   match env.getModuleIdxFor? decl with
@@ -275,12 +275,12 @@ def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAtt
 
 namespace ParametricAttribute
 
-instance {α : Type} : Inhabited (ParametricAttribute α) := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
+instance {α : Type} : Inhabited (ParametricAttribute α) := ⟨{attr := arbitrary, ext := arbitrary }⟩
 
 def getParam {α : Type} [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α :=
   match env.getModuleIdxFor? decl with
   | some modIdx =>
-    match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
+    match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary) (fun a b => Name.quickLt a.1 b.1) with
     | some (_, val) => some val
     | none          => none
   | none        => (attr.ext.getState env).find? decl
@@ -334,12 +334,12 @@ def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDesc
 
 namespace EnumAttributes
 
-instance {α : Type} : Inhabited (EnumAttributes α) := ⟨{attrs := [], ext := arbitrary _}⟩
+instance {α : Type} : Inhabited (EnumAttributes α) := ⟨{attrs := [], ext := arbitrary }⟩
 
 def getValue {α : Type} [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option α :=
   match env.getModuleIdxFor? decl with
   | some modIdx =>
-    match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
+    match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary) (fun a b => Name.quickLt a.1 b.1) with
     | some (_, val) => some val
     | none          => none
   | none        => (attr.ext.getState env).find? decl
diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index 0ce5e59d3f..d6a586be6f 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -287,7 +287,7 @@ abbrev Alt := AltCore FnBody
 @[matchPattern] abbrev Alt.ctor    := @AltCore.ctor FnBody
 @[matchPattern] abbrev Alt.default := @AltCore.default FnBody
 
-instance : Inhabited Alt := ⟨Alt.default (arbitrary _)⟩
+instance : Inhabited Alt := ⟨Alt.default arbitrary⟩
 
 def FnBody.isTerminal : FnBody → Bool
   | FnBody.case _ _ _ _  => true
@@ -367,7 +367,7 @@ partial def reshapeAux (a : Array FnBody) (i : Nat) (b : FnBody) : FnBody :=
   if i == 0 then b
   else
     let i         := i - 1
-    let (curr, a) := a.swapAt! i (arbitrary _)
+    let (curr, a) := a.swapAt! i arbitrary
     let b         := curr.setBody b
     reshapeAux a i b
 
@@ -394,7 +394,7 @@ inductive Decl :=
 namespace Decl
 
 instance : Inhabited Decl :=
-  ⟨fdecl (arbitrary _) (arbitrary _) IRType.irrelevant (arbitrary _)⟩
+  ⟨fdecl arbitrary arbitrary IRType.irrelevant arbitrary⟩
 
 def name : Decl → FunId
   | Decl.fdecl f _ _ _  => f
diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean
index c8cb2dcec7..e157e89f4a 100644
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@@ -143,7 +143,7 @@ def applyParamMap (decls : Array Decl) (map : ParamMap) : Array Decl :=
 
 structure BorrowInfCtx :=
   (env      : Environment)
-  (currFn   : FunId    := arbitrary _) -- Function being analyzed.
+  (currFn   : FunId    := arbitrary) -- Function being analyzed.
   (paramSet : IndexSet := {}) -- Set of all function parameters in scope. This is used to implement the heuristic at `ownArgsUsingParams`
 
 structure BorrowInfState :=
diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index d24fd5bffe..1e923ca99a 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -56,15 +56,15 @@ def mkBoxedVersionAux (decl : Decl) : N Decl := do
       pure (newVDecls, xs.push (Arg.var q.x))
     else
       let x ← N.mkFresh
-      pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (arbitrary _)), xs.push (Arg.var x))
+      pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) arbitrary), xs.push (Arg.var x))
   let r ← N.mkFresh
-  let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (arbitrary _))
+  let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) arbitrary)
   let body ←
     if !decl.resultType.isScalar then
       pure $ reshape newVDecls (FnBody.ret (Arg.var r))
     else
       let newR ← N.mkFresh
-      let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) (arbitrary _))
+      let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) arbitrary)
       pure $ reshape newVDecls (FnBody.ret (Arg.var newR))
   pure $ Decl.fdecl (mkBoxedName decl.name) qs IRType.object body
 
@@ -97,7 +97,7 @@ def eqvTypes (t₁ t₂ : IRType) : Bool :=
   (t₁.isScalar == t₂.isScalar) && (!t₁.isScalar || t₁ == t₂)
 
 structure BoxingContext :=
-  (f : FunId := arbitrary _)
+  (f : FunId := arbitrary)
   (localCtx : LocalContext := {})
   (resultType : IRType := IRType.irrelevant)
   (decls : Array Decl)
@@ -146,7 +146,7 @@ def getDecl (fid : FunId) : M Decl := do
   let ctx ← read
   match findEnvDecl' ctx.env fid ctx.decls with
   | some decl => pure decl
-  | none      => pure (arbitrary _) -- unreachable if well-formed
+  | none      => pure arbitrary -- unreachable if well-formed
 
 @[inline] def withParams {α : Type} (xs : Array Param) (k : M α) : M α :=
   withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addParams xs }) k
diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index 78a87f0f61..57e6f80dd9 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -22,7 +22,7 @@ structure Context :=
   (env        : Environment)
   (modName    : Name)
   (jpMap      : JPParamsMap := {})
-  (mainFn     : FunId := arbitrary _)
+  (mainFn     : FunId := arbitrary)
   (mainParams : Array Param := #[])
 
 abbrev M := ReaderT Context (EStateM String String)
diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean
index 191777df1d..a5ecab2659 100644
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@@ -30,7 +30,7 @@ structure Context :=
 def getDecl (ctx : Context) (fid : FunId) : Decl :=
   match findEnvDecl' ctx.env fid ctx.decls with
   | some decl => decl
-  | none      => arbitrary _ -- unreachable if well-formed
+  | none      => arbitrary -- unreachable if well-formed
 
 def getVarInfo (ctx : Context) (x : VarId) : VarInfo :=
   match ctx.varMap.find? x with
diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean
index dff0b95ae9..5f1b5dd8d1 100644
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/src/Lean/Compiler/InitAttr.lean
@@ -23,7 +23,7 @@ private def isIOUnit (type : Expr) : Bool :=
 
 /-- Run the initializer for `decl` and store its value for global access. Should only be used while importing. -/
 @[extern "lean_run_init"]
-unsafe constant runInit (env : @& Environment) (opts : @& Options) (decl initDecl : @& Name) : IO Unit := arbitrary _
+unsafe constant runInit (env : @& Environment) (opts : @& Options) (decl initDecl : @& Name) : IO Unit
 
 unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) : IO (ParametricAttribute Name) :=
   registerParametricAttribute {
@@ -56,7 +56,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) : IO
   }
 
 @[implementedBy registerInitAttrUnsafe]
-constant registerInitAttr (attrName : Name) (runAfterImport : Bool) : IO (ParametricAttribute Name) := arbitrary _
+constant registerInitAttr (attrName : Name) (runAfterImport : Bool) : IO (ParametricAttribute Name)
 
 builtin_initialize regularInitAttr : ParametricAttribute Name ← registerInitAttr `init true
 builtin_initialize builtinInitAttr : ParametricAttribute Name ← registerInitAttr `builtinInit false
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 7efa9275d0..a37c896275 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -20,7 +20,7 @@ structure State :=
   (ngen            : NameGenerator := {})
   (traceState      : TraceState    := {})
 
-instance : Inhabited State := ⟨{ env := arbitrary _ }⟩
+instance : Inhabited State := ⟨{ env := arbitrary }⟩
 
 structure Context :=
   (options        : Options := {})
@@ -30,7 +30,7 @@ structure Context :=
 
 abbrev CoreM := ReaderT Context $ StateRefT State (EIO Exception)
 
-instance : Inhabited (CoreM α) := ⟨fun _ _ => throw $ arbitrary _⟩
+instance : Inhabited (CoreM α) := ⟨fun _ _ => throw arbitrary⟩
 
 instance : MonadRef CoreM := {
   getRef  := do let ctx ← read; pure ctx.ref,
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index 4ff4039cfd..cc3ad10181 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -26,7 +26,7 @@ private def initOptionDeclsRef : IO (IO.Ref OptionDecls) :=
   IO.mkRef (mkNameMap OptionDecl)
 
 @[builtinInit initOptionDeclsRef]
-private constant optionDeclsRef : IO.Ref OptionDecls := arbitrary _
+private constant optionDeclsRef : IO.Ref OptionDecls
 
 @[export lean_register_option]
 def registerOption (name : Name) (decl : OptionDecl) : IO Unit := do
diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index f40dc1aee3..320e926b9d 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -64,7 +64,7 @@ structure ConstantVal :=
   (lparams : List Name)
   (type : Expr)
 
-instance : Inhabited ConstantVal := ⟨{ name := arbitrary _, lparams := arbitrary _, type := arbitrary _ }⟩
+instance : Inhabited ConstantVal := ⟨{ name := arbitrary, lparams := arbitrary, type := arbitrary }⟩
 
 structure AxiomVal extends ConstantVal :=
   (isUnsafe : Bool)
@@ -228,7 +228,7 @@ def mkConstructorValEx (name : Name) (lparams : List Name) (type : Expr) (induct
 @[export lean_constructor_val_is_unsafe] def ConstructorVal.isUnsafeEx (v : ConstructorVal) : Bool := v.isUnsafe
 
 instance : Inhabited ConstructorVal :=
-  ⟨{ toConstantVal := arbitrary _, induct := arbitrary _, cidx := 0, nparams := 0, nfields := 0, isUnsafe := true }⟩
+  ⟨{ toConstantVal := arbitrary, induct := arbitrary, cidx := 0, nparams := 0, nfields := 0, isUnsafe := true }⟩
 
 /-- Information for reducing a recursor -/
 structure RecursorRule :=
diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 9652626c3f..9052b5fbb0 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -95,7 +95,7 @@ builtin_initialize delabFailureId : InternalExceptionId ← registerInternalExce
 abbrev DelabM := ReaderT Context MetaM
 abbrev Delab := DelabM Syntax
 
-instance {α} : Inhabited (DelabM α) := ⟨throw $ arbitrary _⟩
+instance {α} : Inhabited (DelabM α) := ⟨throw arbitrary⟩
 
 @[inline] protected def orElse {α} (d₁ d₂ : DelabM α) : DelabM α := do
 catchInternalId delabFailureId d₁ (fun _ => d₂)
@@ -110,8 +110,8 @@ instance {α} : OrElse (DelabM α) := ⟨Delaborator.orElse⟩
 -- Macro scopes in the delaborator output are ultimately ignored by the pretty printer,
 -- so give a trivial implementation.
 instance : MonadQuotation DelabM := {
-  getCurrMacroScope   := pure $ arbitrary _,
-  getMainModule       := pure $ arbitrary _,
+  getCurrMacroScope   := pure arbitrary,
+  getMainModule       := pure arbitrary,
   withFreshMacroScope := fun x => x
 }
 
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index b5e48f1777..825cf8f3b3 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -18,7 +18,7 @@ inductive Arg :=
   | stx  (val : Syntax)
   | expr (val : Expr)
 
-instance : Inhabited Arg := ⟨Arg.stx (arbitrary _)⟩
+instance : Inhabited Arg := ⟨Arg.stx arbitrary⟩
 
 instance : ToString Arg := ⟨fun
   | Arg.stx  val => toString val
@@ -33,7 +33,7 @@ structure NamedArg :=
 instance : ToString NamedArg :=
   ⟨fun s => "(" ++ toString s.name ++ " := " ++ toString s.val ++ ")"⟩
 
-instance : Inhabited NamedArg := ⟨{ name := arbitrary _, val := arbitrary _ }⟩
+instance : Inhabited NamedArg := ⟨{ name := arbitrary, val := arbitrary }⟩
 
 def throwInvalidNamedArg {α} (namedArg : NamedArg) (fn? : Option Name) : TermElabM α :=
   withRef namedArg.ref $ match fn? with
diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index 4626f4d51d..c669cc30ca 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -14,7 +14,7 @@ structure Attribute :=
 instance : ToFormat Attribute := ⟨fun attr =>
   Format.bracket "@[" (toString attr.name ++ (if attr.args.isMissing then "" else toString attr.args)) "]"⟩
 
-instance : Inhabited Attribute := ⟨{ name := arbitrary _ }⟩
+instance : Inhabited Attribute := ⟨{ name := arbitrary }⟩
 
 def elabAttr {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (stx : Syntax) : m Attribute := do
   -- rawIdent >> many attrArg
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 61d1dcd74c..f50ca8a611 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -32,7 +32,7 @@ structure State :=
   (nextInstIdx    : Nat := 1) -- for generating anonymous instance names
   (ngen           : NameGenerator := {})
 
-instance : Inhabited State := ⟨{ env := arbitrary _, maxRecDepth := 0 }⟩
+instance : Inhabited State := ⟨{ env := arbitrary, maxRecDepth := 0 }⟩
 
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := {
   env := env,
@@ -248,7 +248,7 @@ def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab := fun st
 private def getVarDecls (s : State) : Array Syntax :=
   s.scopes.head!.varDecls
 
-instance {α} : Inhabited (CommandElabM α) := ⟨throw $ arbitrary _⟩
+instance {α} : Inhabited (CommandElabM α) := ⟨throw arbitrary⟩
 
 private def mkMetaContext : Meta.Context := {
   config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 6088871704..fa2aede4f4 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -144,10 +144,10 @@ inductive Code :=
   | jmp          (ref : Syntax) (jpName : Name) (args : Array Syntax)
 
 instance : Inhabited Code :=
-  ⟨Code.«break» (arbitrary _)⟩
+  ⟨Code.«break» arbitrary⟩
 
 instance : Inhabited (Alt Code) :=
-  ⟨{ ref := arbitrary _, vars := #[], patterns := arbitrary _, rhs := arbitrary _ }⟩
+  ⟨{ ref := arbitrary, vars := #[], patterns := arbitrary, rhs := arbitrary }⟩
 
 /- A code block, and the collection of variables updated by it. -/
 structure CodeBlock :=
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index d45d3772c1..a3ff70fa08 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -45,7 +45,7 @@ structure CtorView :=
   (type?     : Option Syntax)
 
 instance : Inhabited CtorView :=
-  ⟨{ ref := arbitrary _, modifiers := {}, inferMod := false, declName := arbitrary _, binders := arbitrary _, type? := none }⟩
+  ⟨{ ref := arbitrary, modifiers := {}, inferMod := false, declName := arbitrary, binders := arbitrary, type? := none }⟩
 
 structure InductiveView :=
   (ref           : Syntax)
@@ -58,8 +58,8 @@ structure InductiveView :=
   (ctors         : Array CtorView)
 
 instance : Inhabited InductiveView :=
-  ⟨{ ref := arbitrary _, modifiers := {}, shortDeclName := arbitrary _, declName := arbitrary _,
-     levelNames := [], binders := arbitrary _, type? := none, ctors := #[] }⟩
+  ⟨{ ref := arbitrary, modifiers := {}, shortDeclName := arbitrary, declName := arbitrary,
+     levelNames := [], binders := arbitrary, type? := none, ctors := #[] }⟩
 
 structure ElabHeaderResult :=
   (view       : InductiveView)
@@ -69,7 +69,7 @@ structure ElabHeaderResult :=
   (type       : Expr)
 
 instance : Inhabited ElabHeaderResult :=
-  ⟨{ view := arbitrary _, lctx := arbitrary _, localInsts := arbitrary _, params := #[], type := arbitrary _ }⟩
+  ⟨{ view := arbitrary, lctx := arbitrary, localInsts := arbitrary, params := #[], type := arbitrary }⟩
 
 private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) := do
   if h : i < views.size then
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 9275199354..b563c849af 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -269,7 +269,7 @@ structure Context :=
   (args          : List Arg)
   (newArgs       : Array Syntax := #[])
 
-instance : Inhabited Context := ⟨⟨arbitrary _, none, false, false, #[], 0, #[], [], #[]⟩⟩
+instance : Inhabited Context := ⟨⟨arbitrary, none, false, false, #[], 0, #[], [], #[]⟩⟩
 
 private def isDone (ctx : Context) : Bool :=
   ctx.paramDeclIdx ≥ ctx.paramDecls.size
@@ -626,7 +626,7 @@ private def mkLocalDeclFor (mvar : Expr) : M Pattern := do
        If this generates problems in the future, we should update the metavariable declarations. -/
     assignExprMVar mvarId (mkFVar fvarId)
     let userName ← liftM $ mkFreshBinderName
-    let newDecl := LocalDecl.cdecl (arbitrary _) fvarId userName type BinderInfo.default;
+    let newDecl := LocalDecl.cdecl arbitrary fvarId userName type BinderInfo.default;
     modify fun s =>
       { s with
         newLocals  := s.newLocals.insert fvarId,
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index d5b4b91e04..462e16bcf7 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -24,7 +24,7 @@ structure DefViewElabHeader :=
   (valueStx      : Syntax)
 
 instance : Inhabited DefViewElabHeader :=
-  ⟨⟨arbitrary _, {}, DefKind.«def», arbitrary _, arbitrary _, [], 0, arbitrary _, arbitrary _⟩⟩
+  ⟨⟨arbitrary, {}, DefKind.«def», arbitrary, arbitrary, [], 0, arbitrary, arbitrary ⟩⟩
 
 namespace Term
 
@@ -441,7 +441,7 @@ private def pushLocalDecl (toProcess : Array FVarId) (fvarId : FVarId) (userName
     : StateRefT ClosureState TermElabM (Array FVarId) := do
   let type ← preprocess type
   modify fun s => { s with
-    newLocalDecls := s.newLocalDecls.push $ LocalDecl.cdecl (arbitrary _) fvarId userName type bi,
+    newLocalDecls := s.newLocalDecls.push $ LocalDecl.cdecl arbitrary fvarId userName type bi,
     exprArgs      := s.exprArgs.push (mkFVar fvarId)
   }
   pure $ pushNewVars toProcess (collectFVars {} type)
@@ -469,7 +469,7 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu
         let type ← preprocess type
         let val  ← preprocess val
         modify fun s => { s with
-          newLetDecls   := s.newLetDecls.push $ LocalDecl.ldecl (arbitrary _) fvarId userName type val false,
+          newLetDecls   := s.newLetDecls.push $ LocalDecl.ldecl arbitrary fvarId userName type val false,
           /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of fvarId
              at `newLocalDecls` and `localDecls` -/
           newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl fvarId val),
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 77de270d4b..cb770089af 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -26,7 +26,7 @@ structure PreDefinition :=
   (value     : Expr)
 
 instance : Inhabited PreDefinition :=
-  ⟨⟨DefKind.«def», [], {}, arbitrary _, arbitrary _, arbitrary _⟩⟩
+  ⟨⟨DefKind.«def», [], {}, arbitrary, arbitrary, arbitrary⟩⟩
 
 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 1095a6a49d..6683395437 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -173,7 +173,7 @@ inductive FieldLHS :=
   | fieldIndex (ref : Syntax) (idx : Nat)
   | modifyOp   (ref : Syntax) (index : Syntax)
 
-instance : Inhabited FieldLHS := ⟨FieldLHS.fieldName (arbitrary _) (arbitrary _)⟩
+instance : Inhabited FieldLHS := ⟨FieldLHS.fieldName arbitrary arbitrary⟩
 instance : ToFormat FieldLHS := ⟨fun lhs =>
   match lhs with
   | FieldLHS.fieldName _ n  => fmt n
@@ -191,7 +191,7 @@ structure Field (σ : Type) :=
   (val : FieldVal σ)
   (expr? : Option Expr := none)
 
-instance {σ} : Inhabited (Field σ) := ⟨⟨arbitrary _, [], FieldVal.term (arbitrary _), arbitrary _⟩⟩
+instance {σ} : Inhabited (Field σ) := ⟨⟨arbitrary, [], FieldVal.term arbitrary, arbitrary⟩⟩
 
 def Field.isSimple {σ} : Field σ → Bool
   | { lhs := [_], .. } => true
@@ -200,7 +200,7 @@ def Field.isSimple {σ} : Field σ → Bool
 inductive Struct :=
   | mk (ref : Syntax) (structName : Name) (fields : List (Field Struct)) (source : Source)
 
-instance : Inhabited Struct := ⟨⟨arbitrary _, arbitrary _, [], arbitrary _⟩⟩
+instance : Inhabited Struct := ⟨⟨arbitrary, arbitrary, [], arbitrary⟩⟩
 
 abbrev Fields := List (Field Struct)
 
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index da2f69985c..1244f45a45 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -63,7 +63,7 @@ structure StructFieldInfo :=
   (value?   : Option Expr := none)
 
 instance : Inhabited StructFieldInfo :=
-  ⟨{ name := arbitrary _, declName := arbitrary _, fvar := arbitrary _, kind := StructFieldKind.newField }⟩
+  ⟨{ name := arbitrary, declName := arbitrary, fvar := arbitrary, kind := StructFieldKind.newField }⟩
 
 def StructFieldInfo.isFromParent (info : StructFieldInfo) : Bool :=
   match info.kind with
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 88f00ad68f..d1c0e8d0bd 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -71,7 +71,7 @@ structure SavedState :=
   (term   : Term.State)
   (tactic : State)
 
-instance : Inhabited SavedState := ⟨⟨arbitrary _, arbitrary _, arbitrary _, arbitrary _⟩⟩
+instance : Inhabited SavedState := ⟨⟨arbitrary, arbitrary, arbitrary, arbitrary⟩⟩
 
 def saveAllState : TacticM SavedState := do
   pure { core := (← getThe Core.State), meta := (← getThe Meta.State), term := (← getThe Term.State), tactic := (← get) }
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index a6742698d6..c9b5886823 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -146,14 +146,14 @@ abbrev TermElab  := Syntax → Option Expr → TermElabM Expr
 
 open Meta
 
-instance {α} : Inhabited (TermElabM α) := ⟨throw $ arbitrary _⟩
+instance {α} : Inhabited (TermElabM α) := ⟨throw arbitrary⟩
 
 structure SavedState :=
   (core   : Core.State)
   (meta   : Meta.State)
   («elab» : State)
 
-instance : Inhabited SavedState := ⟨⟨arbitrary _, arbitrary _, arbitrary _⟩⟩
+instance : Inhabited SavedState := ⟨⟨arbitrary, arbitrary, arbitrary⟩⟩
 
 def saveAllState : TermElabM SavedState := do
   pure { core := (← getThe Core.State), meta := (← getThe Meta.State), «elab» := (← get) }
@@ -166,7 +166,7 @@ def SavedState.restore (s : SavedState) : TermElabM Unit := do
   setTraceState traceState
 
 abbrev TermElabResult := EStateM.Result Exception SavedState Expr
-instance : Inhabited TermElabResult := ⟨EStateM.Result.ok (arbitrary _) (arbitrary _)⟩
+instance : Inhabited TermElabResult := ⟨EStateM.Result.ok arbitrary arbitrary⟩
 
 def setMessageLog (messages : MessageLog) : TermElabM Unit :=
   modify fun s => { s with messages := messages }
@@ -1276,7 +1276,7 @@ fun stx _ =>
 
 private def mkSomeContext : Context := {
   fileName      := "<TermElabM>",
-  fileMap       := arbitrary _,
+  fileMap       := arbitrary,
   currNamespace := Name.anonymous
 }
 
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 4a96a38ae2..470bd977ca 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -40,13 +40,13 @@ def CompactedRegion := USize
 unsafe constant CompactedRegion.free : CompactedRegion → IO Unit
 
 /- Environment fields that are not used often. -/
-structure EnvironmentHeader :=
-  (trustLevel   : UInt32       := 0)
-  (quotInit     : Bool         := false)
-  (mainModule   : Name         := arbitrary _)
-  (imports      : Array Import := #[]) -- direct imports
-  (regions      : Array CompactedRegion := #[]) -- compacted regions of all imported modules
-  (moduleNames  : NameSet      := {})  -- names of all imported modules
+structure EnvironmentHeader where
+  trustLevel   : UInt32       := 0
+  quotInit     : Bool         := false
+  mainModule   : Name         := arbitrary
+  imports      : Array Import := #[] -- direct imports
+  regions      : Array CompactedRegion := #[] -- compacted regions of all imported modules
+  moduleNames  : NameSet      := {}  -- names of all imported modules
 
 open Std (HashMap)
 
@@ -165,7 +165,7 @@ structure Ext (σ : Type) :=
   (idx       : Nat)
   (mkInitial : IO σ)
 
-instance {σ} : Inhabited (Ext σ) := ⟨{idx := 0, mkInitial := arbitrary _ }⟩
+instance {σ} : Inhabited (Ext σ) := ⟨{idx := 0, mkInitial := arbitrary }⟩
 
 private def mkEnvExtensionsRef : IO (IO.Ref (Array (Ext EnvExtensionState))) := IO.mkRef #[]
 @[builtinInit mkEnvExtensionsRef] private constant envExtensionsRef : IO.Ref (Array (Ext EnvExtensionState))
@@ -202,7 +202,7 @@ def mkInitialExtStates : IO (Array EnvExtensionState) := do
 
 unsafe def imp : EnvExtensionInterface := {
   ext                := Ext,
-  inhabitedExt       := fun _ => ⟨arbitrary _⟩,
+  inhabitedExt       := fun _ => ⟨arbitrary⟩,
   registerExt        := registerExt,
   setState           := setState,
   modifyState        := modifyState,
@@ -278,17 +278,17 @@ structure PersistentEnvExtension (α : Type) (β : Type) (σ : Type) :=
   (statsFn         : σ → Format)
 
 /- Opaque persistent environment extension entry. -/
-constant EnvExtensionEntrySpec : PointedType.{0} := arbitrary _
+constant EnvExtensionEntrySpec : PointedType.{0}
 def EnvExtensionEntry : Type := EnvExtensionEntrySpec.type
 instance : Inhabited EnvExtensionEntry := ⟨EnvExtensionEntrySpec.val⟩
 
 instance {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
-  ⟨{importedEntries := #[], state := arbitrary _ }⟩
+  ⟨{importedEntries := #[], state := arbitrary }⟩
 
 instance {α β σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α β σ) := ⟨{
-   toEnvExtension := arbitrary _,
-   name := arbitrary _,
-   addImportedFn := fun _ => arbitrary _,
+   toEnvExtension := arbitrary,
+   name := arbitrary,
+   addImportedFn := fun _ => arbitrary,
    addEntryFn := fun s _ => s,
    exportEntriesFn := fun _ => #[],
    statsFn := fun _ => Format.nil
@@ -427,7 +427,7 @@ structure ModuleData :=
   (entries    : Array (Name × Array EnvExtensionEntry))
 
 instance : Inhabited ModuleData :=
-  ⟨{imports := arbitrary _, constants := arbitrary _, entries := arbitrary _}⟩
+  ⟨{imports := arbitrary, constants := arbitrary, entries := arbitrary }⟩
 
 @[extern 3 "lean_save_module_data"]
 constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index 4d0604de00..e2eb5e33a8 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -23,7 +23,7 @@ def Exception.getRef : Exception → Syntax
   | Exception.error ref _   => ref
   | Exception.internal _  _ => Syntax.missing
 
-instance : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
+instance : Inhabited Exception := ⟨Exception.error arbitrary arbitrary⟩
 
 /- Similar to `AddMessageContext`, but for error messages.
    The default instance just uses `AddMessageContext`.
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 151be6ebfe..bf359d8aa5 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -184,8 +184,8 @@ inductive Expr :=
 
 namespace Expr
 
-instance : Inhabited Expr :=
-  ⟨sort (arbitrary _) (arbitrary _)⟩
+instance : Inhabited Expr where
+  default := sort arbitrary arbitrary
 
 @[inline] def data : Expr → Data
   | bvar _ d        => d
@@ -729,7 +729,8 @@ protected def beq : ExprStructEq → ExprStructEq → Bool
 protected def hash : ExprStructEq → USize
   | ⟨e⟩ => e.hash
 
-instance : Inhabited ExprStructEq := ⟨{ val := arbitrary _ }⟩
+instance : Inhabited ExprStructEq where
+  default := { val := arbitrary }
 instance : BEq ExprStructEq := ⟨ExprStructEq.beq⟩
 instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩
 instance : ToString ExprStructEq := ⟨fun e => toString e.val⟩
diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index 243a60a012..396fd01559 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -39,7 +39,7 @@ structure Def (γ : Type) :=
       | none    => throwError "invalid attribute argument, expected identifier")
 
 instance {γ} : Inhabited (Def γ) :=
-  ⟨{ builtinName := arbitrary _, name := arbitrary _, descr := arbitrary _, valueTypeName := arbitrary _ }⟩
+  ⟨{ builtinName := arbitrary, name := arbitrary, descr := arbitrary, valueTypeName := arbitrary }⟩
 
 structure OLeanEntry :=
   (key  : Key)
@@ -77,7 +77,7 @@ def Table.insert {γ : Type} (table : Table γ) (k : Key) (v : γ) : Table γ :=
 instance {γ} : Inhabited (ExtensionState γ) := ⟨{}⟩
 
 instance {γ} : Inhabited (KeyedDeclsAttribute γ) :=
-  ⟨{ defn := arbitrary _, tableRef := arbitrary _, ext := arbitrary _ }⟩
+  ⟨{ defn := arbitrary, tableRef := arbitrary, ext := arbitrary }⟩
 
 private def mkInitial {γ} (tableRef : IO.Ref (Table γ)) : IO (ExtensionState γ) := do
   let table ← tableRef.get
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index a0dcce2811..e519e7efc3 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -199,7 +199,7 @@ def toNat (lvl : Level) : Option Nat :=
   | _      => none
 
 @[extern "lean_level_eq"]
-protected constant beq (a : @& Level) (b : @& Level) : Bool := arbitrary _
+protected constant beq (a : @& Level) (b : @& Level) : Bool
 
 instance : BEq Level := ⟨Level.beq⟩
 
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 1c3a251b2a..dcc4b44225 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -25,7 +25,7 @@ def LocalDecl.binderInfoEx : LocalDecl → BinderInfo
   | _                          => BinderInfo.default
 
 namespace LocalDecl
-instance : Inhabited LocalDecl := ⟨ldecl (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) false⟩
+instance : Inhabited LocalDecl := ⟨ldecl arbitrary arbitrary arbitrary arbitrary arbitrary false⟩
 
 def isLet : LocalDecl → Bool
   | cdecl .. => false
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 7082716b33..ee3f631f08 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -62,7 +62,7 @@ def isNest : MessageData → Bool
   | nest _ _ => true
   | _        => false
 
-instance : Inhabited MessageData := ⟨MessageData.ofFormat (arbitrary _)⟩
+instance : Inhabited MessageData := ⟨MessageData.ofFormat arbitrary⟩
 
 def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext := {
   env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts,
@@ -154,7 +154,7 @@ protected def toString (msg : Message) : IO String := do
      | MessageSeverity.error => "error: ") ++
     (if msg.caption == "" then "" else msg.caption ++ ":\n") ++ str)
 
-instance : Inhabited Message := ⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary _}⟩
+instance : Inhabited Message := ⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary }⟩
 
 @[export lean_message_pos] def getPostEx (msg : Message) : Position := msg.pos
 @[export lean_message_severity] def getSeverityEx (msg : Message) : MessageSeverity := msg.severity
diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean
index 35c416349a..646baf36c2 100644
--- a/src/Lean/Meta/AbstractMVars.lean
+++ b/src/Lean/Meta/AbstractMVars.lean
@@ -12,7 +12,7 @@ structure AbstractMVarsResult :=
   (numMVars   : Nat)
   (expr       : Expr)
 
-instance : Inhabited AbstractMVarsResult := ⟨⟨#[], 0, arbitrary _⟩⟩
+instance : Inhabited AbstractMVarsResult := ⟨⟨#[], 0, arbitrary⟩⟩
 
 def AbstractMVarsResult.beq (r₁ r₂ : AbstractMVarsResult) : Bool :=
   r₁.paramNames == r₂.paramNames && r₁.numMVars == r₂.numMVars && r₁.expr == r₂.expr
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 806878f056..4826a663e1 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -75,7 +75,7 @@ structure InfoCacheKey :=
   (nargs?       : Option Nat)
 
 namespace InfoCacheKey
-instance : Inhabited InfoCacheKey := ⟨⟨arbitrary _, arbitrary _, arbitrary _⟩⟩
+instance : Inhabited InfoCacheKey := ⟨⟨arbitrary, arbitrary, arbitrary⟩⟩
 instance : Hashable InfoCacheKey :=
   ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) $ mixHash (hash expr) (hash nargs)⟩
 instance : BEq InfoCacheKey :=
@@ -114,7 +114,7 @@ structure Context :=
 abbrev MetaM  := ReaderT Context $ StateRefT State CoreM
 
 instance : Inhabited (MetaM α) := {
-  default := fun _ _ => arbitrary _
+  default := fun _ _ => arbitrary
 }
 
 instance : MonadLCtx MetaM := {
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index 128951060f..fb16300a54 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -102,7 +102,7 @@ structure ToProcessElement :=
   (newFVarId : FVarId)
 
 instance : Inhabited ToProcessElement :=
-  ⟨⟨arbitrary _, arbitrary _⟩⟩
+  ⟨⟨arbitrary, arbitrary⟩⟩
 
 structure Context :=
   (zeta : Bool)
@@ -205,7 +205,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do
     let newFVarId ← mkFreshFVarId
     let userName ← mkNextUserName
     modify fun s => { s with
-      newLocalDeclsForMVars := s.newLocalDeclsForMVars.push $ LocalDecl.cdecl (arbitrary _) newFVarId userName type BinderInfo.default,
+      newLocalDeclsForMVars := s.newLocalDeclsForMVars.push $ LocalDecl.cdecl arbitrary newFVarId userName type BinderInfo.default,
       exprMVarArgs          := s.exprMVarArgs.push e
     }
     return mkFVar newFVarId
@@ -250,7 +250,7 @@ def pushFVarArg (e : Expr) : ClosureM Unit :=
 
 def pushLocalDecl (newFVarId : FVarId) (userName : Name) (type : Expr) (bi := BinderInfo.default) : ClosureM Unit := do
   let type ← collectExpr type
-  modify fun s => { s with newLocalDecls := s.newLocalDecls.push $ LocalDecl.cdecl (arbitrary _) newFVarId userName type bi }
+  modify fun s => { s with newLocalDecls := s.newLocalDecls.push <| LocalDecl.cdecl arbitrary newFVarId userName type bi }
 
 partial def process : ClosureM Unit := do
   match (← pickNextToProcess?) with
@@ -279,7 +279,7 @@ partial def process : ClosureM Unit := do
         /- Dependent let-decl -/
         let type ← collectExpr type
         let val  ← collectExpr val
-        modify fun s => { s with newLetDecls := s.newLetDecls.push $ LocalDecl.ldecl (arbitrary _) newFVarId userName type val false }
+        modify fun s => { s with newLetDecls := s.newLetDecls.push <| LocalDecl.ldecl arbitrary newFVarId userName type val false }
         /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of newFVarId
            at `newLocalDecls` -/
         modify fun s => { s with newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl newFVarId val) }
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index e969c711fb..4c9e6b7ace 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -218,7 +218,7 @@ private partial def insertAux {α} [BEq α] (keys : Array Key) (v : α) : Nat 
           (fun a b => a.1 < b.1)
           (fun ⟨_, s⟩ => let c := insertAux keys v (i+1) s; (k, c)) -- merge with existing
           (fun _ => let c := createNodes keys v (i+1); (k, c))
-          (k, arbitrary _)
+          (k, arbitrary)
       Trie.node vs c
     else
       Trie.node (insertVal vs v) cs
@@ -315,7 +315,7 @@ private partial def getMatchAux {α} : Array Expr → Trie α → Array α → M
       match k with
       | Key.star => visitStarChild result
       | _ =>
-        match cs.binSearch (k, arbitrary _) (fun a b => a.1 < b.1) with
+        match cs.binSearch (k, arbitrary) (fun a b => a.1 < b.1) with
         | none   => visitStarChild result
         | some c =>
           let result ← visitStarChild result
@@ -355,7 +355,7 @@ private partial def getUnifyAux {α} : Nat → Array Expr → Trie α → (Array
         let first := cs[0]
         let visitStarChild (result : Array α) : MetaM (Array α) :=
           if first.1 == Key.star then getUnifyAux 0 todo first.2 result else pure result
-        match cs.binSearch (k, arbitrary _) (fun a b => a.1 < b.1) with
+        match cs.binSearch (k, arbitrary) (fun a b => a.1 < b.1) with
         | none   => visitStarChild result
         | some c =>
           let result ← visitStarChild result
diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean
index f7738ab30d..90ec8e3d13 100644
--- a/src/Lean/Meta/Match/Basic.lean
+++ b/src/Lean/Meta/Match/Basic.lean
@@ -18,7 +18,7 @@ inductive Pattern : Type :=
 
 namespace Pattern
 
-instance : Inhabited Pattern := ⟨Pattern.inaccessible (arbitrary _)⟩
+instance : Inhabited Pattern := ⟨Pattern.inaccessible arbitrary⟩
 
 partial def toMessageData : Pattern → MessageData
   | inaccessible e         => m!".({e})"
@@ -108,7 +108,7 @@ structure Alt :=
 
 namespace Alt
 
-instance : Inhabited Alt := ⟨⟨arbitrary _, 0, arbitrary _, [], []⟩⟩
+instance : Inhabited Alt := ⟨⟨arbitrary, 0, arbitrary, [], []⟩⟩
 
 partial def toMessageData (alt : Alt) : MetaM MessageData := do
   withExistingLocalDecls alt.fvarDecls do
@@ -237,7 +237,7 @@ structure Problem :=
 def withGoalOf {α} (p : Problem) (x : MetaM α) : MetaM α :=
   withMVarContext p.mvarId x
 
-instance : Inhabited Problem := ⟨{ mvarId := arbitrary _, vars := [], alts := [], examples := []}⟩
+instance : Inhabited Problem := ⟨{ mvarId := arbitrary, vars := [], alts := [], examples := []}⟩
 
 def Problem.toMessageData (p : Problem) : MetaM MessageData :=
   withGoalOf p do
diff --git a/src/Lean/Meta/Match/CaseArraySizes.lean b/src/Lean/Meta/Match/CaseArraySizes.lean
index 1307da144b..954737fc13 100644
--- a/src/Lean/Meta/Match/CaseArraySizes.lean
+++ b/src/Lean/Meta/Match/CaseArraySizes.lean
@@ -15,7 +15,7 @@ structure CaseArraySizesSubgoal :=
   (subst  : FVarSubst := {})
 
 instance : Inhabited CaseArraySizesSubgoal :=
-  ⟨{ mvarId := arbitrary _ }⟩
+  ⟨{ mvarId := arbitrary }⟩
 
 def getArrayArgType (a : Expr) : MetaM Expr := do
   let aType ← inferType a
diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean
index 82bcca4aff..83aaa37704 100644
--- a/src/Lean/Meta/Match/CaseValues.lean
+++ b/src/Lean/Meta/Match/CaseValues.lean
@@ -14,7 +14,7 @@ structure CaseValueSubgoal :=
   (subst  : FVarSubst := {})
 
 instance : Inhabited CaseValueSubgoal :=
-  ⟨{ mvarId := arbitrary _, newH := arbitrary _ }⟩
+  ⟨{ mvarId := arbitrary, newH := arbitrary }⟩
 
 /--
   Split goal `... |- C x` into two subgoals
@@ -65,7 +65,7 @@ structure CaseValuesSubgoal :=
   (subst  : FVarSubst := {})
 
 instance : Inhabited CaseValuesSubgoal :=
-  ⟨{ mvarId := arbitrary _ }⟩
+  ⟨{ mvarId := arbitrary }⟩
 
 /--
   Split goal `... |- C x` into values.size + 1 subgoals
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 63ba4307f9..6e336c7046 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -30,7 +30,7 @@ structure GeneratorNode :=
   (instances       : Array Expr)
   (currInstanceIdx : Nat)
 
-instance : Inhabited GeneratorNode := ⟨⟨arbitrary _, arbitrary _, arbitrary _, arbitrary _, 0⟩⟩
+instance : Inhabited GeneratorNode := ⟨⟨arbitrary, arbitrary, arbitrary, arbitrary, 0⟩⟩
 
 structure ConsumerNode :=
   (mvar     : Expr)
@@ -38,7 +38,7 @@ structure ConsumerNode :=
   (mctx     : MetavarContext)
   (subgoals : List Expr)
 
-instance : Inhabited ConsumerNode := ⟨⟨arbitrary _, arbitrary _, arbitrary _, []⟩⟩
+instance : Inhabited ConsumerNode := ⟨⟨arbitrary, arbitrary, arbitrary, []⟩⟩
 
 inductive Waiter :=
   | consumerNode : ConsumerNode → Waiter
@@ -134,7 +134,7 @@ structure Answer :=
   (result     : AbstractMVarsResult)
   (resultType : Expr)
 
-instance : Inhabited Answer := ⟨⟨arbitrary _, arbitrary _⟩⟩
+instance : Inhabited Answer := ⟨⟨arbitrary, arbitrary⟩⟩
 
 structure TableEntry :=
   (waiters : Array Waiter)
@@ -159,7 +159,7 @@ abbrev SynthM := StateRefT State MetaM
   monadMap @f
 
 instance {α} : Inhabited (SynthM α) :=
-  ⟨fun _ => arbitrary _⟩
+  ⟨fun _ => arbitrary⟩
 
 /-- Return globals and locals instances that may unify with `type` -/
 def getInstances (type : Expr) : MetaM (Array Expr) := do
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index 32ac1b3134..d9aa61f657 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -40,7 +40,7 @@ structure InductionSubgoal :=
   (fields : Array Expr := #[])
   (subst  : FVarSubst := {})
 
-instance : Inhabited InductionSubgoal := ⟨{ mvarId := arbitrary _ }⟩
+instance : Inhabited InductionSubgoal := ⟨{ mvarId := arbitrary }⟩
 
 private def getTypeBody (mvarId : MVarId) (type : Expr) (x : Expr) : MetaM Expr := do
   let type ← whnfForall type
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 55ea862d91..2c4e412777 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -414,8 +414,8 @@ def whnfUntil (e : Expr) (declName : Name) : m (Option Expr) := liftMetaM do
 
 unsafe def reduceBoolNativeUnsafe (constName : Name) : MetaM Bool := evalConstCheck Bool `Bool constName
 unsafe def reduceNatNativeUnsafe (constName : Name) : MetaM Nat := evalConstCheck Nat `Nat constName
-@[implementedBy reduceBoolNativeUnsafe] constant reduceBoolNative (constName : Name) : MetaM Bool := arbitrary _
-@[implementedBy reduceNatNativeUnsafe] constant reduceNatNative (constName : Name) : MetaM Nat := arbitrary _
+@[implementedBy reduceBoolNativeUnsafe] constant reduceBoolNative (constName : Name) : MetaM Bool
+@[implementedBy reduceNatNativeUnsafe] constant reduceNatNative (constName : Name) : MetaM Nat
 
 def reduceNative? (e : Expr) : MetaM (Option Expr) :=
   match e with
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index d6b7b4852f..8747a98ee1 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -261,7 +261,7 @@ structure MetavarDecl :=
 def mkMetavarDeclEx (userName : Name) (lctx : LocalContext) (type : Expr) (depth : Nat) (localInstances : LocalInstances) (kind : MetavarKind) : MetavarDecl :=
   { userName := userName, lctx := lctx, type := type, depth := depth, localInstances := localInstances, kind := kind }
 
-instance : Inhabited MetavarDecl := ⟨{ lctx := arbitrary _, type := arbitrary _, depth := 0, localInstances := #[], kind := MetavarKind.natural }⟩
+instance : Inhabited MetavarDecl := ⟨{ lctx := arbitrary, type := arbitrary, depth := 0, localInstances := #[], kind := MetavarKind.natural }⟩
 
 /--
   A delayed assignment for a metavariable `?m`. It represents an assignment of the form
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index c2e29eb58e..12fd483dbe 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -117,7 +117,7 @@ structure InputContext :=
   (fileMap  : FileMap)
 
 instance : Inhabited InputContext := ⟨{
-  input := "", fileName := "", fileMap := arbitrary _
+  input := "", fileName := "", fileMap := arbitrary
 }⟩
 
 structure ParserContext extends InputContext :=
diff --git a/src/Lean/ParserCompiler/Attribute.lean b/src/Lean/ParserCompiler/Attribute.lean
index 3e279dfe0c..9b38a42689 100644
--- a/src/Lean/ParserCompiler/Attribute.lean
+++ b/src/Lean/ParserCompiler/Attribute.lean
@@ -40,7 +40,7 @@ def registerCombinatorAttribute (name : Name) (descr : String)
 
 namespace CombinatorAttribute
 
-instance : Inhabited CombinatorAttribute := ⟨{impl := arbitrary _, ext := arbitrary _}⟩
+instance : Inhabited CombinatorAttribute := ⟨{ impl := arbitrary, ext := arbitrary }⟩
 
 def getDeclFor? (attr : CombinatorAttribute) (env : Environment) (parserDecl : Name) : Option Name :=
   (attr.ext.getState env).find? parserDecl
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index ed913580dc..ef6a69cc96 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -68,7 +68,7 @@ unsafe def mkFormatterAttribute : IO (KeyedDeclsAttribute Formatter) :=
         else throwError ("invalid [formatter] argument, unknown syntax kind '" ++ toString id ++ "'")
       | none    => throwError "invalid [formatter] argument, expected identifier"
   } `Lean.PrettyPrinter.formatterAttribute
-@[builtinInit mkFormatterAttribute] constant formatterAttribute : KeyedDeclsAttribute Formatter := arbitrary _
+@[builtinInit mkFormatterAttribute] constant formatterAttribute : KeyedDeclsAttribute Formatter
 
 unsafe def mkCombinatorFormatterAttribute : IO ParserCompiler.CombinatorAttribute :=
   ParserCompiler.registerCombinatorAttribute
@@ -79,7 +79,7 @@ unsafe def mkCombinatorFormatterAttribute : IO ParserCompiler.CombinatorAttribut
   Note that, unlike with [formatter], this is not a node kind since combinators usually do not introduce their own node kinds.
   The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced
   with `Formatter` in the parameter types."
-@[builtinInit mkCombinatorFormatterAttribute] constant combinatorFormatterAttribute : ParserCompiler.CombinatorAttribute := arbitrary _
+@[builtinInit mkCombinatorFormatterAttribute] constant combinatorFormatterAttribute : ParserCompiler.CombinatorAttribute
 
 namespace Formatter
 
@@ -158,13 +158,13 @@ constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (a
 
 -- break up big mutual recursion
 @[extern "lean_pretty_printer_formatter_interpret_parser_descr"]
-constant interpretParserDescr' : ParserDescr → CoreM Formatter := arbitrary _
+constant interpretParserDescr' : ParserDescr → CoreM Formatter
 
 unsafe def formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter := do
   (← liftM $ runForNodeKind formatterAttribute k interpretParserDescr')
 
 @[implementedBy formatterForKindUnsafe]
-constant formatterForKind (k : SyntaxNodeKind) : Formatter := arbitrary _
+constant formatterForKind (k : SyntaxNodeKind) : Formatter
 
 @[combinatorFormatter Lean.Parser.withAntiquot]
 def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index e59b420799..2cc4cdf21f 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -194,8 +194,8 @@ def visitArgs (x : ParenthesizerM Unit) : ParenthesizerM Unit := do
 -- Macro scopes in the parenthesizer output are ultimately ignored by the pretty printer,
 -- so give a trivial implementation.
 instance : MonadQuotation ParenthesizerM := {
-  getCurrMacroScope   := pure $ arbitrary _,
-  getMainModule       := pure $ arbitrary _,
+  getCurrMacroScope   := pure arbitrary,
+  getMainModule       := pure arbitrary,
   withFreshMacroScope := fun x => x,
 }
 
@@ -270,13 +270,13 @@ def throwError {α} (msg : MessageData) : ParenthesizerM α :=
 
 -- break up big mutual recursion
 @[extern "lean_pretty_printer_parenthesizer_interpret_parser_descr"]
-constant interpretParserDescr' : ParserDescr → CoreM Parenthesizer := arbitrary _
+constant interpretParserDescr' : ParserDescr → CoreM Parenthesizer
 
 unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do
   (← liftM $ runForNodeKind parenthesizerAttribute k interpretParserDescr')
 
 @[implementedBy parenthesizerForKindUnsafe]
-constant parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer := arbitrary _
+constant parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer
 
 @[combinatorParenthesizer Lean.Parser.withAntiquot]
 def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer :=
diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean
index 9b1eb70762..5f23e2dcf0 100644
--- a/src/Lean/ProjFns.lean
+++ b/src/Lean/ProjFns.lean
@@ -22,7 +22,7 @@ def mkProjectionInfoEx (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass :
   def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass
 
 instance : Inhabited ProjectionFunctionInfo :=
-  ⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩
+  ⟨{ ctorName := arbitrary, nparams := arbitrary, i := 0, fromClass := false }⟩
 
 builtin_initialize projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) ←
   registerSimplePersistentEnvExtension {
@@ -42,14 +42,14 @@ namespace Environment
 def getProjectionFnInfo? (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
   match env.getModuleIdxFor? projName with
   | some modIdx =>
-    match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
+    match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary) (fun a b => Name.quickLt a.1 b.1) with
     | some e => some e.2
     | none   => none
   | none        => (projectionFnInfoExt.getState env).find? projName
 
 def isProjectionFn (env : Environment) (n : Name) : Bool :=
   match env.getModuleIdxFor? n with
-  | some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary _) (fun a b => Name.quickLt a.1 b.1)
+  | some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary) (fun a b => Name.quickLt a.1 b.1)
   | none        => (projectionFnInfoExt.getState env).contains n
 
 /-- If `projName` is the name of a projection function, return the associated structure name -/
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 9642e0eb4b..cdb3e99ce9 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -289,7 +289,7 @@ def setCur (t : Traverser) (stx : Syntax) : Traverser :=
 /-- Advance to the `idx`-th child of the current node. -/
 def down (t : Traverser) (idx : Nat) : Traverser :=
   if idx < t.cur.getNumArgs then
-    { cur := t.cur.getArg idx, parents := t.parents.push $ t.cur.setArg idx (arbitrary _), idxs := t.idxs.push idx }
+    { cur := t.cur.getArg idx, parents := t.parents.push $ t.cur.setArg idx arbitrary, idxs := t.idxs.push idx }
   else
     { cur := Syntax.missing, parents := t.parents.push t.cur, idxs := t.idxs.push idx }
 
diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean
index 391f9919cb..4e06805fc7 100644
--- a/src/Lean/Util/PPExt.lean
+++ b/src/Lean/Util/PPExt.lean
@@ -31,7 +31,7 @@ structure PPFns :=
   (ppExpr : PPContext → Expr → IO Format)
   (ppTerm : PPContext → Syntax → IO Format)
 
-instance : Inhabited PPFns := ⟨⟨arbitrary _, arbitrary _⟩⟩
+instance : Inhabited PPFns := ⟨⟨arbitrary, arbitrary⟩⟩
 
 builtin_initialize ppFnsRef : IO.Ref PPFns ←
   IO.mkRef {
diff --git a/src/Lean/Util/ReplaceExpr.lean b/src/Lean/Util/ReplaceExpr.lean
index bc96da2ddd..ebdd7263dc 100644
--- a/src/Lean/Util/ReplaceExpr.lean
+++ b/src/Lean/Util/ReplaceExpr.lean
@@ -43,7 +43,7 @@ abbrev ReplaceM := StateM State
 
 unsafe def initCache : State :=
   { keys    := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
-    results := mkArray cacheSize.toNat (arbitrary _) }
+    results := mkArray cacheSize.toNat arbitrary }
 
 @[inline] unsafe def replaceUnsafe (f? : Expr → Option Expr) (e : Expr) : Expr :=
   (replaceUnsafeM f? cacheSize e).run' initCache
diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean
index ba03c82962..0b892e18f5 100644
--- a/src/Lean/Util/ReplaceLevel.lean
+++ b/src/Lean/Util/ReplaceLevel.lean
@@ -56,7 +56,7 @@ abbrev ReplaceM := StateM State
 
 unsafe def initCache : State :=
   { keys    := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
-    results := mkArray cacheSize.toNat (arbitrary _) }
+    results := mkArray cacheSize.toNat arbitrary }
 
 @[inline] unsafe def replaceUnsafe (f? : Level → Option Level) (e : Expr) : Expr :=
   (replaceUnsafeM f? cacheSize e).run' initCache
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index a92e1e062c..c31d03a818 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -16,7 +16,7 @@ structure TraceElem :=
   (msg : MessageData)
 
 instance : Inhabited TraceElem :=
-  ⟨⟨arbitrary _, arbitrary _⟩⟩
+  ⟨⟨arbitrary, arbitrary⟩⟩
 
 structure TraceState :=
   (enabled : Bool := true)
diff --git a/src/Std/Data/BinomialHeap.lean b/src/Std/Data/BinomialHeap.lean
index 633652e5f7..fbe28c2fcc 100644
--- a/src/Std/Data/BinomialHeap.lean
+++ b/src/Std/Data/BinomialHeap.lean
@@ -66,8 +66,8 @@ def singleton (a : α) : Heap α :=
 
 /- O(log n) -/
 @[specialize] def head [Inhabited α] (lt : α → α → Bool) : Heap α → α
-  | Heap.empty        => arbitrary α
-  | Heap.heap []      => arbitrary α
+  | Heap.empty        => arbitrary
+  | Heap.heap []      => arbitrary
   | Heap.heap (h::hs) => hs.foldl (init := h.val) fun r n => if lt r n.val then r else n.val
 
 @[specialize] def findMin (lt : α → α → Bool) : List (HeapNode α) → Nat → HeapNode α × Nat → HeapNode α × Nat
diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean
index ac5bc5769e..f98a27454e 100644
--- a/src/Std/Data/PersistentArray.lean
+++ b/src/Std/Data/PersistentArray.lean
@@ -146,7 +146,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
     if h : cs.size ≠ 0 then
       let idx : Fin cs.size := ⟨cs.size - 1, Nat.predLt h⟩
       let last := cs.get idx
-      let cs'  := cs.set idx (arbitrary _)
+      let cs'  := cs.set idx arbitrary
       match popLeaf last with
       | (none,   _)       => (none, emptyArray)
       | (some l, newLast) =>
diff --git a/src/Std/ShareCommon.lean b/src/Std/ShareCommon.lean
index 4619756edd..6c8acee651 100644
--- a/src/Std/ShareCommon.lean
+++ b/src/Std/ShareCommon.lean
@@ -27,10 +27,10 @@ unsafe def Object.ptrHash (a : Object) : USize :=
   ptrAddrUnsafe a
 
 @[extern "lean_sharecommon_eq"]
-unsafe constant Object.eq (a b : @& Object) : Bool := arbitrary _
+unsafe constant Object.eq (a b : @& Object) : Bool
 
 @[extern "lean_sharecommon_hash"]
-unsafe constant Object.hash (a : @& Object) : USize := arbitrary _
+unsafe constant Object.hash (a : @& Object) : USize
 
 unsafe def ObjectMap : Type := @HashMap Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩
 unsafe def ObjectSet : Type := @HashSet Object ⟨Object.eq⟩ ⟨Object.hash⟩
@@ -86,7 +86,7 @@ unsafe def ObjectPersistentSet.insert (s : ObjectPersistentSet) (o : Object) : O
   @PersistentHashSet.insert Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o
 
 /- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet` -/
-constant StatePointed : PointedType := arbitrary _
+constant StatePointed : PointedType
 abbrev State : Type u := StatePointed.type
 @[extern "lean_sharecommon_mk_state"]
 constant mkState : Unit → State := fun _ => StatePointed.val
@@ -94,7 +94,7 @@ def State.empty : State := mkState ()
 instance State.inhabited : Inhabited State := ⟨State.empty⟩
 
 /- Internally `PersistentState` is implemented as a pair `ObjectPersistentMap` and `ObjectPersistentSet` -/
-constant PersistentStatePointed : PointedType := arbitrary _
+constant PersistentStatePointed : PointedType
 abbrev PersistentState : Type u := PersistentStatePointed.type
 @[extern "lean_sharecommon_mk_pstate"]
 constant mkPersistentState : Unit → PersistentState := fun _ => PersistentStatePointed.val