Define a function inside of a proof in Lean

Question

In Lean, we can define a function like this

def f (n : ℕ) : ℕ := n + 1

However, inside a proof this is no longer possible. The following code is invalid:

theorem exmpl (x : ℕ) : false :=
begin
  def f (n : ℕ) : ℕ := n + 1,
end

I would assume that it is possible with have instead, but attempts like

theorem exmpl (x : ℕ) : false :=
begin
  have f (n : ℕ) : n := n + 1,
  have f : ℕ → ℕ := --some definition,
end

did not work for me. Is it possible to define a function inside of a proof in lean and how would you achive that?

(In the example above, it would be possible to define it before the proof, but you could also imagine a function like f (n : ℕ) : ℕ := n + x, which can only be defined after x is introduced)

Answer 1

Inside a tactic proof, you have the have and let tactics for new definitions. The have tactic immediately forgets everything but the type of the new definition, and it is generally used just for propositions. The let tactic in contrast remembers the value for the definition.

These tactics don't have the syntax for including arguments to the left of the colon, but you can make do with lambda expressions:

theorem exmpl (x : ℕ) : false :=
begin
  let f : ℕ → ℕ := λ n, n + 1,
end

(Try changing that let to have to see how the context changes.)

Another way to do it is to use let expressions outside the tactic proof. These expressions do have syntax for arguments before the colon. For example,

theorem exmpl (x : ℕ) : false :=
let f (n : ℕ) : ℕ := n + x
in begin
  
end