English
FindX is the subset of ℕ^+ consisting of those n with p(n) and such that no smaller m satisfies p(m); it encodes a canonical minimal witness.
Русский
FindX — множество элементов ℕ^+, для которых выполнено p(n) и для всех m < n не выполняется p(m).
LaTeX
$$$ \\{ n \\in \\mathbb{N}^+ \\mid p(n) \\land \\forall m < n, \\neg p(m) \\} $$$
Lean4
/-- The `PNat` version of `Nat.findX` -/
protected def findX : { n // p n ∧ ∀ m : ℕ+, m < n → ¬p m } :=
by
have : ∃ (n' : ℕ) (n : ℕ+) (_ : n' = n), p n := Exists.elim h fun n hn => ⟨n, n, rfl, hn⟩
have n := Nat.findX this
refine ⟨⟨n, ?_⟩, ?_, fun m hm pm => ?_⟩
· obtain ⟨n', hn', -⟩ := n.prop.1
rw [hn']
exact n'.prop
· obtain ⟨n', hn', pn'⟩ := n.prop.1
simpa [hn', Subtype.coe_eta] using pn'
· exact n.prop.2 m hm ⟨m, rfl, pm⟩
