case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
⊢ (x, i) ∈ Finset.map (coeEmbedding m) Finset.univ ↔ (x, i) ∈ toEnumFinset m
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Finset.map (coeEmbedding m) Finset.univ = toEnumFinset m
ext ⟨x, i⟩
no goals
case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
⊢ (x, i) ∈ Finset.map (coeEmbedding m) Finset.univ ↔ (x, i) ∈ toEnumFinset m
simp only [Fin.exists_iff, Finset.mem_map, Finset.mem_univ, Multiset.coeEmbedding_apply,
  Prod.mk.inj_iff, exists_true_left, Multiset.exists_coe, Multiset.coe_mk, Fin.val_mk,
  exists_prop, exists_eq_right_right, exists_eq_right, Multiset.mem_toEnumFinset, iff_self_iff,
  true_and_iff]