mathlib documentation

tactic.auto_cases

meta structure tactic.auto_cases.auto_cases_tac  :
Type 1

Structure representing a tactic which can be used by tactic.auto_cases.

The auto_cases_tac for tactic.induction⟩.

Find an auto_cases_tac which matches the given type : expr.

Applies cases or induction on the local_hypothesis hyp : expr.

Applies cases or induction on certain hypotheses.