diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index e0e30974ac..44f2ca4a33 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -268,18 +268,18 @@ def data : (@& Expr) → Data
   | proj _ _ _ d    => d
 
 def ctorName : Expr → String
-  | bvar _ _        => "bvar"
-  | fvar _ _        => "fvar"
-  | mvar _ _        => "mvar"
-  | sort _ _        => "sort"
-  | const _ _ _     => "const"
-  | app _ _ _       => "app"
-  | lam _ _ _ _     => "lam"
-  | forallE _ _ _ _ => "forallE"
-  | letE _ _ _ _ _  => "letE"
-  | lit _ _         => "lit"
-  | mdata _ _ _     => "mdata"
-  | proj _ _ _ _    => "proj"
+  | bvar ..    => "bvar"
+  | fvar ..    => "fvar"
+  | mvar ..    => "mvar"
+  | sort ..    => "sort"
+  | const ..   => "const"
+  | app ..     => "app"
+  | lam ..     => "lam"
+  | forallE .. => "forallE"
+  | letE ..    => "letE"
+  | lit ..     => "lit"
+  | mdata ..   => "mdata"
+  | proj ..    => "proj"
 
 protected def hash (e : Expr) : UInt64 :=
   e.data.hash
@@ -486,8 +486,8 @@ protected unsafe def ptrEq (a b : Expr) : Bool :=
 constant equal (a : @& Expr) (b : @& Expr) : Bool
 
 def isSort : Expr → Bool
-  | sort _ _ => true
-  | _        => false
+  | sort .. => true
+  | _       => false
 
 def isType : Expr → Bool
   | sort (Level.succ ..) _ => true
@@ -498,16 +498,16 @@ def isProp : Expr → Bool
   | _ => false
 
 def isBVar : Expr → Bool
-  | bvar _ _ => true
-  | _        => false
+  | bvar .. => true
+  | _       => false
 
 def isMVar : Expr → Bool
-  | mvar _ _ => true
-  | _        => false
+  | mvar .. => true
+  | _       => false
 
 def isFVar : Expr → Bool
-  | fvar _ _ => true
-  | _        => false
+  | fvar .. => true
+  | _       => false
 
 def isApp : Expr → Bool
   | app .. => true
@@ -522,8 +522,8 @@ def isConst : Expr → Bool
   | _        => false
 
 def isConstOf : Expr → Name → Bool
-  | const n _ _, m => n == m
-  | _,           _ => false
+  | const n .., m => n == m
+  | _,          _ => false
 
 def isForall : Expr → Bool
   | forallE .. => true
@@ -854,13 +854,13 @@ instance : ToString Expr where
 
 /-- Returns true when the expression does not have any sub-expressions. -/
 def isAtomic : Expr → Bool
-  | Expr.const _ _ _ => true
-  | Expr.sort _ _    => true
-  | Expr.bvar _ _    => true
-  | Expr.lit _ _     => true
-  | Expr.mvar _ _    => true
-  | Expr.fvar _ _    => true
-  | _                => false
+  | Expr.const .. => true
+  | Expr.sort ..  => true
+  | Expr.bvar ..  => true
+  | Expr.lit ..   => true
+  | Expr.mvar ..  => true
+  | Expr.fvar ..  => true
+  | _             => false
 
 end Expr
 
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index accef1deac..4ba8fc6d92 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -396,7 +396,7 @@ def assignExpr (m : MetavarContext) (mvarId : MVarId) (val : Expr) : MetavarCont
   { m with eAssignment := m.eAssignment.insert mvarId val }
 
 def assignDelayed (m : MetavarContext) (mvarId : MVarId) (lctx : LocalContext) (fvars : Array Expr) (val : Expr) : MetavarContext :=
-  { m with dAssignment := m.dAssignment.insert mvarId { lctx := lctx, fvars := fvars, val := val } }
+  { m with dAssignment := m.dAssignment.insert mvarId { lctx, fvars, val } }
 
 def getLevelAssignment? (m : MetavarContext) (mvarId : MVarId) : Option Level :=
   m.lAssignment.find? mvarId
@@ -557,7 +557,7 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi
         let mctx ← getMCtx
         match mctx.getDelayedAssignment? mvarId with
         | none => instApp
-        | some { fvars := fvars, val := val, .. } =>
+        | some { fvars, val, .. } =>
           /-
              Apply "delayed substitution" (i.e., delayed assignment + application).
              That is, `f` is some metavariable `?m`, that is delayed assigned to `val`.
@@ -628,7 +628,7 @@ def instantiateMVarDeclMVars (mctx : MetavarContext) (mvarId : MVarId) : Metavar
   let mvarDecl     := mctx.getDecl mvarId
   let (lctx, mctx) := mctx.instantiateLCtxMVars mvarDecl.lctx
   let (type, mctx) := mctx.instantiateMVars mvarDecl.type
-  { mctx with decls := mctx.decls.insert mvarId { mvarDecl with lctx := lctx, type := type } }
+  { mctx with decls := mctx.decls.insert mvarId { mvarDecl with lctx, type } }
 
 namespace DependsOn
 
@@ -897,7 +897,7 @@ mutual
     | Expr.lam _ d b _     => return e.updateLambdaE! (← visit xs d) (← visit xs b)
     | Expr.letE _ t v b _  => return e.updateLet! (← visit xs t) (← visit xs v) (← visit xs b)
     | Expr.mdata _ b _     => return e.updateMData! (← visit xs b)
-    | Expr.app _ _ _       => e.withApp fun f args => elimApp xs f args
+    | Expr.app ..          => e.withApp fun f args => elimApp xs f args
     | Expr.mvar mvarId _   => elimApp xs e #[]
     | e                    => return e
 
@@ -993,7 +993,7 @@ mutual
         cont #[] mvarLCtx
       else match mctx.getDelayedAssignment? mvarId with
       | none => cont #[] mvarLCtx
-      | some { fvars := fvars, lctx := nestedLCtx, .. } => cont fvars nestedLCtx -- Remark: nestedLCtx is bigger than mvarLCtx
+      | some { fvars, lctx := nestedLCtx, .. } => cont fvars nestedLCtx -- Remark: nestedLCtx is bigger than mvarLCtx
 
   private partial def elimApp (xs : Array Expr) (f : Expr) (args : Array Expr) : M Expr := do
     match f with
@@ -1209,9 +1209,9 @@ structure UnivMVarParamResult where
 def levelMVarToParam (mctx : MetavarContext) (alreadyUsedPred : Name → Bool) (except : MVarId → Bool) (e : Expr) (paramNamePrefix : Name := `u) (nextParamIdx : Nat := 1)
     : UnivMVarParamResult :=
   let (e, s) := LevelMVarToParam.main e { except, paramNamePrefix, alreadyUsedPred } { mctx, nextParamIdx }
-  { mctx          := s.mctx,
-    newParamNames := s.paramNames,
-    nextParamIdx  := s.nextParamIdx,
+  { mctx          := s.mctx
+    newParamNames := s.paramNames
+    nextParamIdx  := s.nextParamIdx
     expr          := e }
 
 def getExprAssignmentDomain (mctx : MetavarContext) : Array MVarId :=