case split on Fin?

Stream: lean4

[Ben Selfridge]

I'm trying to define a function Fin 5 to Fin 5, like so:

example (x : Fin 5) : Fin 5 := by
  -- 0 ↦ 2
  -- 1 ↦ 3
  -- 2 ↦ 4
  -- 3 ↦ 1
  -- 4 ↦ 0
  sorry

Is there a clean way to do this?

[Henrik Böving]

def foo (x : Fin 5) : Fin 5 :=
  match x with
  | 0 => 2
  | 1 => 3
  | 2 => 4
  | 3 => 1
  | 4 => 0

[Ben Selfridge]

Thanks. I had a feeling it was that easy, but for some reason couldn't get the syntax right.

[Ben Selfridge]

Followup question: I'm trying to finish the sorry below without having to list out all the cases again. Any ideas?

def f : Fin 5 → Fin 5 := fun x => match x with
  | 0 => 2
  | 1 => 3
  | 2 => 4
  | 3 => 1
  | 4 => 0

def g : Fin 5 → Fin 5 := fun x => match x with
  | 2 => 0
  | 3 => 1
  | 4 => 2
  | 1 => 3
  | 0 => 4

example : f ∘ g = id := by
  funext x
  simp [f, g]
  sorry

[Ilmārs Cīrulis]

import Mathlib.Tactic.FinCases

def f : Fin 5 → Fin 5 := fun x => match x with
  | 0 => 2
  | 1 => 3
  | 2 => 4
  | 3 => 1
  | 4 => 0

def g : Fin 5 → Fin 5 := fun x => match x with
    | 2 => 0
    | 3 => 1
    | 4 => 2
    | 1 => 3
    | 0 => 4

example : f ∘ g = id := by
  funext x
  simp [f, g]
  fin_cases x <;> simp

[Ilmārs Cīrulis]

em, I forgot how to narrow imports to only what's necessary... but fin_cases x should be solution, I believe

[Ben Selfridge]

Where does fin_cases live?

[Ben Selfridge]

Ah, nvm got it

[Ben Selfridge]

Thanks!!