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

Question

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

Answer 1

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

Answer 2

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)