diff --git a/lua/lean/commands.lua b/lua/lean/commands.lua
index d1bc4767..71d1e9cb 100644
--- a/lua/lean/commands.lua
+++ b/lua/lean/commands.lua
@@ -116,11 +116,11 @@ end
 
 function commands.enable()
   vim.cmd[[
-    command LeanPlainGoal :lua require'lean.commands'.show_goal(false)
-    command LeanPlainTermGoal :lua require'lean.commands'.show_term_goal(false)
-    command LeanGoal :lua require'lean.commands'.show_goal()
-    command LeanTermGoal :lua require'lean.commands'.show_term_goal()
-    command LeanLineDiagnostics :lua require'lean.commands'.show_line_diagnostics()
+    command! LeanPlainGoal :lua require'lean.commands'.show_goal(false)
+    command! LeanPlainTermGoal :lua require'lean.commands'.show_term_goal(false)
+    command! LeanGoal :lua require'lean.commands'.show_goal()
+    command! LeanTermGoal :lua require'lean.commands'.show_term_goal()
+    command! LeanLineDiagnostics :lua require'lean.commands'.show_line_diagnostics()
   ]]
 end
 
diff --git a/lua/lean/ft.lua b/lua/lean/ft.lua
index 99ecd7dc..c5d59225 100644
--- a/lua/lean/ft.lua
+++ b/lua/lean/ft.lua
@@ -21,7 +21,7 @@ function ft.enable(opts)
     -- this means we have to manage it
     global_default_managed = true
   end
-  options= vim.tbl_extend("force", options._DEFAULTS, opts)
+  options= vim.tbl_extend("force", options, opts)
   if global_default_managed then
     lean_nvim_default_filetype = options.default
   end
diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua
index 8203926a..a9c94cf8 100644
--- a/lua/lean/infoview.lua
+++ b/lua/lean/infoview.lua
@@ -20,7 +20,6 @@ local infoview = {
   debug = false,
 }
 local options = {
-  _DEFAULTS = {
     width = 50,
     height = 20,
     horizontal_position = 'bottom',
@@ -46,7 +45,6 @@ local options = {
       ['C'] = 'clear_all',
       ['<LocalLeader><Tab>'] = 'goto_last_window',
     }
-  }
 }
 
 --- An individual pin.
@@ -1039,13 +1037,13 @@ end
 
 --- Enable and open the infoview across all Lean buffers.
 function infoview.enable(opts)
-  options = vim.tbl_extend("force", options._DEFAULTS, opts)
+  options = vim.tbl_extend("force", options, opts)
   infoview.mappings = options.mappings
   infoview.enabled = true
   infoview.set_autoopen(options.autoopen)
   set_augroup("LeanInfoviewInit", [[
-    autocmd FileType lean3 lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
-    autocmd FileType lean lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
+    autocmd! FileType lean3 lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
+    autocmd! FileType lean lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
   ]])
 end
 
diff --git a/lua/lean/init.lua b/lua/lean/init.lua
index 4953c3e7..2082a194 100644
--- a/lua/lean/init.lua
+++ b/lua/lean/init.lua
@@ -43,7 +43,6 @@ function lean.setup(opts)
 
   opts.infoview = opts.infoview or {}
   require'lean.infoview'.enable(opts.infoview)
-
   require'lean.commands'.enable()
 
   opts.lsp3 = opts.lsp3 or {}
@@ -64,31 +63,34 @@ function lean.setup(opts)
   if opts.stderr.enable ~= false then require'lean.stderr'.enable(opts.stderr or {}) end
 
   vim.cmd[[
-    command LeanRestartFile :lua require'lean.lsp'.restart_file()
-    command LeanRefreshFileDependencies :lua require'lean.lsp'.restart_file()
-
-    command LeanInfoviewToggle :lua require'lean.infoview'.toggle()
-    command LeanInfoviewPinTogglePause :lua require'lean.infoview'.pin_toggle_pause()
-    command LeanInfoviewAddPin :lua require'lean.infoview'.add_pin()
-    command LeanInfoviewClearPins :lua require'lean.infoview'.clear_pins()
-    command LeanInfoviewSetDiffPin :lua require'lean.infoview'.set_diff_pin()
-    command LeanInfoviewClearDiffPin :lua require'lean.infoview'.clear_diff_pin()
-    command LeanInfoviewToggleAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(true)
-    command LeanInfoviewToggleNoClearAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(false)
-    command LeanInfoviewEnableWidgets :lua require'lean.infoview'.enable_widgets()
-    command LeanInfoviewDisableWidgets :lua require'lean.infoview'.disable_widgets()
-    command LeanGotoInfoview :lua require'lean.infoview'.go_to()
-
-    command LeanAbbreviationsReverseLookup :lua require'lean.abbreviations'.show_reverse_lookup()
-
-    command LeanSorryFill :lua require'lean.sorry'.fill()
-    command LeanTryThis :lua require'lean.trythis'.swap()
+    command! LeanRestartFile :lua require'lean.lsp'.restart_file()
+    command! LeanRefreshFileDependencies :lua require'lean.lsp'.restart_file()
+
+    command! LeanInfoviewToggle :lua require'lean.infoview'.toggle()
+    command! LeanInfoviewPinTogglePause :lua require'lean.infoview'.pin_toggle_pause()
+    command! LeanInfoviewAddPin :lua require'lean.infoview'.add_pin()
+    command! LeanInfoviewClearPins :lua require'lean.infoview'.clear_pins()
+    command! LeanInfoviewSetDiffPin :lua require'lean.infoview'.set_diff_pin()
+    command! LeanInfoviewClearDiffPin :lua require'lean.infoview'.clear_diff_pin()
+    command! LeanInfoviewToggleAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(true)
+    command! LeanInfoviewToggleNoClearAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(false)
+    command! LeanInfoviewEnableWidgets :lua require'lean.infoview'.enable_widgets()
+    command! LeanInfoviewDisableWidgets :lua require'lean.infoview'.disable_widgets()
+    command! LeanGotoInfoview :lua require'lean.infoview'.go_to()
+
+    command! LeanAbbreviationsReverseLookup :lua require'lean.abbreviations'.show_reverse_lookup()
+
+    command! LeanSorryFill :lua require'lean.sorry'.fill()
+    command! LeanTryThis :lua require'lean.trythis'.swap()
   ]]
 
   if opts.mappings == true then
     vim.cmd[[
-      autocmd FileType lean3 lua require'lean'.use_suggested_mappings(true)
-      autocmd FileType lean lua require'lean'.use_suggested_mappings(true)
+      augroup lean_nvim_mappings
+        autocmd!
+        autocmd FileType lean3 lua require'lean'.use_suggested_mappings(true)
+        autocmd FileType lean lua require'lean'.use_suggested_mappings(true)
+      augroup END
     ]]
   end
 
diff --git a/lua/lean/progress_bars.lua b/lua/lean/progress_bars.lua
index 8b84a84e..d06b1481 100644
--- a/lua/lean/progress_bars.lua
+++ b/lua/lean/progress_bars.lua
@@ -1,7 +1,8 @@
 local progress = require('lean.progress')
 
-local M = {}
-local options = { _DEFAULTS = { priority = 10, character = '⋯' } }
+local progress_bars = {}
+local options = {  priority = 10, character = '⋯' }
+options._DEFAULTS = vim.deepcopy(options)
 
 local sign_group_name = 'leanSignProgress'
 local sign_name = 'leanSignProgress'
@@ -41,8 +42,8 @@ end
 -- Table from bufnr to timer object.
 local timers = {}
 
-function M.update(params)
-  if not M.enabled then return end
+function progress_bars.update(params)
+  if not progress_bars.enabled then return end
   -- TODO FIXME can potentially create new buffer
   local bufnr = vim.uri_to_bufnr(params.textDocument.uri)
 
@@ -54,15 +55,15 @@ function M.update(params)
   end
 end
 
-function M.enable(opts)
-  options = vim.tbl_extend("force", options._DEFAULTS, opts)
+function progress_bars.enable(opts)
+  options = vim.tbl_extend("force", options, opts)
 
   vim.fn.sign_define(sign_name, {
     text = options.character,
     texthl = 'leanSignProgress',
   })
   vim.cmd[[hi def leanSignProgress guifg=orange ctermfg=215]]
-  M.enabled = true
+  progress_bars.enabled = true
 end
 
-return M
+return progress_bars