diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 677fa2a614..0345ffb9ce 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -23,6 +23,7 @@ structure Context where
   congrLemmas    : CongrLemmas := {}
   parent?        : Option Expr := none
   dischargeDepth : Nat      := 0
+  deriving Inhabited
 
 def Context.mkDefault : MetaM Context :=
   return { config := {}, simpLemmas := (← getSimpLemmas), congrLemmas := (← getCongrLemmas) }
diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
new file mode 100644
index 0000000000..6e738acad6
--- /dev/null
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.LazyInitExtension
+import Lean.Meta.Tactic.Simp.Types
+
+namespace Lean.Meta
+namespace SplitIf
+
+builtin_initialize ext : LazyInitExtension MetaM Simp.Context ←
+  registerLazyInitExtension do
+    let mut s : SimpLemmas := {}
+    s ← s.addConst ``if_pos
+    s ← s.addConst ``if_neg
+    s ← s.addConst ``dif_pos
+    s ← s.addConst ``dif_neg
+    return {
+      simpLemmas    := s
+      congrLemmas   := (← getCongrLemmas)
+      config.zeta   := false
+      config.beta   := false
+      config.eta    := false
+      config.iota   := false
+      config.proj   := false
+      config.decide := false
+    }
+
+def getSimpContext : MetaM Simp.Context :=
+  ext.get
+
+end SplitIf
+end Lean.Meta