Theorem: Classical.choose!_eq_iff (Logic/Vorspiel/ExistsUnique.lean)

State before:
α : Sort u_1
p : α → Prop
h : ∃! x, p x
x : α
⊢ x = choose! h → p x
Tactic:
rintro rfl
State after:
α : Sort u_1
p : α → Prop
h : ∃! x, p x
⊢ p (choose! h)

State before:
α : Sort u_1
p : α → Prop
h : ∃! x, p x
⊢ p (choose! h)
Tactic:
exact choose!_spec h
State after:
no goals