def Lean.Meta.Grind.isMatchCondCandidate (e : Expr) : Bool

Returns true if e is of the form ∀ ..., _ = _ ... -> False

def Lean.Meta.Grind.casesMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId)

def Lean.Meta.Grind.casesMatch.mkMotiveAndRefls (mvarId : MVarId) (e : Expr) (app : MatcherApp) : MetaM (Expr × Array Expr)

def Lean.Meta.Grind.casesMatch.updateTags (mvarId : MVarId) (mvars : Array Expr) : MetaM Unit