ι : Sort ?u.25148
α✝ : Sort ?u.25153
κ : ι → Sort ?u.25150
p✝ q✝ : α✝ → Prop
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (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, q x hx
ι : Sort ?u.25148
α✝ : Sort ?u.25153
κ : ι → Sort ?u.25150
p✝ q✝ : α✝ → Prop
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (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, q x hx
simp only [exists_unique_iff_exists]
no goals
ι : Sort ?u.25148
α✝ : Sort ?u.25153
κ : ι → Sort ?u.25150
p✝ q✝ : α✝ → Prop
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (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, q x hx
exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq