Theorem: SciLean.Alternatives.pick_fst (SciLean/Util/Alternatives.lean)

State before:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ choose a b ap = a
Tactic:
unfold Alternatives.choose
State after:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ a = a

State before:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ a = a
Tactic:
rfl
State after:
no goals