nat.find

Stream: new members

[Joachim Breitner]

I am a bit unsure about the best way to phrase a lemma about nat.find. Consider something like the following. Which formulation of the lemma about nat.find is best?

lemma green_are_followed_by_red n (hG : is_green n) : ∃ m > n. is_red m := …

lemma first_red_after_green_is_joe1 n (hG : is_green n) :
  (h : ∃ m > n. is_red m)
  nat.find h = joe

lemma first_red_after_green_is_joe2 n (hG : is_green n) :
  let h : ∃ m > n. is_red m := green_are_followed_by_red n hG in
  nat.find h = joe

lemma first_red_after_green_is_joe3 n (hG : is_green n) :
  nat.find (green_are_followed_by_red n hG) = joe

The first is most readable, but annoying to use – you have to provide a proof for h when you want to use the lemma.
The last is compact, but it somehow look silly to me to give a _specific_ proof term for that existential here (and indeed later lean prints this as nat.find _ = joe, because the proof term doesn’t matter…).
The middle one might be a compromise.

Or maybe I am approaching this the wrong way?

(If you want a more real example; this comes up when proving that various possible nilpotency class definitions are equivalent.)