Tactic documentation
====================

.. toctree::
   :maxdepth: 1
   :caption: 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
   triv	     
   use