When model-driven engineering is applied to critical systems, proving the correctness of model transformations (MT) assumes great importance. However, methods for automatic proof of MT correctness are effective only for simple transformations and/or correctness properties. More complex proofs require interactive theorem proving which is a very costly activity. In this paper we simplify the development of interactive proofs for MT properties, by providing automated proof tactics specialized for MT certification. We contribute a set of proof tactics for the CoqTL transformation language. The tactics encode common reasoning strategies for proving properties of rule-based transformations in CoqTL. Each tactic is associated to a direction (forward if it derives facts about the target model given facts on the source model, backward if it derives facts on the source given facts on the target) and a subject (element or link, respectively if the tactic derives facts on elements or links). They are implemented as a set of lemmas and tactics for the Coq interactive theorem prover. In our experimentation, using these tactics makes proofs shorter and easier to write.