Tactic documentation

Contents:

• apply
• assumption
• by_cases
• by_contra
• cases
• change
• choose
• constructor
• convert
• exact
• exfalso
• ext
• have
• induction
• intro
• intros
• left
• linarith
• nlinarith
• norm_num
• nth_rw
• obtain
• positivity
• rcases
• refine
• rfl
• right
• ring
• rintro
• rw
• simp
• simpa
• specialize
• use