def Lean.Meta.Match.simpH (mvarId : MVarId) (numEqs : Nat) : MetaM (Option MVarId)

Like simpH?, but works directly on a goal corresponding to the unsimplified equational theorem hypothesis, and either closes it or returns a residual goal whose type is the simplified equational theorem hypothesis.

def Lean.Meta.Match.simpH? (h : Expr) (numEqs : Nat) : MetaM (Option Expr)

Auxiliary method for simplifying equational theorem hypotheses.

Recall that each equation contains additional hypotheses to ensure the associated case was not taken by previous cases. We have one hypothesis for each previous case.