diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index 9159bbd76d..ee03c3b800 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -204,8 +204,7 @@ instance : Repr Substring where
   reprPrec s _ := Format.text <| String.quote s.toString ++ ".toSubstring"
 
 instance : Repr String.Iterator where
-  reprPrec | ⟨s, pos⟩, prec =>
-    Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
+  reprPrec | ⟨s, pos⟩, prec => Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
 
 instance (n : Nat) : Repr (Fin n) where
   reprPrec f _ := repr f.val
diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean
index fc1f07a7e7..f277d7e0b3 100644
--- a/src/Init/Data/Stream.lean
+++ b/src/Init/Data/Stream.lean
@@ -77,12 +77,13 @@ instance : ToStream Std.Range Std.Range where
   toStream r := r
 
 instance [Stream ρ α] [Stream γ β] : Stream (ρ × γ) (α × β) where
-  next? | (s₁, s₂) =>
-    match Stream.next? s₁ with
-    | none => none
-    | some (a, s₁) => match Stream.next? s₂ with
+  next?
+    | (s₁, s₂) =>
+      match Stream.next? s₁ with
       | none => none
-      | some (b, s₂) => some ((a, b), (s₁, s₂))
+      | some (a, s₁) => match Stream.next? s₂ with
+        | none => none
+        | some (b, s₂) => some ((a, b), (s₁, s₂))
 
 instance : Stream (List α) α where
   next?
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 75393d36b7..4693e10853 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -953,7 +953,7 @@ private def isLambdaWithImplicit (stx : Syntax) : Bool :=
   | `(fun $binders* => $body) => binders.any fun b => b.isOfKind `Lean.Parser.Term.implicitBinder || b.isOfKind `Lean.Parser.Term.instBinder
   | _                         => false
 
-private partial def dropTermParens : Syntax → Syntax | stx =>
+private partial def dropTermParens : Syntax → Syntax := fun stx =>
   match stx with
   | `(($stx)) => dropTermParens stx
   | _         => stx