# How to show that an expression of a finite type must be one of the finitely many possible values?

In Lean, how do I prove that a variable, or more generally an expression, ranging over a finite type must be equal to one of the values of the finite type?

In particular, the following should be easy, but I do not know where to begin:

inductive Foo where
| alice
| bob
| charles

open Foo

inductive Bar where
| boy
| girl

open Bar

def f : Foo → Bar
| charles => boy
| alice => girl
| bob => boy

example (x:Foo) (h: f x = boy): (x=bob ∨ x=charles) :=
sorry


Here's a shorter proof using the equation compiler:

example : ∀ (x : Foo), f x = boy → x = bob ∨ x = charles
| .bob, _ => .inl rfl
| .charles, _ => .inr rfl


Here is a verbose/expressive proof in "term mode":

example (x:Foo) (h: f x = boy): (x=bob ∨ x=charles) :=
match x with
| bob =>
have h : bob = bob := rfl
show bob=bob ∨ bob=charles from Or.inl h
| charles =>
have h : charles = charles := rfl
show charles=bob ∨ charles=charles from Or.inr h
| alice =>
have h1 : f alice = girl := rfl
have h2 : girl ≠ boy := Bar.noConfusion
have h3 : f alice = boy := h
have h4 : girl = boy := h1 ▸ h3
show alice=bob ∨ alice=charles from False.elim  (h2 h4)