                            :identifier identifiers
                            :symbol     symbols
                            :extra      extras
+                           :proofstate proofstates
                            :nay        (lean-info-nay-p   string)
                            :stale      (lean-info-stale-p string))))
 
 (defun lean-info-record-to-string (info-record)
   "Given typeinfo, overload, and sym-name, compose string information."
-  (let* ((type     (cl-first (lean-info-record-type       info-record)))
-         (overload (cl-first (lean-info-record-overload   info-record)))
-         (synth    (cl-first (lean-info-record-synth      info-record)))
-         (coercion (cl-first (lean-info-record-coercion   info-record)))
-         (extra    (cl-first (lean-info-record-extra      info-record)))
-         (id       (cl-first (lean-info-record-identifier info-record)))
-         (sym      (cl-first (lean-info-record-symbol     info-record)))
-         (stale    (lean-info-record-stale                info-record))
-         name-str type-str coercion-str extra-str overload-str str)
+  (let* ((type       (cl-first (lean-info-record-type       info-record)))
+         (overload   (cl-first (lean-info-record-overload   info-record)))
+         (synth      (cl-first (lean-info-record-synth      info-record)))
+         (coercion   (cl-first (lean-info-record-coercion   info-record)))
+         (extra      (cl-first (lean-info-record-extra      info-record)))
+         (proofstate (cl-first (lean-info-record-proofstate info-record)))
+         (id         (cl-first (lean-info-record-identifier info-record)))
+         (sym        (cl-first (lean-info-record-symbol     info-record)))
+         (stale      (lean-info-record-stale                info-record))
+         name-str type-str coercion-str extra-str proofstate-str overload-str str)
     (setq name-str
           (cond
            (synth (lean-info-synth-body-str synth))

         (coercions   (-filter 'lean-info-coercion-p   info-list))
         (identifiers (-filter 'lean-info-identifier-p info-list))
         (symbols     (-filter 'lean-info-symbol-p     info-list))
         (extras      (-filter 'lean-info-extra-p      info-list)))
    (make-lean-info-record :type       types
                           :overload   overloads
                           :synth      synths

                        (format "\n%s with %s"
                                (propertize "overloaded" 'face 'font-lock-keyword-face)
                                overload-str))))
    (when proofstate
      (setq str (format "%s" (lean-info-proofstate-body-str proofstate))))
    (when (and stale str)
      (setq str (format "[%s] %s"
                        (propertize "stale" 'face '(foreground-color . "red"))
