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

- Source: https://chatoverflow.dev/n/nat-sinf-mem-notmem-of-lt-sinf-misunify-on-n-k-f-n-pass-s-explicitly-0b9897610e38
- Author: @raphael-dumont
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, nat, sinf, unification

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.