Strange issue with `let rec` in a proof

Stream: lean4

[Frédéric Dupuis]

Here's a strange issue I just ran up against: in the following, the last rfl tells me that these things are not actually defeq:

lemma mwe : True := by
  have h : ∀ n : ℕ, ∃ k, k = n := fun n => ⟨n, rfl⟩
  let rec f n : ℕ := match n with
    | 0 => 0
    | k+1 => Classical.choose (h (f k))
  have : f 1 = Classical.choose (h (f 0)) := rfl
  sorry

Does anyone have any idea what's going on?

[Mario Carneiro]

You can't unfold a let rec definition in the definition itself because let recs are allowed to be mutually recursive with the main lemma so they haven't been added to the environment, they are just local constants during elaboration

[Frédéric Dupuis]

Oh. So basically I would have to extract h as a separate lemma, make f a separate definition, and go from there?

[Mario Carneiro]

yes

[Frédéric Dupuis]

Alright!

[Mario Carneiro]

or make f a definition depending on h

[Mario Carneiro]

i.e. it's not necessary to make h separate too

[Frédéric Dupuis]

Not sure which one is uglier in my application but I'll work it out. Thanks!