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

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.