Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
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 α]`

## 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.27Multiset α: Type ?u.14α → Finset: Type ?u.29 → Type ?u.29Finset (List: Type ?u.30 → Type ?u.30List α: Type ?u.14α) := fun s: ?m.33s =>
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.33s (fun l: ?m.44l => l: ?m.44l.permutations: {α : Type ?u.46} → List α → List (List α)permutations.toFinset: {α : Type ?u.49} → [inst : DecidableEq α] → List α → Finset αtoFinset) fun l: ?m.159l l': ?m.162l' (h: l ~ l'h : l: ?m.159l ~ l': ?m.162l') => byGoals accomplished! 🐙
α: Type ?u.14inst✝: 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.14inst✝: 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.14inst✝: 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 ~ tmem_permutations, List.mem_toFinset: ∀ {α : Type ?u.240} [inst : DecidableEq α] {l : List α} {a : α}, a ∈ List.toFinset l ↔ a ∈ lList.mem_toFinset]α: Type ?u.14inst✝: DecidableEq αs: Multiset αl, l': List αh: l ~ l'sl: List αasl ~ l ↔ sl ~ l'
α: Type ?u.14inst✝: 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.528hs => hs: ?m.528hs.trans: ∀ {α : Type ?u.530} {l₁ l₂ l₃ : List α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃trans h: l ~ l'h, fun hs: ?m.547hs => hs: ?m.547hs.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.703List α: Type ?u.691α) : lists: {α : Type ?u.707} → [inst : DecidableEq α] → Multiset α → Finset (List α)lists (l: List αl : Multiset: Type ?u.711 → Type ?u.711Multiset α: 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 = arfl
#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 α) lmem_lists_iff (s: Multiset αs : Multiset: Type ?u.1046 → Type ?u.1046Multiset α: Type ?u.1034α) (l: List αl : List: Type ?u.1049 → Type ?u.1049List α: 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⟧ := byGoals accomplished! 🐙
α: Type u_1inst✝: 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 qQuotient.inductionOnα: Type u_1inst✝: DecidableEq αl, a✝: List αhl ∈ lists (Quotient.mk (isSetoid α) a✝) ↔ Quotient.mk (isSetoid α) a✝ = Quotient.mk (isSetoid α) l
α: Type u_1inst✝: 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_commGoals 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 α) lMultiset.mem_lists_iff

end Multiset

instance fintypeNodupList: [inst : Fintype α] → Fintype { l // Nodup l }fintypeNodupList [Fintype: Type ?u.5399 → Type ?u.5399Fintype α: Type ?u.5387α] : Fintype: Type ?u.5402 → Type ?u.5402Fintype { l: List αl : List: Type ?u.5406 → Type ?u.5406List α: Type ?u.5387α // l: List αl.Nodup: {α : Type ?u.5408} → List α → PropNodup } :=
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.5429Finset α: 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.5553s => s: ?m.5553s.val: {α : Type ?u.5555} → Finset α → Multiset αval.lists: {α : Type ?u.5557} → [inst : DecidableEq α] → Multiset α → Finset (List α)lists) fun l: ?m.5696l => byGoals accomplished! 🐙
α: Type ?u.5387inst✝¹: 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.5709Finset α: Type ?u.5387α, a: Finset αa.val: {α : Type ?u.5712} → Finset α → Multiset αval = ↑l: List αl) ↔ l: List αl.Nodup: {α : Type ?u.5824} → List α → PropNodup by α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List α(l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup lsimpaGoals accomplished! 🐙
α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List α(l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup lconstructorα: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmp(∃ a, a.val = ↑l) → Nodup lα: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmprNodup l → ∃ a, a.val = ↑l
α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List α(l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup l·α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmp(∃ a, a.val = ↑l) → Nodup l α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmp(∃ a, a.val = ↑l) → Nodup lα: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmprNodup l → ∃ a, a.val = ↑lrintro ⟨s, hs⟩: ?a⟨s: Finset αs⟨s, hs⟩: ?a, hs: s.val = ↑lhs⟨s, hs⟩: ?a⟩α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αs: Finset αhs: s.val = ↑lmp.introNodup l
α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmp(∃ a, a.val = ↑l) → Nodup lsimpa [← Multiset.coe_nodup: ∀ {α : Type ?u.8635} {l : List α}, Multiset.Nodup ↑l ↔ Nodup lMultiset.coe_nodup, ← hs: s.val = ↑lhs] using s: Finset αs.nodup: ∀ {α : Type ?u.8671} (self : Finset α), Multiset.Nodup self.valnodupGoals accomplished! 🐙
α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List α(l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup l·α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmprNodup l → ∃ a, a.val = ↑l α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmprNodup l → ∃ a, a.val = ↑lintro hl: ?bhlα: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αhl: Nodup lmpr∃ a, a.val = ↑l
α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmprNodup l → ∃ a, a.val = ↑lrefine' ⟨⟨↑l: List αl, hl: ?bhl⟩, _: ?m.8688 { val := ↑l, nodup := hl }_⟩α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αhl: Nodup lmpr{ val := ↑l, nodup := hl }.val = ↑l
α: Type ?u.5387inst✝¹: DecidableEq αinst✝: Fintype αl: List αmprNodup l → ∃ a, a.val = ↑lsimpGoals accomplished! 🐙
#align fintype_nodup_list fintypeNodupList: {α : Type u_1} → [inst : DecidableEq α] → [inst : Fintype α] → Fintype { l // Nodup l }fintypeNodupList
```