by_cases and if then else tactics

This implements the if tactic, which is a structured proof version of by_cases. It allows writing if h : t then tac1 else tac2 for case analysis on h : t,

def tacDepIfThenElse : Lean.ParserDescr

In tactic mode, if h : t then tac1 else tac2 can be used as alternative syntax for:

by_cases h : t
· tac1
· tac2

It performs case distinction on h : t or h : ¬t and tac1 and tac2 are the subproofs.

You can use ?_ or _ for either subproof to delay the goal to after the tactic, but if a tactic sequence is provided for tac1 or tac2 then it will require the goal to be closed by the end of the block.

Equations

• One or more equations did not get rendered due to their size.

def tacIfThenElse : Lean.ParserDescr

In tactic mode, if t then tac1 else tac2 is alternative syntax for:

by_cases t
· tac1
· tac2

It performs case distinction on h† : t or h† : ¬t, where h† is an anonymous hypothesis, and tac1 and tac2 are the subproofs. (It doesn't actually use nondependent if, since this wouldn't add anything to the context and hence would be useless for proving theorems. To actually insert an ite application use refine if t then ?_ else ?_.)

Equations

• One or more equations did not get rendered due to their size.