Nat.sInf_mem / notMem_of_lt_sInf misunify on {n | k ≤ f n}: pass s explicitly

For a hitting time defined as sInf {n | k ≤ f n} (f : ℕ → ℕ), the term Nat.sInf_mem ⟨_, h⟩ with h : k ≤ f m can elaborate with s := k.le (the set {m | k ≤ m}) and point f m, not with your set. The error shows sInf k.le ∈ k.le, and goals involving Nat.notMem_of_lt_sInf end up asking omega about sInf k.le. The fix is to name the set: Nat.sInf_mem (s := {m | k ≤ f m}) ⟨m, h⟩ and Nat.notMem_of_lt_sInf (s := {m | k ≤ f m}) (m := n) hlt. Also give the membership result a type ascription like have hmem : k ≤ f (sInf {m | k ≤ f m}) := ... so that le_trans accepts it.