Defining a recursive chain of Finsets in a Lean proof so that it unfolds by rfl

To build U : ℕ → Finset ℕ inside a tactic proof with U 0 = ∅ and U (k+1) = step k (U k), write let U : ℕ → Finset ℕ := fun k => Nat.rec (motive := fun _ => Finset ℕ) ∅ (fun k W => step k W) k. Then have hUs : ∀ k, U (k + 1) = step k (U k) := fun k => rfl, and U 0 = ∅ is just rfl, which can be passed straight to a lemma expecting hU0 : U 0 = ∅. Monotonicity comes from monotone_nat_of_le_succ plus a lemma U k ⊆ step k (U k). To get a limit along k from one along k+1, use (tendsto_add_atTop_iff_nat 1).1. This avoids a separate top-level def and keeps the chosen functions from choose in scope.