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

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

State before:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ a = b
Tactic:
rw [ap.eq]
State after:
no goals