diff --git a/common/vscode.nix b/common/vscode.nix
index 7bc1bce..7f9ed5a 100755
--- a/common/vscode.nix
+++ b/common/vscode.nix
@@ -38,6 +38,12 @@
        version = "0.0.226";
        sha256 = "sha256-Fj9cw+VJ2jkTGUclB1TLvURhzQsaryFQs/+f2RZOLHs=";
      }
+     {
+       name = "lean4";
+       publisher = "leanprover";
+       version = "0.0.133";
+       sha256 = "sha256-tjBTOkh4UeEmOo/ZbadpeyW07QiPcUO4aI2NWdtTxrE=";
+     }
     ];
    userSettings = {
      "agdaMode.connection.agdaLanguageServer" = false;
diff --git a/gunther/hypr/hyprland.nix b/gunther/hypr/hyprland.nix
index 7be7ccb..013f817 100644
--- a/gunther/hypr/hyprland.nix
+++ b/gunther/hypr/hyprland.nix
@@ -155,7 +155,7 @@
     font = "monospace 14";
     terminal = "foot";
     extraConfig = {
-      modi = "drun,run,top";
+      modi = "drun,run";
     };
     plugins = [
       pkgs.rofi-top
diff --git a/gunther/leonv.nix b/gunther/leonv.nix
index 41841b2..56ef712 100755
--- a/gunther/leonv.nix
+++ b/gunther/leonv.nix
@@ -15,6 +15,7 @@
     orchis-theme
 
     # stuff
+    tidal-hifi
     jq
     vlc
     openvpn
@@ -81,11 +82,12 @@
     yubikey-manager
 
     # agda
-
     (agda.withPackages [ 
       agdaPackages.standard-library
       agdaPackages.agda-categories
     ])
+
+    lean4
   ];
 
   programs.home-manager.enable = true;