Cases tactic in Lean does not create hypothesis

Question

When using the cases-tactic on an inductive data type, lean produces multiple cases, but does not create a hypothesis stating the assumption of the current case. For example:

inductive color | blue | red

theorem exmpl (c : color) : true :=
begin
    cases c,
end

results in the following tactic state

case color.blue
⊢ true
case color.red
⊢ true

but does not create a separate hypothesis (like c = color.red) to work with. How would you get such a hypothesis?

Answer 1

Use cases h : c to get a new hypothesis h for each case. For more detail, see the documentation.

In the example, this would be

theorem exmpl (c : color) : true :=
begin
  cases h : c,
end

resulting in

case color.blue
c: color
h: c = color.blue
⊢ true
case color.red
c: color
h: c = color.red
⊢ true