diff --git a/Auto/Embedding/LCtx.lean b/Auto/Embedding/LCtx.lean
index b576334..39e2d3b 100644
--- a/Auto/Embedding/LCtx.lean
+++ b/Auto/Embedding/LCtx.lean
@@ -4,7 +4,6 @@ import Auto.Lib.NatExtra
 import Auto.Lib.ListExtra
 import Auto.Lib.HList
 import Auto.Lib.BinTree
-import Std.Data.List.Lemmas
 
 namespace Auto.Embedding
 
@@ -23,7 +22,7 @@ section generic
       dsimp
       rw [Nat.sub_add_cancel (Nat.le_of_ble_eq_true h)]
     | false => rfl
-  
+
   theorem mapAt_id_eq_id' (pos : Nat) : mapAt pos (fun x => x) = id :=
     mapAt_id_eq_id pos
 
@@ -52,7 +51,7 @@ section generic
       rw [hble]; dsimp; rw [Nat.add_sub_cancel]
     | false =>
       dsimp; rw [h]
-  
+
   @[reducible] def restoreAt {α} (pos : Nat) (restore : (Nat → α) → (Nat → α)) :=
     fun (lctx : Nat → α) (n : Nat) =>
       match pos.ble n with
@@ -76,11 +75,11 @@ section generic
 
   def coPair {α} (f : Nat → Nat) (restore : (Nat → α) → (Nat → α)) :=
     ∀ (lctx : Nat → α) (n : Nat), (restore lctx) (f n) = lctx n
-  
+
   def coPairAt {α} (f : Nat → Nat) (restore : (Nat → α) → (Nat → α)) :=
     ∀ (pos : Nat) (lctx : Nat → α) (n : Nat),
       (restoreAt pos restore lctx) (mapAt pos f n) = lctx n
-  
+
   theorem coPairAt.ofcoPair (cp : coPair f restore) : coPairAt f restore := by
     intros pos lctx n;
     dsimp [restoreAt, mapAt]
@@ -238,7 +237,7 @@ end generic
 
 
 section push
-  
+
   @[reducible] def pushLCtx (x : α) (lctx : Nat → α) (n : Nat) : α :=
     match n with
     | 0 => x
@@ -256,7 +255,7 @@ section push
     dsimp [pushLCtxAt, restoreAt]
     rw [show (pos.ble pos = true) by (apply Nat.ble_eq_true_of_le; apply Nat.le_refl)]
     rw [Nat.sub_self]
-  
+
   theorem pushLCtxAt_gt (x : α) (pos : Nat) (n : Nat) (hle : n > pos) : pushLCtxAt x pos lctx n = lctx n.pred := by
     dsimp [pushLCtxAt, restoreAt]
     rw [show (pos.ble n = true) by (apply Nat.ble_eq_true_of_le; apply Nat.le_of_lt hle)]
@@ -274,15 +273,15 @@ section push
 
   theorem pushLCtxAt_succ_zero (x : α) (pos : Nat) (lctx : Nat → α) :
     pushLCtxAt x (.succ pos) lctx 0 = lctx 0 := rfl
-  
+
   theorem pushLCtxAt_succ_succ (x : α) (pos : Nat) (lctx : Nat → α) (n : Nat) :
     pushLCtxAt x (.succ pos) lctx (.succ n) = pushLCtxAt x pos (fun n => lctx (.succ n)) n :=
     restoreAt_succ_succ _ _ _ _
-  
+
   theorem pushLCtxAt_succ_succ_Fn (x : α) (pos : Nat) (lctx : Nat → α) :
     (fun n => pushLCtxAt x (.succ pos) lctx (.succ n)) = pushLCtxAt x pos (fun n => lctx (.succ n)) :=
     restoreAt_succ_succ_Fn _ _ _
-  
+
   theorem pushLCtxAt_comm (f : α → β) (x : α) (pos : Nat) (lctx : Nat → α) (n : Nat) :
     f (pushLCtxAt x pos lctx n) = pushLCtxAt (f x) pos (f ∘ lctx) n := by
     dsimp [pushLCtxAt, restoreAt]
@@ -292,11 +291,11 @@ section push
       | 0 => rfl
       | _ + 1 => rfl
     | false => rfl
-  
+
   theorem pushLCtxAt_commFn (f : α → β) (x : α) (pos : Nat) (lctx : Nat → α) :
     (fun n => f (pushLCtxAt x pos lctx n)) = (fun n => pushLCtxAt (f x) pos (fun n => f (lctx n)) n) :=
     funext (pushLCtxAt_comm f x pos lctx)
-  
+
   @[reducible] def pushLCtxDep {lctxty : α → Sort u} {xty : α} (x : lctxty xty)
     {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) (n : Nat) : lctxty (pushLCtx xty rty n) := by
     dsimp [pushLCtx]
@@ -315,7 +314,7 @@ section push
     cases h₁; cases h₂; cases h₃; cases h₄; cases h₅; cases h₆; apply HEq.refl
 
   theorem pushLCtxDep_substLCtx
-    {lctxty : α → Sort u} {ty : α} (x : lctxty ty) 
+    {lctxty : α → Sort u} {ty : α} (x : lctxty ty)
     {rty₁ : Nat → α} (lctx₁ : ∀ n, lctxty (rty₁ n))
     {rty₂ : Nat → α} (lctx₂ : ∀ n, lctxty (rty₂ n))
     (h₁ : rty₁ = rty₂) (h₂ : HEq lctx₁ lctx₂) :
@@ -333,7 +332,7 @@ section push
   def pushLCtxAtDep {lctxty : α → Sort u} {xty : α} (x : lctxty xty) (pos : Nat)
     {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) (n : Nat) : lctxty (pushLCtxAt xty pos rty n) :=
     restoreAtDep pos (pushLCtxDep x) lctx n
-  
+
   theorem pushLCtxAtDep_heq
     {lctxty₁ : α₁ → Sort u} {ty₁ : α₁} (x₁ : lctxty₁ ty₁) (pos₁ : Nat)
     (rty₁ : Nat → α₁) (lctx₁ : ∀ n, lctxty₁ (rty₁ n))
@@ -367,17 +366,17 @@ section push
   theorem pushLCtxAtDep_succ_zero {rty : Nat → α} {lctxty : α → Sort u}
     {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) :
     pushLCtxAtDep x (.succ pos) lctx 0 = lctx 0 := rfl
-  
+
   theorem pushLCtxAtDep_succ_succ {rty : Nat → α} {lctxty : α → Sort u} {xty : α}
     (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) (n : Nat) :
     HEq (pushLCtxAtDep x (.succ pos) lctx (.succ n)) (pushLCtxAtDep x pos (fun n => lctx (.succ n)) n) :=
     restoreAtDep_succ_succ _ _ _ _
-  
+
   theorem pushLCtxAtDep_succ_succ_Fn {rty : Nat → α} {lctxty : α → Sort u}
     {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) :
     HEq (fun n => pushLCtxAtDep x (.succ pos) lctx (.succ n)) (pushLCtxAtDep x pos (fun n => lctx (.succ n))) :=
     restoreAtDep_succ_succ_Fn _ _ _
-  
+
   def pushLCtxAtDep_comm {α : Sort w} {β : α → Sort x} {rty : Nat → α} {lctxty : α → Sort u}
     (f : ∀ (x : α), lctxty x → β x) {xty : α} (x : lctxty xty) (pos : Nat)
     (lctx : ∀ n, lctxty (rty n)) (n : Nat) :
@@ -389,11 +388,11 @@ section push
       | 0 => rfl
       | _ + 1 => rfl
     | false => rfl
-  
+
   def pushLCtxAtDep.nonDep {rty : Nat → α} {lctxty : Sort u}
     {xty : α} (x : lctxty) (pos : Nat) (lctx : Nat → lctxty) (n : Nat) :
     @pushLCtxAtDep _ (fun _ => lctxty) xty x pos rty lctx n = pushLCtxAt x pos lctx n := rfl
-  
+
   def pushLCtxAtDep_absorbAux {rty : Nat → α} {lctxty : α → Sort u}
     {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) (n : Nat) :
     HEq
@@ -407,36 +406,36 @@ section push
       | 0 => rfl
       | _ + 1 => rfl
     | false => rfl
-  
+
   theorem pushLCtxAtDep_absorb {rty : Nat → α} {lctxty : α → Sort u}
     {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) :
     HEq (@pushLCtxAtDep _ lctxty _ x pos rty lctx) (@pushLCtxAtDep _ id _ x pos (lctxty ∘ rty) lctx) :=
     HEq.funext _ _ (pushLCtxAtDep_absorbAux _ _ _)
-  
+
   theorem pushLCtx_zero (x : α) (lctx : Nat → α) : pushLCtx x lctx 0 = x := rfl
 
   theorem pushLCtx_succ (x : α) (lctx : Nat → α) (n : Nat) : pushLCtx x lctx (.succ n) = lctx n := rfl
-  
+
   theorem pushLCtx_succ_Fn (x : α) (lctx : Nat → α) :
     (fun n => pushLCtx x lctx (.succ n)) = lctx := rfl
-  
+
   theorem pushLCtx_comm (f : α → β) (x : α) (lctx : Nat → α) (n : Nat) :
     f (pushLCtx x lctx n) = pushLCtx (f x) (fun n => f (lctx n)) n := by
     rw [← pushLCtxAt_zero]; rw [← pushLCtxAt_zero]
     apply pushLCtxAt_comm f x 0 lctx n
-  
+
   theorem pushLCtx_commFn (f : α → β) (x : α) (lctx : Nat → α) :
     (fun n => f (pushLCtx x lctx n)) = (fun n => pushLCtx (f x) (fun n => f (lctx n)) n) :=
     funext (pushLCtx_comm f x lctx)
-  
+
   theorem pushLCtx_pushLCtxAt (x y : α) (pos : Nat) (lctx : Nat → α) :
     pushLCtx y (pushLCtxAt x pos lctx) = pushLCtxAt x (Nat.succ pos) (pushLCtx y lctx) := by
     apply funext; intro n; cases n; rfl; rw [pushLCtxAt_succ_succ];
-  
+
   theorem pushLCtxDep_zero {lctxty : α → Sort u} {xty : α} (x : lctxty xty)
     {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) :
     pushLCtxDep x lctx 0 = x := rfl
-  
+
   theorem pushLCtxDep_succ {lctxty : α → Sort u}
     {xty : α} (x : lctxty xty) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) (n : Nat) :
     pushLCtxDep x lctx (.succ n) = lctx n := rfl
@@ -444,7 +443,7 @@ section push
   theorem pushLCtxDep_succ_Fn {lctxty : α → Sort u}
     {xty : α} (x : lctxty xty) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) :
     (fun n => pushLCtxDep x lctx (.succ n)) = lctx := rfl
-  
+
   theorem pushLCtxDep_comm {α : Sort w} {β : α → Sort x} {rty : Nat → α} {lctxty : α → Sort u}
     (f : ∀ (x : α), lctxty x → β x) (lctx : ∀ n, lctxty (rty n))
     {xty : α} (x : lctxty xty) (n : Nat) :
@@ -455,7 +454,7 @@ section push
   theorem pushLCtx_commDep {β : α → Sort x} {x : α} {lctx : Nat → α} (f : ∀ (x : α), β x) :
     HEq (f (pushLCtx x lctx n)) (pushLCtxDep (f x) (fun n => f (lctx n)) n) := by
     cases n <;> rfl
-  
+
   theorem pushLCtxDep_absorbAux {rty : Nat → α} {lctxty : α → Sort u}
     (lctx : ∀ n, lctxty (rty n)) {xty : α} (x : lctxty xty) (n : Nat) :
     HEq
@@ -463,12 +462,12 @@ section push
       (@pushLCtxDep _ id _ x (lctxty ∘ rty) lctx n) := by
     dsimp [pushLCtx, pushLCtxDep]
     cases n <;> rfl
-  
+
   theorem pushLCtxDep_absorb {rty : Nat → α} {lctxty : α → Sort u}
     (lctx : ∀ n, lctxty (rty n)) {xty : α} (x : lctxty xty) :
     HEq (@pushLCtxDep _ lctxty _ x rty lctx) (@pushLCtxDep _ id _ x (lctxty ∘ rty) lctx) :=
     HEq.funext _ _ (fun n => pushLCtxDep_absorbAux lctx x n)
-  
+
   theorem pushLCtxDep_pushLCtxAtDep {rty : Nat → α} {lctxty : α → Sort u}
     (lctx : ∀ n, lctxty (rty n)) {xty : α} (x : lctxty xty) {yty : α} (y : lctxty yty) (pos : Nat) :
     HEq (pushLCtxDep y (pushLCtxAtDep x pos lctx)) (pushLCtxAtDep x (Nat.succ pos) (pushLCtxDep y lctx)) := by
@@ -587,7 +586,7 @@ section push
     cases h₁; cases h₂; cases h₃; cases h₄; cases h₅; cases h₆; apply HEq.rfl
 
   theorem pushLCtxsDep_substLCtx
-    {tys : List α} {lctxty : _} (xs : HList lctxty tys) 
+    {tys : List α} {lctxty : _} (xs : HList lctxty tys)
     {rty₁ : Nat → α} (lctx₁ : ∀ n, lctxty (rty₁ n))
     {rty₂ : Nat → α} (lctx₂ : ∀ n, lctxty (rty₂ n))
     (h₁ : rty₁ = rty₂) (h₂ : HEq lctx₁ lctx₂) :
@@ -638,7 +637,7 @@ section push
     (xs : HList lctxty tys) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) :
     HEq (fun n => pushLCtxsDep (.cons x xs) lctx (.succ n)) (pushLCtxsDep xs lctx) :=
     HEq.funext _ _ (fun n => pushLCtxsDep_cons_succ x xs lctx n)
-  
+
   theorem pushLCtxsDep_append {lctxty : α → Sort u}
     {as bs : List α} (xs : HList lctxty as) (ys : HList lctxty bs)
     {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) :
@@ -711,13 +710,13 @@ section push
     {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) :
     pushLCtxsAtDep xs (.succ pos) lctx 0 = lctx 0 := rfl
 
-  theorem pushLCtxsAtDep_succ_succ 
+  theorem pushLCtxsAtDep_succ_succ
     {lctxty : α → Sort u} {tys : List α} (xs : HList lctxty tys) (pos : Nat)
     {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) (n : Nat) :
     HEq (pushLCtxsAtDep xs (.succ pos) lctx (.succ n)) (pushLCtxsAtDep xs pos (fun n => lctx (.succ n)) n) := by
     dsimp [pushLCtxsAtDep]; apply restoreAtDep_succ_succ
 
-  theorem pushLCtxsAtDep_succ_succ_Fn 
+  theorem pushLCtxsAtDep_succ_succ_Fn
     {lctxty : α → Sort u} {tys : List α} (xs : HList lctxty tys) (pos : Nat)
     {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) :
     HEq (fun n => pushLCtxsAtDep xs (.succ pos) lctx (.succ n)) (pushLCtxsAtDep xs pos (fun n => lctx (.succ n))) := by
@@ -853,7 +852,7 @@ section pushs_pops
     pushLCtx (lctx 0) (fun n => lctx (.succ n)) = lctx := by
     apply funext
     intro n; cases n <;> rfl
-  
+
   theorem pushs_pops_eq (lctx : Nat → α) :
     pushLCtxs (List.ofFun lctx lvl) (fun n => lctx (n + lvl)) = lctx := by
     apply funext; intro n; dsimp [pushLCtxs, List.getD]
@@ -868,7 +867,7 @@ section pushs_pops
       dsimp [Nat.blt] at h;
       let h' := Nat.lt_of_ble_eq_false h
       exact Nat.le_of_succ_le_succ h'
-  
+
   theorem ofFun_pushs (heq : xs.length = n) :
     List.ofFun (pushLCtxs xs lctx) n = xs := by
     cases heq; induction xs generalizing lctx
@@ -903,14 +902,14 @@ end pushs_pops
 
 
 section add_nat
-  
+
   @[reducible] def addAt (lvl pos : Nat) := mapAt pos (fun x => x + lvl)
 
   @[reducible] def succAt := addAt 1
 
   theorem addAt_succ_zero (lvl pos : Nat) :
     addAt lvl (.succ pos) 0 = 0 := rfl
-  
+
   theorem addAt_succ_succ (lvl pos : Nat) (n : Nat) :
     addAt lvl (.succ pos) (.succ n) = .succ (addAt lvl pos n) := by
     dsimp [addAt]; rw [mapAt_succ_succ]
@@ -919,14 +918,14 @@ section add_nat
     addAt (.succ lvl) pos n = succAt pos (addAt lvl pos n) := by
     dsimp [addAt, Nat.add_succ]
     rw [mapAt_comp pos Nat.succ (fun x => x + lvl) n]
-  
+
   def addAt_succ_r (lvl pos : Nat) (n : Nat) :
     addAt (.succ lvl) pos n = addAt lvl pos (succAt pos n) := by
     dsimp [addAt];
     have heq : (fun x => x + Nat.succ lvl) = (fun x => (Nat.succ x) + lvl) := by
       apply funext; intros x; rw [Nat.succ_add]; rfl
     rw [heq]; rw [mapAt_comp pos (fun x => x + lvl) Nat.succ n]
-  
+
   def addAt_zero (pos : Nat) : addAt 0 pos = id := by
     apply funext; intro n;
     dsimp [addAt];
@@ -1018,17 +1017,17 @@ section genericInst
         rw [← IH xs heq lctx n]
         dsimp [pushLCtxs, Nat.blt, Nat.ble, Nat.add_succ]
         rw [Nat.succ_sub_succ]
-  
+
   theorem contraPair.ofPushsPops (lvl : Nat) (xs : List α) (heq : xs.length = lvl) :
     contraPair (fun n => n + lvl) (fun lctx => List.ofFun lctx lvl = xs) (pushLCtxs xs) := by
     intro lctx hcstr; cases hcstr; apply pushs_pops_eq
-  
+
   theorem coPairDep.ofPushsDepPopsDep
     {lctxty : α → Sort u} (lvl : Nat) {tys : List α}
     (xs : HList lctxty tys) (heq : tys.length = lvl) :
     coPairDep lctxty (fun x => x + lvl) (pushLCtxs tys) (pushLCtxsDep xs) :=
     And.intro (coPair.ofPushsPops lvl tys heq) (fun {rty} lctx n => by
-      dsimp [pushLCtxsDep, pushLCtxs]; 
+      dsimp [pushLCtxsDep, pushLCtxs];
       induction lvl generalizing tys lctx n
       case zero =>
         cases xs;
@@ -1051,4 +1050,4 @@ section genericInst
     And.intro (contraPair.ofPushsPops lvl tys heq) (fun {rty} hcstr lctx hcstrDep => by
       cases hcstr; cases hcstrDep; apply pushsDep_popsDep_eq)
 
-end genericInst
\ No newline at end of file
+end genericInst
diff --git a/Auto/Embedding/Lam2Base.lean b/Auto/Embedding/Lam2Base.lean
index ef2a2c4..27de546 100644
--- a/Auto/Embedding/Lam2Base.lean
+++ b/Auto/Embedding/Lam2Base.lean
@@ -1,5 +1,4 @@
 import Auto.Embedding.Lift
-import Std.Data.List.Lemmas
 
 namespace Auto.Embedding.Lam₂
 
@@ -120,7 +119,7 @@ def Lam₂Type.check_iff_interp
     simp [check, interp, Option.map]
   case bvar n =>
     simp [check, interp]
-    cases hLt : (Nat.decLt n (List.length lctx))
+    cases Nat.decLt n (List.length lctx)
     case isTrue h =>
       simp [h]; simp [List.get?_eq_get h]
     case isFalse h =>
@@ -148,7 +147,7 @@ def Lam₂Type.check_iff_interp
       | .some ⟨n + 1, _⟩, _ => simp
       | .none , _ => simp
     | .some 0, .none =>
-      simp; cases ciarg : interp val lctx arg <;> simp
+      simp; cases interp val lctx arg <;> simp
     | .some (n + 1), _ =>
       simp;
       match cifn : interp val lctx fn, ciarg : interp val lctx arg with
@@ -158,7 +157,7 @@ def Lam₂Type.check_iff_interp
       | .some ⟨n + 1, _⟩, _ => simp
       | .none , _ => simp
     | .none, _ =>
-      simp; cases cifn : interp val lctx fn <;> simp
+      simp; cases interp val lctx fn <;> simp
   case app fn arg IHfn IHarg =>
     revert IHfn IHarg
     simp [check, interp]
@@ -182,7 +181,7 @@ def Lam₂Type.check_iff_interp
       | .some ⟨0, _⟩, _ => simp
       | .none , _ => simp
     | .some (n + 1), none =>
-      simp; cases ciarg : interp val lctx arg <;> simp
+      simp; cases interp val lctx arg <;> simp
     | .some 0, _ =>
       simp;
       match cifn : interp val lctx fn with
@@ -190,6 +189,6 @@ def Lam₂Type.check_iff_interp
       | .some ⟨0, _⟩ => simp
       | .none => simp
     | .none, _ =>
-      simp; cases cifn : interp val lctx fn <;> simp
+      simp; cases interp val lctx fn <;> simp
 
-end Auto.Embedding.Lam₂
\ No newline at end of file
+end Auto.Embedding.Lam₂
diff --git a/Auto/Embedding/LamBitVec.lean b/Auto/Embedding/LamBitVec.lean
index 9ee1fce..52f3871 100644
--- a/Auto/Embedding/LamBitVec.lean
+++ b/Auto/Embedding/LamBitVec.lean
@@ -1,8 +1,5 @@
 import Auto.Embedding.LamConv
 import Auto.Lib.NatExtra
-import Std.Data.Int.Lemmas
-import Std.Data.Fin.Lemmas
-import Std.Data.BitVec.Lemmas
 
 namespace Auto.Embedding.Lam
 
@@ -96,7 +93,7 @@ namespace BVLems
     apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
 
   theorem ushiftRight_ge_length_eq_zero' (a : BitVec n) (i : Nat) : i ≥ n → (a.toNat >>> i)#n = 0#n := by
-    intro h; apply congr_arg (@BitVec.ofNat n)
+    intro h; apply congrArg (@BitVec.ofNat n)
     rw [Nat.shiftRight_eq_div_pow, Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)]
     apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
 
diff --git a/Auto/Embedding/LamConv.lean b/Auto/Embedding/LamConv.lean
index c065a3f..a2a9767 100644
--- a/Auto/Embedding/LamConv.lean
+++ b/Auto/Embedding/LamConv.lean
@@ -1,5 +1,4 @@
 import Auto.Embedding.LamSystem
-import Std.Data.Array.Basic
 
 namespace Auto.Embedding.Lam
 
diff --git a/Auto/Lib/BinTree.lean b/Auto/Lib/BinTree.lean
index 9189644..8b2e887 100644
--- a/Auto/Lib/BinTree.lean
+++ b/Auto/Lib/BinTree.lean
@@ -1,6 +1,4 @@
 import Lean
-import Std.Data.Nat.Lemmas
-import Std.Logic
 import Auto.MathlibEmulator
 import Auto.Lib.BoolExtra
 import Auto.Lib.NatExtra
diff --git a/Auto/Lib/IntExtra.lean b/Auto/Lib/IntExtra.lean
index 91d0e4d..5e2871e 100644
--- a/Auto/Lib/IntExtra.lean
+++ b/Auto/Lib/IntExtra.lean
@@ -1,5 +1,4 @@
 import Auto.Lib.NatExtra
-import Std.Data.Int.Lemmas
 namespace Auto
 
 def Int.beq : Int → Int → Bool
diff --git a/Auto/Lib/ListExtra.lean b/Auto/Lib/ListExtra.lean
index 190f7bb..0dec1f8 100644
--- a/Auto/Lib/ListExtra.lean
+++ b/Auto/Lib/ListExtra.lean
@@ -1,4 +1,3 @@
-import Std.Data.List.Lemmas
 import Auto.Lib.IsomType
 
 namespace Auto
diff --git a/Auto/Lib/Pos.lean b/Auto/Lib/Pos.lean
index 3a70a62..8d18437 100644
--- a/Auto/Lib/Pos.lean
+++ b/Auto/Lib/Pos.lean
@@ -1,5 +1,4 @@
 import Auto.MathlibEmulator
-import Std.Data.Nat.Lemmas
 
 namespace Auto
 
diff --git a/Auto/Translation/Assumptions.lean b/Auto/Translation/Assumptions.lean
index 6d9eda0..81d5fd1 100644
--- a/Auto/Translation/Assumptions.lean
+++ b/Auto/Translation/Assumptions.lean
@@ -1,5 +1,4 @@
 import Lean
-import Std.Data.Array.Basic
 import Auto.Lib.BoolExtra
 import Auto.Lib.MessageData
 import Auto.Lib.ExprExtra
diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean
index c51b28f..b89d179 100644
--- a/Auto/Translation/LamReif.lean
+++ b/Auto/Translation/LamReif.lean
@@ -1,5 +1,4 @@
 import Lean
-import Std.Data.Array.Basic
 import Auto.Lib.MonadUtils
 import Auto.Lib.ExprExtra
 import Auto.Lib.MetaExtra
diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
index 14a03de..32498f6 100644
--- a/Auto/Translation/Monomorphization.lean
+++ b/Auto/Translation/Monomorphization.lean
@@ -433,7 +433,7 @@ structure State where
   activeCi : Std.Queue (Expr × Nat)  := Std.Queue.empty
   -- During initialization, we supply an array `lemmas` of lemmas
   --   `liArr[i]` are instances of `lemmas[i]`.
-  lisArr    : Array LemmaInsts       := #[]
+  lisArr   : Array LemmaInsts       := #[]
 
 abbrev MonoM := StateRefT State MetaM
 
diff --git a/Test/SmtTranslation/MatchWorkaround.lean b/Test/SmtTranslation/MatchWorkaround.lean
index ade970b..ba4141e 100644
--- a/Test/SmtTranslation/MatchWorkaround.lean
+++ b/Test/SmtTranslation/MatchWorkaround.lean
@@ -1,5 +1,4 @@
 import Auto.Tactic
-import Std.Data.BitVec
 set_option auto.smt true
 set_option auto.smt.trust true
 set_option trace.auto.smt.printCommands true
diff --git a/lake-manifest.json b/lake-manifest.json
index 426f4dc..27b1b2d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,14 +1,5 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover/std4.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
-   "name": "std",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+ "packages": [],
  "name": "auto",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 2dea24a..3c8d68a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,9 +6,6 @@ package «auto» {
   preferReleaseBuild := true
 }
 
-require std from git
-  "https://github.com/leanprover/std4.git"@"main"
-
 @[default_target]
 lean_lib «Auto» {
   -- add any library configuration options here