/-
Copyright (c) 2021 Yakov Pechersky. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yakov Pechersky

! This file was ported from Lean 3 source module data.fintype.list
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Finset.Powerset

/-!

# Fintype instance for nodup lists

The subtype of `{l : List α // l.nodup}` over a `[Fintype α]`
admits a `Fintype` instance.

## Implementation details
To construct the `Fintype` instance, a function lifting a `Multiset α`
to the `Finset (List α)` that can construct it is provided.
This function is applied to the `Finset.powerset` of `Finset.univ`.

In general, a `DecidableEq` instance is not necessary to define this function,
but a proof of `(List.permutations l).nodup` is required to avoid it,
which is a TODO.

-/


variable {α: Type ?u.14
α : Type _: Type (?u.2+1)
Type _} [DecidableEq: Sort ?u.694 → Sort (max1?u.694)
DecidableEq α: Type ?u.691
α]

open List

namespace Multiset

/-- The `Finset` of `l : List α` that, given `m : Multiset α`, have the property `⟦l⟧ = m`.
-/
def lists: Multiset α → Finset (List α)
lists : Multiset: Type ?u.27 → Type ?u.27
Multiset α: Type ?u.14
α → Finset: Type ?u.29 → Type ?u.29
Finset (List: Type ?u.30 → Type ?u.30
List α: Type ?u.14
α) := fun s: ?m.33
s =>
  Quotient.liftOn: {α : Sort ?u.36} → {β : Sort ?u.35} → {s : Setoid α} → Quotient s → (f : α → β) → (∀ (a b : α), a ≈ b → f a = f b) → β
Quotient.liftOn s: ?m.33
s (fun l: ?m.44
l => l: ?m.44
l.permutations: {α : Type ?u.46} → List α → List (List α)
permutations.toFinset: {α : Type ?u.49} → [inst : DecidableEq α] → List α → Finset α
toFinset) fun l: ?m.159
l l': ?m.162
l' (h: l ~ l'
h : l: ?m.159
l ~ l': ?m.162
l') => by
Goals accomplished! 🐙
    α: Type ?u.14

inst✝: DecidableEq α

s: Multiset α

l, l': List α

h: l ~ l'

(fun l => List.toFinset (permutations l)) l = (fun l => List.toFinset (permutations l)) l'ext sl: ?α
slα: Type ?u.14

inst✝: DecidableEq α

s: Multiset α

l, l': List α

h: l ~ l'

sl: List α

asl ∈ (fun l => List.toFinset (permutations l)) l ↔ sl ∈ (fun l => List.toFinset (permutations l)) l'
    α: Type ?u.14

inst✝: DecidableEq α

s: Multiset α

l, l': List α

h: l ~ l'

(fun l => List.toFinset (permutations l)) l = (fun l => List.toFinset (permutations l)) l'simp only [mem_permutations: ∀ {α : Type ?u.219} {s t : List α}, s ∈ permutations t ↔ s ~ t
mem_permutations, List.mem_toFinset: ∀ {α : Type ?u.240} [inst : DecidableEq α] {l : List α} {a : α}, a ∈ List.toFinset l ↔ a ∈ l
List.mem_toFinset]α: Type ?u.14

inst✝: DecidableEq α

s: Multiset α

l, l': List α

h: l ~ l'

sl: List α

asl ~ l ↔ sl ~ l'
    α: Type ?u.14

inst✝: DecidableEq α

s: Multiset α

l, l': List α

h: l ~ l'

(fun l => List.toFinset (permutations l)) l = (fun l => List.toFinset (permutations l)) l'exact ⟨fun hs: ?m.528
hs => hs: ?m.528
hs.trans: ∀ {α : Type ?u.530} {l₁ l₂ l₃ : List α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
trans h: l ~ l'
h, fun hs: ?m.547
hs => hs: ?m.547
hs.trans: ∀ {α : Type ?u.549} {l₁ l₂ l₃ : List α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
trans h: l ~ l'
h.symm: ∀ {α : Type ?u.560} {l₁ l₂ : List α}, l₁ ~ l₂ → l₂ ~ l₁
symm⟩
Goals accomplished! 🐙
#align multiset.lists Multiset.lists: {α : Type u_1} → [inst : DecidableEq α] → Multiset α → Finset (List α)
Multiset.lists

@[simp]
theorem lists_coe: ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), lists ↑l = List.toFinset (permutations l)
lists_coe (l: List α
l : List: Type ?u.703 → Type ?u.703
List α: Type ?u.691
α) : lists: {α : Type ?u.707} → [inst : DecidableEq α] → Multiset α → Finset (List α)
lists (l: List α
l : Multiset: Type ?u.711 → Type ?u.711
Multiset α: Type ?u.691
α) = l: List α
l.permutations: {α : Type ?u.857} → List α → List (List α)
permutations.toFinset: {α : Type ?u.859} → [inst : DecidableEq α] → List α → Finset α
toFinset :=
  rfl: ∀ {α : Sort ?u.961} {a : α}, a = a
rfl
#align multiset.lists_coe Multiset.lists_coe: ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), lists ↑l = List.toFinset (permutations l)
Multiset.lists_coe

@[simp]
theorem mem_lists_iff: ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (l : List α), l ∈ lists s ↔ s = Quotient.mk (isSetoid α) l
mem_lists_iff (s: Multiset α
s : Multiset: Type ?u.1046 → Type ?u.1046
Multiset α: Type ?u.1034
α) (l: List α
l : List: Type ?u.1049 → Type ?u.1049
List α: Type ?u.1034
α) : l: List α
l ∈ lists: {α : Type ?u.1058} → [inst : DecidableEq α] → Multiset α → Finset (List α)
lists s: Multiset α
s ↔ s: Multiset α
s = ⟦l: List α
l⟧ := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

s: Multiset α

l: List α

l ∈ lists s ↔ s = Quotient.mk (isSetoid α) linduction s: Multiset α
s using Quotient.inductionOn: ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s),
  (∀ (a : α), motive (Quotient.mk s a)) → motive q
Quotient.inductionOnα: Type u_1

inst✝: DecidableEq α

l, a✝: List α

hl ∈ lists (Quotient.mk (isSetoid α) a✝) ↔ Quotient.mk (isSetoid α) a✝ = Quotient.mk (isSetoid α) l
  α: Type u_1

inst✝: DecidableEq α

s: Multiset α

l: List α

l ∈ lists s ↔ s = Quotient.mk (isSetoid α) lsimpa using perm_comm: ∀ {α : Type ?u.5109} {l₁ l₂ : List α}, l₁ ~ l₂ ↔ l₂ ~ l₁
perm_comm
Goals accomplished! 🐙
#align multiset.mem_lists_iff Multiset.mem_lists_iff: ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (l : List α), l ∈ lists s ↔ s = Quotient.mk (isSetoid α) l
Multiset.mem_lists_iff

end Multiset

instance fintypeNodupList: [inst : Fintype α] → Fintype { l // Nodup l }
fintypeNodupList [Fintype: Type ?u.5399 → Type ?u.5399
Fintype α: Type ?u.5387
α] : Fintype: Type ?u.5402 → Type ?u.5402
Fintype { l: List α
l : List: Type ?u.5406 → Type ?u.5406
List α: Type ?u.5387
α // l: List α
l.Nodup: {α : Type ?u.5408} → List α → Prop
Nodup } :=
  Fintype.subtype: {α : Type ?u.5418} → {p : α → Prop} → (s : Finset α) → (∀ (x : α), x ∈ s ↔ p x) → Fintype { x // p x }
Fintype.subtype ((Finset.univ: {α : Type ?u.5430} → [inst : Fintype α] → Finset α
Finset.univ : Finset: Type ?u.5429 → Type ?u.5429
Finset α: Type ?u.5387
α).powerset: {α : Type ?u.5461} → Finset α → Finset (Finset α)
powerset.biUnion: {α : Type ?u.5464} → {β : Type ?u.5463} → [inst : DecidableEq β] → Finset α → (α → Finset β) → Finset β
biUnion fun s: ?m.5553
s => s: ?m.5553
s.val: {α : Type ?u.5555} → Finset α → Multiset α
val.lists: {α : Type ?u.5557} → [inst : DecidableEq α] → Multiset α → Finset (List α)
lists) fun l: ?m.5696
l => by
Goals accomplished! 🐙
    α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

(l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup lsuffices (∃ a: Finset α
a : Finset: Type ?u.5709 → Type ?u.5709
Finset α: Type ?u.5387
α, a: Finset α
a.val: {α : Type ?u.5712} → Finset α → Multiset α
val = ↑l: List α
l) ↔ l: List α
l.Nodup: {α : Type ?u.5824} → List α → Prop
Nodup by α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

(l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup lsimpa
Goals accomplished! 🐙
    α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

(l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup lconstructorα: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mp(∃ a, a.val = ↑l) → Nodup l
α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mprNodup l → ∃ a, a.val = ↑l
    α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

(l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup l·α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mp(∃ a, a.val = ↑l) → Nodup l α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mp(∃ a, a.val = ↑l) → Nodup l
α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mprNodup l → ∃ a, a.val = ↑lrintro ⟨s, hs⟩: ?a
⟨s: Finset α
s⟨s, hs⟩: ?a
, hs: s.val = ↑l
hs⟨s, hs⟩: ?a
⟩α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

s: Finset α

hs: s.val = ↑l

mp.introNodup l
      α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mp(∃ a, a.val = ↑l) → Nodup lsimpa [← Multiset.coe_nodup: ∀ {α : Type ?u.8635} {l : List α}, Multiset.Nodup ↑l ↔ Nodup l
Multiset.coe_nodup, ← hs: s.val = ↑l
hs] using s: Finset α
s.nodup: ∀ {α : Type ?u.8671} (self : Finset α), Multiset.Nodup self.val
nodup
Goals accomplished! 🐙
    α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

(l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup l·α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mprNodup l → ∃ a, a.val = ↑l α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mprNodup l → ∃ a, a.val = ↑lintro hl: ?b
hlα: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

hl: Nodup l

mpr∃ a, a.val = ↑l
      α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mprNodup l → ∃ a, a.val = ↑lrefine' ⟨⟨↑l: List α
l, hl: ?b
hl⟩, _: ?m.8688 { val := ↑l, nodup := hl }
_⟩α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

hl: Nodup l

mpr{ val := ↑l, nodup := hl }.val = ↑l
      α: Type ?u.5387

inst✝¹: DecidableEq α

inst✝: Fintype α

l: List α

mprNodup l → ∃ a, a.val = ↑lsimp
Goals accomplished! 🐙
#align fintype_nodup_list fintypeNodupList: {α : Type u_1} → [inst : DecidableEq α] → [inst : Fintype α] → Fintype { l // Nodup l }
fintypeNodupList