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.

Find an auto_cases_tac which matches the given type : expr.

meta def tactic.auto_cases_at (hyp : expr) :

Applies cases or induction on the local_hypothesis hyp : expr.

Applies cases or induction on certain hypotheses.