α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ (if h : Nonempty α then some (Classical.choice h) else none) = some a
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ choice α = some a
simp [choice]
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ some (Classical.choice (_ : Nonempty α)) = some a
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ (if h : Nonempty α then some (Classical.choice h) else none) = some a
rw [dif_pos (⟨a⟩ : Nonempty α)]
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ Classical.choice (_ : Nonempty α) = a
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ some (Classical.choice (_ : Nonempty α)) = some a
simp
no goals
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ Classical.choice (_ : Nonempty α) = a
apply Subsingleton.elim