Tactic documentation

Contents:

• apply
• assumption
• by_cases
• by_contra
• cases
• change
• choose
• convert
• exact
• exfalso
• ext
• have
• induction
• intro
• intros
• left
• linarith
• nlinarith
• norm_num
• nth_rewrite
• obtain
• rcases
• refine
• refl
• right
• ring
• rintro
• rw
• simp
• simpa
• specialize
• split
• triv
• use