assume h and then prove cases for h and not h

Stream: Is there code for X?

[Ariel Fridman]

I am currently proving some (elementary) results about groups, and I got to a lemma where it would be easier to split into cases where g is equal to the identity element, and g is surely not the identity element.

Is there some kind of cases variant for such a thing? I am not a constructivist so if such a tactic only works in classical mode that's ok with me too.

[Yakov Pechersky]

by_cases h : g = 1

[Ariel Fridman]

@Yakov Pechersky oops, now I feel bad that I haven't found it by myself, with such a simple naming ^^'. Thank you!

[Kevin Buzzard]

Sometimes when I was learning I would just read through all of https://leanprover-community.github.io/mathlib_docs/tactics.html , but honestly it's easier to ask here :-)

[Kevin Buzzard]

I actually find by_cases annoying sometimes, because the second case will be \not g = 1 rather than g \ne 1. I often do cases eq_or_ne g 1 in this situation (or whatever it's called)

[Ariel Fridman]

I first try searching the docs, of course. but sometimes you just miss stuff, or stuff is not documented in an easy-to-find way. This is probably not the case for by_cases though, that's just me ^^'.

[Yakov Pechersky]

rcases eq_or_ne g 1 with rfl|h -- if eq_or_ne existed

to even skip the rw [h] step, and have g automatically be substituted with 1 everywhere.

[Ariel Fridman]

Kevin Buzzard said:

I actually find by_cases annoying sometimes, because the second case will be \not g = 1 rather than g \ne 1. I often do cases eq_or_ne g 1 in this situation (or whatever it's called)

hmm, I did a rename and change, but if this works then it sound better in this situation. Thanks for the tip!

[Kevin Buzzard]

I've said that, but now I think about it I'm usually in a situation where I want to split on <= or >, and I use le_or_gt because I don't want the second case to be "not le". I've just looked around a bit and I can't even find eq_or_ne and am now wondering if it even exists!

[Ariel Fridman]

I also tried to search through the docs, and couldn't see something like that, but it looks useful for these kind of situations. Is this something one can just PR into the language, or is there some RFC process for such a thing?

[Yakov Pechersky]

Kevin, are you working with solely with the naturals, and are doing cases k.zero_le.eq_or_lt and relying on the fact that 0 < k \iff 0 \ne k :upside_down: