diff --git a/.vscode/settings.json b/.vscode/settings.json
index 58b54e97..1b2d7b32 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -1,19 +1,11 @@
 {
     "files.exclude": {
-        ".devcontainer": true,
-        ".docker": true,
         "**/.DS_Store": true,
         "**/.DS_yml": true,
         "**/.git": true,
-        "**/.gitpod.yml": true,
-        "**/.vscode": true,
         "**/*.olean": true,
         "build": true,
         "html": true,
-        "lake-packages": true,
-        "lean-tactics.tex": true,
-        "LICENSE": true,
-        "mathematics_in_lean.pdf": true
     },
     "editor.minimap.enabled": false,
     "editor.acceptSuggestionOnEnter": "off",
diff --git a/lean-tactics.pdf b/lean-tactics.pdf
deleted file mode 100644
index 217f343b..00000000
Binary files a/lean-tactics.pdf and /dev/null differ