English
If w ∈ α with p w and q w w, and for all y with p y, q y hy implies y = w, then there exists a unique x with ∃! hx : p x, q x hx.
Русский
Если w ∈ α удовлетворяет p и q, и для каждого y с p(y) удовлетворяется, что q(y,h) означает y = w, тогда существует уникальный x с ∃! hx : p x, q x hx.
LaTeX
$$$$ \\exists w\\, (p(w) \\land q(w, w)) \\to \\left( \\forall y\\,(p(y) \\to (\\\\forall h:(p(y)), q(y,h) \\\\to y = w)) \\Rightarrow \\exists! x\\, \\exists! h: p(x), q(x,h) \\right). $$$$
Lean4
theorem intro₂ {p : α → Sort*} [∀ x, Subsingleton (p x)] {q : ∀ (x : α) (_ : p x), Prop} (w : α) (hp : p w)
(hq : q w hp) (H : ∀ (y) (hy : p y), q y hy → y = w) : ∃! x, ∃! hx : p x, q x hx :=
by
simp only [existsUnique_iff_exists]
exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq
