mathlib3 documentation

tactic.auto_cases

meta structure tactic.auto_cases.auto_cases_tac  :

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

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.