Tactics for splitting if statements

Stream: lean4

[Jeremy Salwen]

Suppose I am proving a theorem like

theorem splitme (i:ℤ) (P: if i = 0 then Q else R): Q ∨ R

How would I "split the if statement" in P into two cases? The split tactic seems to only be for the goal, not hypotheses. The cases tactic refuses to split on i=0. I have figured out a workaround of usingcases heq: i==0 and then using (i==0) = true to prove i=0 and simplify away the if, but this seems overly convoluted.

[David Renshaw]

does split at P work?

[Jeremy Salwen]

Ah, that does work! It is not mentioned by the split docs!

[Kevin Buzzard]

Nice catch! Docs PRs are always welcome!

[Kevin Buzzard]

docs4#split

[Kevin Buzzard]

tactic4#split

[Kevin Buzzard]

hmm, I don't know how to summon links to tactic docstrings in Lean 4.

[Jeremy Salwen]

Created this PR to improve the docs! https://github.com/leanprover/lean4/pull/1988