diff --git a/src/Lean.lean b/src/Lean.lean
index 5da1bb9c2435..9e2d798c190c 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -30,7 +30,6 @@ import Lean.Server
 import Lean.ScopedEnvExtension
 import Lean.DocString
 import Lean.DeclarationRange
-import Lean.LazyInitExtension
 import Lean.LoadDynlib
 import Lean.Widget
 import Lean.Log
diff --git a/src/Lean/LazyInitExtension.lean b/src/Lean/LazyInitExtension.lean
deleted file mode 100644
index f50b7453cc52..000000000000
--- a/src/Lean/LazyInitExtension.lean
+++ /dev/null
@@ -1,42 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.MonadEnv
-
-namespace Lean
-
-structure LazyInitExtension (m : Type → Type) (α : Type) where
-  ext : EnvExtension (Option α)
-  fn  : m α
-
-instance [Monad m] [Inhabited α] : Inhabited (LazyInitExtension m α) where
-  default := {
-    ext := default
-    fn  := pure default
-  }
-
-/--
-  Register an environment extension for storing the result of `fn`.
-  We initialize the extension with `none`, and `fn` is executed the
-  first time `LazyInit.get` is executed.
-
-  This kind of extension is useful for avoiding work duplication in
-  scenarios where a thunk cannot be used because the computation depends
-  on state from the `m` monad. For example, we may want to "cache" a collection
-  of theorems as a `SimpLemmas` object.  -/
-def registerLazyInitExtension (fn : m α) : IO (LazyInitExtension m α) := do
-  let ext ← registerEnvExtension (pure none)
-  return { ext, fn }
-
-def LazyInitExtension.get [MonadEnv m] [Monad m] (init : LazyInitExtension m α) : m α := do
-  match init.ext.getState (← getEnv) with
-  | some a => return a
-  | none   =>
-    let a ← init.fn
-    modifyEnv fun env => init.ext.setState env (some a)
-    return a
-
-end Lean
diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
index 32d954df6feb..d6a21e31495f 100644
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -4,31 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.LazyInitExtension
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 namespace SplitIf
 
-builtin_initialize ext : LazyInitExtension MetaM Simp.Context ←
-  registerLazyInitExtension do
-    let mut s : SimpTheorems := {}
-    s ← s.addConst ``if_pos
-    s ← s.addConst ``if_neg
-    s ← s.addConst ``dif_pos
-    s ← s.addConst ``dif_neg
-    return {
-      simpTheorems  := #[s]
-      congrTheorems := (← getSimpCongrTheorems)
-      config        := { Simp.neutralConfig with dsimp := false }
-    }
-
 /--
   Default `Simp.Context` for `simpIf` methods. It contains all congruence theorems, but
   just the rewriting rules for reducing `if` expressions. -/
-def getSimpContext : MetaM Simp.Context :=
-  ext.get
+def getSimpContext : MetaM Simp.Context := do
+  let mut s : SimpTheorems := {}
+  s ← s.addConst ``if_pos
+  s ← s.addConst ``if_neg
+  s ← s.addConst ``dif_pos
+  s ← s.addConst ``dif_neg
+  return {
+    simpTheorems  := #[s]
+    congrTheorems := (← getSimpCongrTheorems)
+    config        := { Simp.neutralConfig with dsimp := false }
+  }
 
 /--
   Default `discharge?` function for `simpIf` methods.