by_cases hx : p x <;> simp [hx]
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x : α
⊢ ∃! y, (p x → r x y) ∧ (¬p x → y = default)
case pos
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x : α
hx : p x
⊢ ∃! y, r x y