Bindings and lean goal not working

[Jlh18]

I had to add "data" to :files to get bindings and the lean goal working (probably among other things). So I did

(defconst lean4-packages
  '((lean4-mode :location (recipe
                           :fetcher github
                           :repo "leanprover/lean4-mode"
                           :files ("*.el" "data")))
    smartparens
    )
  )

instead of the original

(defconst lean4-packages
  '((lean4-mode :location (recipe
                           :fetcher github
                           :repo "leanprover/lean4-mode"
                           :files ("*.el")))
    smartparens
    )
  )

The lean4-mode page seems to suggest requiring "data" as well. I didn't put this as a pull request because maybe you only wanted syntax highlighting or something?