diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out
index e768883fb7..680c7cb403 100644
--- a/tests/lean/docStr.lean.expected.out
+++ b/tests/lean/docStr.lean.expected.out
@@ -16,7 +16,7 @@ doc string for 'f' is not available
 doc string for 'g' is not available
 "let rec documentation at g "
 "Gadget for optional parameter support. "
-"Auxiliary Declaration used to implement the named patterns `x@p`\n    -- TODO: add proof for `x = a`\n"
+"Auxiliary Declaration used to implement the named patterns `x@h:p` "
 "Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\n  it reduces `A` and continues bulding the telescope if it is a `forall`. "
 Foo :=
   { range := { pos := { line := 4, column := 0 },