tactic.trunc_cases - mathlib3 docs

source

meta def tactic.interactive.trunc_cases (e : interactive.parse interactive.types.texpr) (ids : interactive.parse interactive.types.with_ident_list) :

tactic unit

trunc_cases e performs case analysis on a trunc expression e, attempting the following strategies:

when the goal is a subsingleton, calling induction e using trunc.rec_on_subsingleton,
when the goal does not depend on e, calling fapply trunc.lift_on e, and using intro and clear afterwards to make the goals look like we used induction,
otherwise, falling through to trunc.rec_on, and in the new invariance goal calling cases h_p on the useless h_p : true hypothesis, and then attempting to simplify the eq.rec.

trunc_cases e with h names the new hypothesis h. If e is a local hypothesis already, trunc_cases defaults to reusing the same name.

trunc_cases e with h h_a h_b will use the names h_a and h_b for the new hypothesis in the invariance goal if trunc_cases uses trunc.lift_on or trunc.rec_on.

Finally, if the new hypothesis from inside the trunc is a type class, trunc_cases resets the instance cache so that it is immediately available.

source

def tactic_doc.tactic.trunc_cases :

tactic_doc_entry

trunc_cases e performs case analysis on a trunc expression e, attempting the following strategies:

when the goal is a subsingleton, calling induction e using trunc.rec_on_subsingleton,
when the goal does not depend on e, calling fapply trunc.lift_on e, and using intro and clear afterwards to make the goals look like we used induction,
otherwise, falling through to trunc.rec_on, and in the new invariance goal calling cases h_p on the useless h_p : true hypothesis, and then attempting to simplify the eq.rec.

trunc_cases e with h names the new hypothesis h. If e is a local hypothesis already, trunc_cases defaults to reusing the same name.

trunc_cases e with h h_a h_b will use the names h_a and h_b for the new hypothesis in the invariance goal if trunc_cases uses trunc.lift_on or trunc.rec_on.

Finally, if the new hypothesis from inside the trunc is a type class, trunc_cases resets the instance cache so that it is immediately available.