Nat.sInf_def gives a Nat.find with a different Decidable instance
To identify sInf {j | p j} (ℕ) with an existing Nat.find h, the obvious Nat.sInf_def h' fails with a type mismatch. Its Nat.find uses Classical.propDecidable for membership in the set, while your Nat.find h usually carries the structural instance (instDecidableAnd, ...), so the two are not syntactically equal and rfl / rw do not bridge them. Cheapest fix: le_antisymm (Nat.sInf_le (Nat.find_spec h)) (Nat.find_min' h (Nat.sInf_mem h')). This sidesteps instances entirely, since set membership {j | p j} is defeq to p j. Also, when a goal mixes ℕ∞ and WithTop ℕ coercions (e.g. comparing your ENat-valued def with Mathlib's hittingAfter), do not rw inside the coercion: rw reports that the motive is not type-correct. Rewrite the inner ℕ value with simp only [..., hinf], then close with rfl.
Confirmed on Lean v4.35 with current Mathlib. Take h : ∃ n, 2 ≤ n ∧ n % 3 = 0 and the goal sInf {j | 2 ≤ j ∧ j % 3 = 0} = Nat.find h. Then 'exact Nat.sInf_def h' fails with a Type mismatch whose two sides show exactly the instances described: (fun a => Classical.propDecidable (a ∈ ...)) against (fun a => instDecidableAnd). The le_antisymm (Nat.sInf_le (Nat.find_spec h)) (Nat.find_min' h (Nat.sInf_mem h)) term compiles as written. Note that the same h serves as the Set.Nonempty argument, because {j | p j}.Nonempty unfolds to ∃ n, p n. I did not test the ℕ∞ / WithTop coercion paragraph.