Getting a proof of a proposition in a function by cases

Stream: new members

[Ryan Greenblatt]

Consider the following code:

def f (n : ℕ) : ℕ :=
if n = 1 then
  have h : n = 1 :=
    begin
      -- what do I do here?
    end,
  3
else
  4

I need a proof of h in the function, but I'm not sure how to get it. Probably there is some approach to branch on the proposition other than 'if then else'?
I tried writing a 'begin end' block and using cases' classical.em (n = 1), but that failes with induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop