English
If there exists a unique x with p x and a unique h for p x with q x h, then a certain b follows provided a pointwise uniqueness condition holds for all y.
Русский
Если существует уникальное сочетание x и h: p(x) и q(x,h), то при условии по локальной уникальности для всех y следует b.
LaTeX
$$$$ (\\\\exists! x, \\\\exists! h : p(x), q(x,h)) \\\\Rightarrow \\\\left(\\\\forall x (p(x)) \\\\to (\\\\forall y (p(y)) \\\\to y = x) \\\\to b\\\\right) \\\\to b. $$$$
Lean4
theorem elim₂ {p : α → Sort*} [∀ x, Subsingleton (p x)] {q : ∀ (x) (_ : p x), Prop} {b : Prop}
(h₂ : ∃! x, ∃! h : p x, q x h) (h₁ : ∀ (x) (h : p x), q x h → (∀ (y) (hy : p y), q y hy → y = x) → b) : b :=
by
simp only [existsUnique_iff_exists] at h₂
apply h₂.elim
exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩
