def Lean.Meta.CheckTactic.mkCheckGoalType (val type : Expr) : MetaM Expr

def Lean.Meta.CheckTactic.matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level)