[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
l l' : List α
h : l ~ l'
⊢ (fun l => List.toFinset (permutations l)) l = (fun l => List.toFinset (permutations l)) l'
[PROOFSTEP]
ext sl
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
l l' : List α
h : l ~ l'
sl : List α
⊢ sl ∈ (fun l => List.toFinset (permutations l)) l ↔ sl ∈ (fun l => List.toFinset (permutations l)) l'
[PROOFSTEP]
simp only [mem_permutations, List.mem_toFinset]
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
l l' : List α
h : l ~ l'
sl : List α
⊢ sl ~ l ↔ sl ~ l'
[PROOFSTEP]
exact ⟨fun hs => hs.trans h, fun hs => hs.trans h.symm⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
l : List α
⊢ l ∈ lists s ↔ s = Quotient.mk (isSetoid α) l
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l a✝ : List α
⊢ l ∈ lists (Quotient.mk (isSetoid α) a✝) ↔ Quotient.mk (isSetoid α) a✝ = Quotient.mk (isSetoid α) l
[PROOFSTEP]
simpa using perm_comm
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
⊢ (l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup l
[PROOFSTEP]
suffices (∃ a : Finset α, a.val = ↑l) ↔ l.Nodup by simpa
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
this : (∃ a, a.val = ↑l) ↔ Nodup l
⊢ (l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup l
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
⊢ (∃ a, a.val = ↑l) ↔ Nodup l
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
⊢ (∃ a, a.val = ↑l) → Nodup l
[PROOFSTEP]
rintro ⟨s, hs⟩
[GOAL]
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
s : Finset α
hs : s.val = ↑l
⊢ Nodup l
[PROOFSTEP]
simpa [← Multiset.coe_nodup, ← hs] using s.nodup
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
⊢ Nodup l → ∃ a, a.val = ↑l
[PROOFSTEP]
intro hl
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
hl : Nodup l
⊢ ∃ a, a.val = ↑l
[PROOFSTEP]
refine' ⟨⟨↑l, hl⟩, _⟩
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
hl : Nodup l
⊢ { val := ↑l, nodup := hl }.val = ↑l
[PROOFSTEP]
simp
