case mk.mk
α : Type u_1
β : Type ?u.461724
γ : Type ?u.461727
inst✝ : DecidableEq α
l✝ l' : List α
a : α
val✝ : Multiset α
l : List α
hl : Multiset.Nodup (Quot.mk Setoid.r l)
a✝ : { val := Quot.mk Setoid.r l, nodup := hl } ∈ Set.univ
⊢ { val := Quot.mk Setoid.r l, nodup := hl } ∈ toFinset '' {l | Nodup l}
α : Type u_1
β : Type ?u.461724
γ : Type ?u.461727
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ Set.SurjOn toFinset {l | Nodup l} Set.univ
rintro ⟨⟨l⟩, hl⟩ _
no goals
case mk.mk
α : Type u_1
β : Type ?u.461724
γ : Type ?u.461727
inst✝ : DecidableEq α
l✝ l' : List α
a : α
val✝ : Multiset α
l : List α
hl : Multiset.Nodup (Quot.mk Setoid.r l)
a✝ : { val := Quot.mk Setoid.r l, nodup := hl } ∈ Set.univ
⊢ { val := Quot.mk Setoid.r l, nodup := hl } ∈ toFinset '' {l | Nodup l}
exact ⟨l, hl, (toFinset_eq hl).symm⟩