Theorem: Classical.exitsUnique_extend (Arithmetization/Vorspiel/ExistsUnique.lean)

State before:
α : 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)
Tactic:
by_cases hx : p x <;> simp [hx]
State after:
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

State before:
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
Tactic:
exact h _ hx
State after:
no goals