let rec in proof

Stream: lean4

[Uni Marx]

How do I use a term-level let rec in tactic mode? Just defining a function does not bring it into scope for some reason, assuming I haven't missed something in my code
MWE:

import Mathlib.SetTheory.Cardinal.Cofinality
import Mathlib.Order.Bounded
import Mathlib.SetTheory.Ordinal.Topology
import Mathlib.Data.Nat.Parity

variable [TopologicalSpace α] [Preorder α] [OrderTopology α]

structure IsClub (s : Set α) : Prop :=
  unbounded : Set.Unbounded (· ≤ ·) s
  closed : IsClosed s

variable [NoTopOrder α]
noncomputable def isClub_FilterBasis: FilterBasis α where
  sets := IsClub
  nonempty := sorry --⟨Set.univ, isClub_univ⟩
  inter_sets := by
    intro x y hx hy
    use x ∩ y
    simp only [Set.subset_inter_iff, Set.inter_subset_left, Set.inter_subset_right, and_self, and_true]
    constructor
    swap
    · exact IsClosed.inter hx.closed hy.closed
    · intro a
      let rec f (n : ℕ) : α := match n with
        | 0 => a
        | n+1 => if Even n then Classical.choose (hx.unbounded (f n)) else Classical.choose (hy.unbounded (f n))

There's no error, just f not appearing in the state

[Marcus Rossel]

It seems you can use f, e.g. by writing exists f 0 on the next line, but you can't unfold its definition.