Cases on fin 2

Stream: new members

[Thomas Read]

Is there an easy way to do cases on a fin 2? Specifically I'd like to show that if we have
swap : fin 2 → fin 2 := λ x, if x = 0 then 1 else 0 then swap(swap(x)) = x.

I can repeatedly do cases on the fin to eventually get the answer, but it seems very tedious.

[Johan Commelin]

You could see if the library know about an equivalence between fin 2 and bool

[Johan Commelin]

Your problem might also be a good job for the case_bash tactic

[Johan Commelin]

Which is hiding somewhere in mathlib, if I'm not mistaken

[Bryan Gin-ge Chen]

Is this something fin_cases can do?

[Thomas Read]

Awesome, that works perfectly!

[Johan Commelin]

Aah, that's the one I meant