Theorem: Multiset.map_get (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
l : List α
⊢ map (List.get l) Finset.univ.val = ↑l
Tactic:
simp [Finset.univ, Fintype.elems]
State after:
no goals