Lecture 13, Level 1: Monotone Subsequence: if-then-else

[thomas-strohmann]

The Strategy Outline recommends:
Define τ'(n) = if n ≤ k then n+1 else τ(n) that grows faster than identity everywhere

Presumably the intended Lean implementation is
let τ' : ℕ → ℕ := fun n ↦ if h : n ≤ k then n+1 else τ n (lt_of_not_ge h)

It's not so clear though (at least to me) how one then uses the "then" and "else" branches later in the proof
(maybe there are even some additional tactic(s) needed to do this?). For example:

apply Subseq_of_Iterate
intro n -- goal becomes: n < τ' n
by_cases h : n ≤ k
have f0 : τ' n = n + 1 := by sorry

I think it would be really helpful to have a hint/tactic that allows plugging in the "then" branch of τ'.

Thanks

[AlexKontorovich]

Was there a reason to close this issue? I would like to address it (in the future)

[thomas-strohmann]

After seeing the reference solution here https://github.com/AlexKontorovich/RealAnalysisGame/blob/main/Game/Levels/L13Levels/L03_MonotoneSubseq.lean
(the following:
let τ' : ℕ → ℕ := fun n => if h : n ≤ k then n + 1 else τ n (lt_of_not_ge h)
have τ'_eq : ∀ n, τ' n = if h : n ≤ k then n + 1 else τ n (lt_of_not_ge h) := by intro n; rfl
have τ'_gt : ∀ n, n < τ' n := by
intro n;
by_cases hn : n ≤ k;
rewrite [τ'_eq];
bound;
rewrite [τ'_eq];
bound)
It seemed like in retrospect that I should have thought of trying this approach (starting with have τ'_eq : ∀ n, τ' n = ... and then relying on rewrite/bound to prove ∀ n, n < τ' n). But you're right, maybe others will also get stuck here so a hint could still be helpful. Thanks!