  In theorem provers based on dependent type theory such as Coq and Lean,
induction is a fundamental proof method and induction tactics are omnipresent
in proof scripts. Yet the ergonomics of existing induction tactics are not
ideal: they do not reliably support inductive predicates and relations; they
sometimes generate overly specific or unnecessarily complex induction
hypotheses; and they occasionally choose confusing names for the hypotheses
they introduce.
  This paper describes a new induction tactic, implemented in Lean 3, which
addresses these issues. The tactic is particularly suitable for educational
use, but experts should also find it more convenient than existing induction
tactics. In addition, the tactic serves as a moderately complex case study for
the metaprogramming framework of Lean 3. The paper describes some difficulties
encountered during the implementation and suggests improvements to the
framework.
