by_cases for Sigma type/exists clause with explicit element

Stream: new members

[Theo Müller]

Hello,

say I have a function f: Nat → Nat and then want to prove a theorem like

def g : Σ' (f: Nat), f n = 20 := sorry

using some properties of f. (The important point here being that g explicitly names an x, and is not just a Prop).
In the proof, I (in my example) want to make a distinction of cases on whether f n < 10 for all n < 1000, or not. In the latter case, I want to find an explicit n where ¬(f n < 10).
Now, I can run by_cases ∀ (n: Fin 1000), f n < 10 just fine, and ∀ (n: Fin 1000), f n < 10 is even computable, but in the negative case I obtain ¬(∀ (n: Fin 1000), f n < 10), which (as far as I know) I can only turn into ∃ (n: Fin 1000), ¬(f n < 10), which is a Prop (so that I cannot get an explicit n out of it when not proving a Prop).

Is there some clean solution here, or do I need to define my own helper functions to recursively find such an n given the assumption that ¬(∀ (n: Fin 1000), f n < 10)?

[Yakov Pechersky]

You can get an explicit n out using Nat.find, which by construction is the least such n satisfying your predicate