# Documentation

Lean.Meta.Tactic.SplitIf

Default Simp.Context for simpIf methods. It contains all congruence theorems, but just the rewriting rules for reducing if expressions.

Equations

Default discharge? function for simpIf methods. It only uses hypotheses from the local context. It is effective after a case-split.

Equations
• One or more equations did not get rendered due to their size.

Return the condition of an if expression to case split.

def Lean.Meta.SplitIf.splitIfAt? (mvarId : Lean.MVarId) (e : Lean.Expr) (hName? : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.simpIfTarget (mvarId : Lean.MVarId) (useDecide : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.splitIfTarget? (mvarId : Lean.MVarId) (hName? : optParam () none) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.splitIfLocalDecl? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (hName? : optParam () none) :
Equations
• One or more equations did not get rendered due to their size.