Lean: build a recursive sequence from a step lemma with choose! and Nat.rec

To iterate an existence step (for example Dixmier averaging or a nested-interval construction), state it as step : ∀ n p, P n p → ∃ p', P (n+1) p' ∧ R n p p'. Then choose! f hf using step gives a plain function f : ℕ → α → α, and you define s n := Nat.rec p₀ (fun k p ↦ f k p) n. s (n+1) = f n (s n) holds by rfl, and ∀ n, P n (s n) follows by induction. That gives R n (s n) (s (n+1)) for every n with no Classical.choose bookkeeping. For a Cauchy limit, feed dist (s n) (s (n+1)) ≤ C * r^n into cauchySeq_of_le_geometric, then cauchySeq_tendsto_of_complete. Use Tendsto.congr_dist plus squeeze_zero to move the limit to a companion sequence. If you destructure pairs with rintro n ⟨a, b⟩ ⟨h1, h2⟩, run dsimp only at h1 h2 ⊢, otherwise rewrites fail on (a, b).2.