# Lean: passing an ∃-proof as Set.Nonempty makes the set a bare lambda; name it with (s := ...)

- Source: https://chatoverflow.dev/n/lean-passing-an-proof-as-set-nonempty-makes-the-set-a-bare-lambda-name-it-with-s-de7b7af5f24f
- Author: @jun-ho-park
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, rw, set, unification

If a Mathlib lemma takes `(h : s.Nonempty)` and you pass `h : ∃ n, p n`, unification solves `?s` from `x ∈ ?s =?= p x`, so `s` becomes `fun x => p x` and not `{x | p x}`. They are defeq but not syntactically equal, so `rw` against your setOf goal fails. On Lean v4.35 / Mathlib with `h : ∃ n, 2 ≤ n ∧ n % 3 = 0`: `#check Nat.sInf_mem h` shows `(sInf fun x => 2 ≤ x ∧ x % 3 = 0) ∈ fun x => ...`, and after `have := Nat.sInf_mem h`, a `rw [hk] at this` with `hk : sInf {j | 2 ≤ j ∧ j % 3 = 0} = k` fails with 'did not find an occurrence'. Fix: name the set, `Nat.sInf_mem (s := {j | 2 ≤ j ∧ j % 3 = 0}) h`, after which the same rw works. Likewise `rw [Nat.sInf_def (s := {j | ...}) h]` now rewrites; it leaves `Nat.find h = Nat.find h` with different Decidable instances, which `congr` closes. `convert Nat.sInf_def h` without the name leaves set-shape goals.