One of the main goals of formalizing mathematics is to develop automation strategies/tactics that prove (partial) goals without requiring any input from the user. In this talk we show how to achieve this desideratum for the domain of real analysis in the proof assistant Coq, by defining ever more powerful tactics through two different strategies: the Auto with Hints mechanism and the use of Reflection.