diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 117581b680..780e60a812 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -107,7 +107,7 @@ def isEtaUnassignedMVar (e : Expr) : MetaM Bool := do
   ```
   fun x₁ ... xₙ => ?m x₁ ... xₙ =?= t
   t =?= fun x₁ ... xₙ => ?m x₁ ... xₙ
-
+  ```
   This is important because type inference often produces
   eta-expanded terms, and without this extra case, we could
   introduce counter intuitive behavior.