α : Type u_1
β : Type ?u.469969
γ : Type ?u.469972
inst✝ : DecidableEq α
l l' : List α
a : α
hl : Nodup l
hl' : Nodup l'
h : toFinset l = toFinset l'
⊢ ↑l = ↑l'
α : Type u_1
β : Type ?u.469969
γ : Type ?u.469972
inst✝ : DecidableEq α
l l' : List α
a : α
hl : Nodup l
hl' : Nodup l'
h : toFinset l = toFinset l'
⊢ l ~ l'
rw [← Multiset.coe_eq_coe]
no goals
α : Type u_1
β : Type ?u.469969
γ : Type ?u.469972
inst✝ : DecidableEq α
l l' : List α
a : α
hl : Nodup l
hl' : Nodup l'
h : toFinset l = toFinset l'
⊢ ↑l = ↑l'
exact Multiset.Nodup.toFinset_inj hl hl' h