Take a match branch

Stream: lean4

[Hanting Zhang]

How would I take the match branch in a situation like this?

def f (i : Nat) : Nat :=
  match i with
  | 0 => 2
  | i + 1 => 3

theorem take_match (h : 0 < i) : f i = 3 := by
  unfold f
  -- How do I convince Lean that `i` is in the `succ` case?
  sorry

For more context, I have a large proof, and a large match statement. I know my hypotheses imply that one of the branches must be taken. Is there some way to do "casework" here? One approach I see is to consider both branches, and then clearly the 0 branch would be contradictory. However, trying cases doesn't seem to work, so I'm stuck. Thank you!

[Aaron Liu]

The tactic for this is called split. In this case, it gives two goals, one corresponding to each match branch.

theorem take_match (h : 0 < i) : f i = 3 := by
  unfold f
  -- How do I convince Lean that `i` is in the `succ` case?
  split
  · contradiction
  · rfl

[Hanting Zhang]

Thanks!

[Edward van de Meent]

Alternatively, I think cases h might do the right thing?