ι : Sort ?u.25704
α✝ : Sort ?u.25709
κ : ι → Sort ?u.25706
p✝ q✝ : α✝ → Prop
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
h : ∃! x, ∃ hx, q x hx
⊢ y₁ = y₂
ι : Sort ?u.25704
α✝ : Sort ?u.25709
κ : ι → Sort ?u.25706
p✝ q✝ : α✝ → Prop
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
h : ∃! x hx, q x hx
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
⊢ y₁ = y₂
simp only [exists_unique_iff_exists] at h
no goals
ι : Sort ?u.25704
α✝ : Sort ?u.25709
κ : ι → Sort ?u.25706
p✝ q✝ : α✝ → Prop
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
h : ∃! x, ∃ hx, q x hx
⊢ y₁ = y₂
exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩