/-
Copyright (c) 2019 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon

! This file was ported from Lean 3 source module data.fin_enum
! 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.Control.Monad.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.List.ProdSigma

/-!
Type class for finitely enumerable types. The property is stronger
than `Fintype` in that it assigns each element a rank in a finite
enumeration.
-/


universe u v

open Finset

/- ./././Mathport/Syntax/Translate/Command.lean:379:30:
  infer kinds are unsupported in Lean 4: #[`Equiv] [] -/
/-- `FinEnum α` means that `α` is finite and can be enumerated in some order,
  i.e. `α` has an explicit bijection with `Fin n` for some n. -/
class FinEnum: {α : Sort u_1} → (card : ℕ) → α ≃ Fin card → [decEq : DecidableEq α] → FinEnum α
FinEnum (α: Sort ?u.2
α : Sort _: Type ?u.2
SortSort _: Type ?u.2
 _) where
  /-- `FinEnum.card` is the cardinality of the `FinEnum` -/
  card: (α : Sort u_1) → [self : FinEnum α] → ℕ
card : ℕ: Type
ℕ
  /-- `FinEnum.Equiv` states that type `α` is in bijection with `Fin card`,
    the size of the `FinEnum` -/
  Equiv: {α : Sort u_1} → [self : FinEnum α] → α ≃ Fin (FinEnum.card α)
Equiv : α: Sort ?u.2
α ≃ Fin: ℕ → Type
Fin card: ℕ
card
  [decEq: {α : Sort u_1} → [self : FinEnum α] → DecidableEq α
decEq : DecidableEq: Sort ?u.13 → Sort (max1?u.13)
DecidableEq α: Sort ?u.2
α]
#align fin_enum FinEnum: Sort u_1 → Sort (max1u_1)
FinEnum

attribute [instance 100] FinEnum.decEq: {α : Sort u_1} → [self : FinEnum α] → DecidableEq α
FinEnum.decEq

namespace FinEnum

variable {α: Type u
α : Type u: Type (u+1)
Type u} {β: α → Type v
β : α: Type u
α → Type v: Type (v+1)
Type v}

/-- transport a `FinEnum` instance across an equivalence -/
def ofEquiv: (α : Sort ?u.54) → {β : Sort ?u.58} → [inst : FinEnum α] → β ≃ α → FinEnum β
ofEquiv (α: Sort ?u.54
α) {β: ?m.51
β} [FinEnum: Sort ?u.54 → Sort (max1?u.54)
FinEnum α: ?m.48
α] (h: β ≃ α
h : β: ?m.51
β ≃ α: ?m.48
α) : FinEnum: Sort ?u.61 → Sort (max1?u.61)
FinEnum β: ?m.51
β
    where
  card := card: (α : Sort ?u.70) → [self : FinEnum α] → ℕ
card α: Sort ?u.54
α
  Equiv := h: β ≃ α
h.trans: {α : Sort ?u.76} → {β : Sort ?u.75} → {γ : Sort ?u.74} → α ≃ β → β ≃ γ → α ≃ γ
trans (Equiv: {α : Sort ?u.89} → [self : FinEnum α] → α ≃ Fin (card α)
Equiv)
  decEq := (h: β ≃ α
h.trans: {α : Sort ?u.101} → {β : Sort ?u.100} → {γ : Sort ?u.99} → α ≃ β → β ≃ γ → α ≃ γ
trans (Equiv: {α : Sort ?u.110} → [self : FinEnum α] → α ≃ Fin (card α)
Equiv)).decidableEq: {α : Sort ?u.118} → {β : Sort ?u.117} → α ≃ β → [inst : DecidableEq β] → DecidableEq α
decidableEq
#align fin_enum.of_equiv FinEnum.ofEquiv: (α : Sort u_1) → {β : Sort u_2} → [inst : FinEnum α] → β ≃ α → FinEnum β
FinEnum.ofEquiv

/-- create a `FinEnum` instance from an exhaustive list without duplicates -/
def ofNodupList: [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → List.Nodup xs → FinEnum α
ofNodupList [DecidableEq: Sort ?u.240 → Sort (max1?u.240)
DecidableEq α: Type u
α] (xs: List α
xs : List: Type ?u.249 → Type ?u.249
List α: Type u
α) (h: ∀ (x : α), x ∈ xs
h : ∀ x: α
x : α: Type u
α, x: α
x ∈ xs: List α
xs) (h': List.Nodup xs
h' : List.Nodup: {α : Type ?u.285} → List α → Prop
List.Nodup xs: List α
xs) : FinEnum: Sort ?u.290 → Sort (max1?u.290)
FinEnum α: Type u
α
    where
  card := xs: List α
xs.length: {α : Type ?u.302} → List α → ℕ
length
  Equiv :=
    ⟨fun x: ?m.319
x => ⟨xs: List α
xs.indexOf: {α : Type ?u.326} → [inst : BEq α] → α → List α → ℕ
indexOf x: ?m.319
x, by
Goals accomplished! 🐙 α: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h: ∀ (x : α), x ∈ xs

h': List.Nodup xs

x: α

List.indexOf x xs < List.length xsrw [α: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h: ∀ (x : α), x ∈ xs

h': List.Nodup xs

x: α

List.indexOf x xs < List.length xsList.indexOf_lt_length: ∀ {α : Type ?u.629} [inst : DecidableEq α] {a : α} {l : List α}, List.indexOf a l < List.length l ↔ a ∈ l
List.indexOf_lt_lengthα: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h: ∀ (x : α), x ∈ xs

h': List.Nodup xs

x: α

x ∈ xs]α: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h: ∀ (x : α), x ∈ xs

h': List.Nodup xs

x: α

x ∈ xs α: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h: ∀ (x : α), x ∈ xs

h': List.Nodup xs

x: α

List.indexOf x xs < List.length xs;α: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h: ∀ (x : α), x ∈ xs

h': List.Nodup xs

x: α

x ∈ xs α: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h: ∀ (x : α), x ∈ xs

h': List.Nodup xs

x: α

List.indexOf x xs < List.length xsapply h: ∀ (x : α), x ∈ xs
h
Goals accomplished! 🐙⟩, fun ⟨i: ℕ
i, h: i < List.length xs
h⟩ =>
      xs: List α
xs.nthLe: {α : Type ?u.410} → (l : List α) → (n : ℕ) → n < List.length l → α
nthLe _: ℕ
_ h: i < List.length xs
h, fun x: ?m.487
x => by
Goals accomplished! 🐙 α: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h: ∀ (x : α), x ∈ xs

h': List.Nodup xs

x: α

(fun x =>
      match x with
      | { val := i, isLt := h } => List.nthLe xs i h)
    ((fun x => { val := List.indexOf x xs, isLt := (_ : List.indexOf x xs < List.length xs) }) x) =   xsimp
Goals accomplished! 🐙, fun ⟨i: ℕ
i, h: i < List.length xs
h⟩ => by
Goals accomplished! 🐙
      α: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h✝: ∀ (x : α), x ∈ xs

h': List.Nodup xs

x✝: Fin (List.length xs)

i: ℕ

h: i < List.length xs

(fun x => { val := List.indexOf x xs, isLt := (_ : List.indexOf x xs < List.length xs) })
    ((fun x =>
        match x with
        | { val := i, isLt := h } => List.nthLe xs i h)
      { val := i, isLt := h }) =   { val := i, isLt := h }simp [*]
Goals accomplished! 🐙⟩
#align fin_enum.of_nodup_list FinEnum.ofNodupList: {α : Type u} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → List.Nodup xs → FinEnum α
FinEnum.ofNodupList

/-- create a `FinEnum` instance from an exhaustive list; duplicates are removed -/
def ofList: {α : Type u} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList [DecidableEq: Sort ?u.2715 → Sort (max1?u.2715)
DecidableEq α: Type u
α] (xs: List α
xs : List: Type ?u.2724 → Type ?u.2724
List α: Type u
α) (h: ∀ (x : α), x ∈ xs
h : ∀ x: α
x : α: Type u
α, x: α
x ∈ xs: List α
xs) : FinEnum: Sort ?u.2760 → Sort (max1?u.2760)
FinEnum α: Type u
α :=
  ofNodupList: {α : Type ?u.2768} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → List.Nodup xs → FinEnum α
ofNodupList xs: List α
xs.dedup: {α : Type ?u.2850} → [inst : DecidableEq α] → List α → List α
dedup (by
Goals accomplished! 🐙 α: Type u

β: α → Type v

inst✝: DecidableEq α

xs: List α

h: ∀ (x : α), x ∈ xs

∀ (x : α), x ∈ List.dedup xssimp [*]
Goals accomplished! 🐙) (List.nodup_dedup: ∀ {α : Type ?u.2886} [inst : DecidableEq α] (l : List α), List.Nodup (List.dedup l)
List.nodup_dedup _: List ?m.2887
_)
#align fin_enum.of_list FinEnum.ofList: {α : Type u} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
FinEnum.ofList

/-- create an exhaustive list of the values of a given type -/
def toList: (α : Type ?u.5238) → [inst : FinEnum α] → List α
toList (α: ?m.5232
α) [FinEnum: Sort ?u.5235 → Sort (max1?u.5235)
FinEnum α: ?m.5232
α] : List: Type ?u.5238 → Type ?u.5238
List α: ?m.5232
α :=
  (List.finRange: (n : ℕ) → List (Fin n)
List.finRange (card: (α : Sort ?u.5242) → [self : FinEnum α] → ℕ
card α: Type ?u.5238
α)).map: {α : Type ?u.5247} → {β : Type ?u.5246} → (α → β) → List α → List β
map (Equiv: {α : Sort ?u.5255} → [self : FinEnum α] → α ≃ Fin (card α)
Equiv).symm: {α : Sort ?u.5261} → {β : Sort ?u.5260} → α ≃ β → β ≃ α
symm
#align fin_enum.to_list FinEnum.toList: (α : Type u_1) → [inst : FinEnum α] → List α
FinEnum.toList

open Function

@[simp]
theorem mem_toList: ∀ {α : Type u} [inst : FinEnum α] (x : α), x ∈ toList α
mem_toList [FinEnum: Sort ?u.5447 → Sort (max1?u.5447)
FinEnum α: Type u
α] (x: α
x : α: Type u
α) : x: α
x ∈ toList: (α : Type ?u.5469) → [inst : FinEnum α] → List α
toList α: Type u
α := by
Goals accomplished! 🐙
  α: Type u

β: α → Type v

inst✝: FinEnum α

x: α

x ∈ toList αsimp [toList: (α : Type ?u.5491) → [inst : FinEnum α] → List α
toList]α: Type u

β: α → Type v

inst✝: FinEnum α

x: α

∃ a, ↑Equiv.symm a = x α: Type u

β: α → Type v

inst✝: FinEnum α

x: α

x ∈ toList α;α: Type u

β: α → Type v

inst✝: FinEnum α

x: α

∃ a, ↑Equiv.symm a = x α: Type u

β: α → Type v

inst✝: FinEnum α

x: α

x ∈ toList αexists Equiv: {α : Sort ?u.8962} → [self : FinEnum α] → α ≃ Fin (card α)
Equiv x: α
xα: Type u

β: α → Type v

inst✝: FinEnum α

x: α

↑Equiv.symm (↑Equiv x) = x α: Type u

β: α → Type v

inst✝: FinEnum α

x: α

x ∈ toList α;α: Type u

β: α → Type v

inst✝: FinEnum α

x: α

↑Equiv.symm (↑Equiv x) = x α: Type u

β: α → Type v

inst✝: FinEnum α

x: α

x ∈ toList αsimp
Goals accomplished! 🐙
#align fin_enum.mem_to_list FinEnum.mem_toList: ∀ {α : Type u} [inst : FinEnum α] (x : α), x ∈ toList α
FinEnum.mem_toList

@[simp]
theorem nodup_toList: ∀ [inst : FinEnum α], List.Nodup (toList α)
nodup_toList [FinEnum: Sort ?u.9188 → Sort (max1?u.9188)
FinEnum α: Type u
α] : List.Nodup: {α : Type ?u.9191} → List α → Prop
List.Nodup (toList: (α : Type ?u.9193) → [inst : FinEnum α] → List α
toList α: Type u
α) := by
Goals accomplished! 🐙
  α: Type u

β: α → Type v

inst✝: FinEnum α

List.Nodup (toList α)simp [toList: (α : Type ?u.9205) → [inst : FinEnum α] → List α
toList]α: Type u

β: α → Type v

inst✝: FinEnum α

List.Nodup (List.map (↑Equiv.symm) (List.finRange (card α))) α: Type u

β: α → Type v

inst✝: FinEnum α

List.Nodup (toList α);α: Type u

β: α → Type v

inst✝: FinEnum α

List.Nodup (List.map (↑Equiv.symm) (List.finRange (card α))) α: Type u

β: α → Type v

inst✝: FinEnum α

List.Nodup (toList α)apply List.Nodup.map: ∀ {α : Type ?u.9339} {β : Type ?u.9338} {l : List α} {f : α → β}, Injective f → List.Nodup l → List.Nodup (List.map f l)
List.Nodup.mapα: Type u

β: α → Type v

inst✝: FinEnum α

hfInjective ↑Equiv.symm
α: Type u

β: α → Type v

inst✝: FinEnum α

aList.Nodup (List.finRange (card α)) <;> [α: Type u

β: α → Type v

inst✝: FinEnum α

List.Nodup (List.map (↑Equiv.symm) (List.finRange (card α)))apply Equiv.injective: ∀ {α : Sort ?u.9362} {β : Sort ?u.9361} (e : α ≃ β), Injective ↑e
Equiv.injective
Goals accomplished! 🐙; α: Type u

β: α → Type v

inst✝: FinEnum α

List.Nodup (List.map (↑Equiv.symm) (List.finRange (card α)))apply List.nodup_finRange: ∀ (n : ℕ), List.Nodup (List.finRange n)
List.nodup_finRange
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align fin_enum.nodup_to_list FinEnum.nodup_toList: ∀ {α : Type u} [inst : FinEnum α], List.Nodup (toList α)
FinEnum.nodup_toList

/-- create a `FinEnum` instance using a surjection -/
def ofSurjective: {β : Sort ?u.9419} → (f : β → α) → [inst : DecidableEq α] → [inst : FinEnum β] → Surjective f → FinEnum α
ofSurjective {β: ?m.9416
β} (f: β → α
f : β: ?m.9416
β → α: Type u
α) [DecidableEq: Sort ?u.9423 → Sort (max1?u.9423)
DecidableEq α: Type u
α] [FinEnum: Sort ?u.9432 → Sort (max1?u.9432)
FinEnum β: ?m.9416
β] (h: Surjective f
h : Surjective: {α : Sort ?u.9436} → {β : Sort ?u.9435} → (α → β) → Prop
Surjective f: β → α
f) : FinEnum: Sort ?u.9445 → Sort (max1?u.9445)
FinEnum α: Type u
α :=
  ofList: {α : Type ?u.9455} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList ((toList: (α : Type ?u.9537) → [inst : FinEnum α] → List α
toList β: Sort ?u.9419
β).map: {α : Type ?u.9543} → {β : Type ?u.9542} → (α → β) → List α → List β
map f: β → α
f) (by
Goals accomplished! 🐙 α: Type u

β✝: α → Type v

β: Type ?u.9537

f: β → α

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Surjective f

∀ (x : α), x ∈ List.map f (toList β)introα: Type u

β✝: α → Type v

β: Type ?u.9537

f: β → α

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Surjective f

x✝: α

x✝ ∈ List.map f (toList β) α: Type u

β✝: α → Type v

β: Type ?u.9537

f: β → α

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Surjective f

∀ (x : α), x ∈ List.map f (toList β);α: Type u

β✝: α → Type v

β: Type ?u.9537

f: β → α

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Surjective f

x✝: α

x✝ ∈ List.map f (toList β) α: Type u

β✝: α → Type v

β: Type ?u.9537

f: β → α

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Surjective f

∀ (x : α), x ∈ List.map f (toList β)simpα: Type u

β✝: α → Type v

β: Type ?u.9537

f: β → α

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Surjective f

x✝: α

∃ a, f a = x✝ α: Type u

β✝: α → Type v

β: Type ?u.9537

f: β → α

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Surjective f

∀ (x : α), x ∈ List.map f (toList β);α: Type u

β✝: α → Type v

β: Type ?u.9537

f: β → α

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Surjective f

x✝: α

∃ a, f a = x✝ α: Type u

β✝: α → Type v

β: Type ?u.9537

f: β → α

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Surjective f

∀ (x : α), x ∈ List.map f (toList β)exact h: Surjective f
h _: α
_
Goals accomplished! 🐙)
#align fin_enum.of_surjective FinEnum.ofSurjective: {α : Type u} → {β : Type u_1} → (f : β → α) → [inst : DecidableEq α] → [inst : FinEnum β] → Surjective f → FinEnum α
FinEnum.ofSurjective

/-- create a `FinEnum` instance using an injection -/
noncomputable def ofInjective: {α : Sort ?u.13146} →
  {β : Sort ?u.13147} → (f : α → β) → [inst : DecidableEq α] → [inst : FinEnum β] → Injective f → FinEnum α
ofInjective {α: ?m.13140
α β: ?m.13143
β} (f: α → β
f : α: ?m.13140
α → β: ?m.13143
β) [DecidableEq: Sort ?u.13150 → Sort (max1?u.13150)
DecidableEq α: ?m.13140
α] [FinEnum: Sort ?u.13159 → Sort (max1?u.13159)
FinEnum β: ?m.13143
β] (h: Injective f
h : Injective: {α : Sort ?u.13163} → {β : Sort ?u.13162} → (α → β) → Prop
Injective f: α → β
f) :
    FinEnum: Sort ?u.13171 → Sort (max1?u.13171)
FinEnum α: ?m.13140
α :=
  ofList: {α : Type ?u.13181} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList ((toList: (α : Type ?u.13263) → [inst : FinEnum α] → List α
toList β: Sort ?u.13147
β).filterMap: {α : Type ?u.13269} → {β : Type ?u.13268} → (α → Option β) → List α → List β
filterMap (partialInv: {α : Type ?u.13278} → {β : Sort ?u.13277} → (α → β) → β → Option α
partialInv f: α → β
f))
    (by
Goals accomplished! 🐙
      α✝: Type u

β✝: α✝ → Type v

α: Type ?u.13181

β: Type ?u.13263

f: α → β

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Injective f

∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)intro x: α
xα✝: Type u

β✝: α✝ → Type v

α: Type ?u.13181

β: Type ?u.13263

f: α → β

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Injective f

x: α

x ∈ List.filterMap (partialInv f) (toList β)
      α✝: Type u

β✝: α✝ → Type v

α: Type ?u.13181

β: Type ?u.13263

f: α → β

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Injective f

∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)simp only [mem_toList: ∀ {α : Type ?u.13343} [inst : FinEnum α] (x : α), x ∈ toList α
mem_toList, true_and_iff: ∀ (p : Prop), True ∧ p ↔ p
true_and_iff, List.mem_filterMap: ∀ {α : Type ?u.13371} {β : Type ?u.13372} (f : α → Option β) (l : List α) {b : β},
  b ∈ List.filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b
List.mem_filterMap]α✝: Type u

β✝: α✝ → Type v

α: Type ?u.13181

β: Type ?u.13263

f: α → β

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Injective f

x: α

∃ a, partialInv f a = some x
      α✝: Type u

β✝: α✝ → Type v

α: Type ?u.13181

β: Type ?u.13263

f: α → β

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Injective f

∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)use f: α → β
f x: α
xα✝: Type u

β✝: α✝ → Type v

α: Type ?u.13181

β: Type ?u.13263

f: α → β

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Injective f

x: α

partialInv f (f x) = some x
      α✝: Type u

β✝: α✝ → Type v

α: Type ?u.13181

β: Type ?u.13263

f: α → β

inst✝¹: DecidableEq α

inst✝: FinEnum β

h: Injective f

∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)simp only [h: Injective f
h, Function.partialInv_left: ∀ {α : Type ?u.13632} {β : Sort ?u.13633} {f : α → β}, Injective f → ∀ (x : α), partialInv f (f x) = some x
Function.partialInv_left]
Goals accomplished! 🐙)
#align fin_enum.of_injective FinEnum.ofInjective: {α : Type u_1} → {β : Type u_2} → (f : α → β) → [inst : DecidableEq α] → [inst : FinEnum β] → Injective f → FinEnum α
FinEnum.ofInjective

instance pempty: FinEnum PEmpty
pempty : FinEnum: Sort ?u.13742 → Sort (max1?u.13742)
FinEnum PEmpty: Sort ?u.13743
PEmpty :=
  ofList: {α : Type ?u.13745} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList []: List ?m.13828
[] fun x: ?m.13831
x => PEmpty.elim: ∀ {C : Sort ?u.13834}, PEmpty → C
PEmpty.elim x: ?m.13831
x
#align fin_enum.pempty FinEnum.pempty: FinEnum PEmpty
FinEnum.pempty

instance empty: FinEnum Empty
empty : FinEnum: Sort ?u.13937 → Sort (max1?u.13937)
FinEnum Empty: Type
Empty :=
  ofList: {α : Type ?u.13939} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList []: List ?m.14022
[] fun x: ?m.14025
x => Empty.elim: ∀ {C : Sort ?u.14027}, Empty → C
Empty.elim x: ?m.14025
x
#align fin_enum.empty FinEnum.empty: FinEnum Empty
FinEnum.empty

instance punit: FinEnum PUnit
punit : FinEnum: Sort ?u.14099 → Sort (max1?u.14099)
FinEnum PUnit: Sort ?u.14100
PUnit :=
  ofList: {α : Type ?u.14102} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList [PUnit.unit: PUnit
PUnit.unit] fun x: ?m.14191
x => by
Goals accomplished! 🐙 α: Type u

β: α → Type v

x: PUnit

x ∈ [PUnit.unit]cases x: PUnit
xα: Type u

β: α → Type v

unitPUnit.unit ∈ [PUnit.unit] α: Type u

β: α → Type v

x: PUnit

x ∈ [PUnit.unit];α: Type u

β: α → Type v

unitPUnit.unit ∈ [PUnit.unit] α: Type u

β: α → Type v

x: PUnit

x ∈ [PUnit.unit]simp
Goals accomplished! 🐙
#align fin_enum.punit FinEnum.punit: FinEnum PUnit
FinEnum.punit

/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
instance prod: {β : Type ?u.14376} → [inst : FinEnum α] → [inst : FinEnum β] → FinEnum (α × β)
prod {β: ?m.14366
β} [FinEnum: Sort ?u.14369 → Sort (max1?u.14369)
FinEnum α: Type u
α] [FinEnum: Sort ?u.14372 → Sort (max1?u.14372)
FinEnum β: ?m.14366
β] : FinEnum: Sort ?u.14375 → Sort (max1?u.14375)
FinEnum (α: Type u
α × β: ?m.14366
β) :=
  ofList: {α : Type ?u.14382} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList (toList: (α : Type ?u.14467) → [inst : FinEnum α] → List α
toList α: Type u
α ×ˢ toList: (α : Type ?u.14472) → [inst : FinEnum α] → List α
toList β: Type ?u.14376
β) fun x: ?m.14508
x => by
Goals accomplished! 🐙 α: Type u

β✝: α → Type v

β: Type ?u.14483

inst✝¹: FinEnum α

inst✝: FinEnum β

x: α × β

x ∈ toList α ×ˢ toList βcases x: α × β
xα: Type u

β✝: α → Type v

β: Type ?u.14483

inst✝¹: FinEnum α

inst✝: FinEnum β

fst✝: α

snd✝: β

mk(fst✝, snd✝) ∈ toList α ×ˢ toList β α: Type u

β✝: α → Type v

β: Type ?u.14483

inst✝¹: FinEnum α

inst✝: FinEnum β

x: α × β

x ∈ toList α ×ˢ toList β;α: Type u

β✝: α → Type v

β: Type ?u.14483

inst✝¹: FinEnum α

inst✝: FinEnum β

fst✝: α

snd✝: β

mk(fst✝, snd✝) ∈ toList α ×ˢ toList β α: Type u

β✝: α → Type v

β: Type ?u.14483

inst✝¹: FinEnum α

inst✝: FinEnum β

x: α × β

x ∈ toList α ×ˢ toList βsimp
Goals accomplished! 🐙
#align fin_enum.prod FinEnum.prod: {α : Type u} → {β : Type u_1} → [inst : FinEnum α] → [inst : FinEnum β] → FinEnum (α × β)
FinEnum.prod

instance sum: {β : Type ?u.17715} → [inst : FinEnum α] → [inst : FinEnum β] → FinEnum (α ⊕ β)
sum {β: Type ?u.17715
β} [FinEnum: Sort ?u.17708 → Sort (max1?u.17708)
FinEnum α: Type u
α] [FinEnum: Sort ?u.17711 → Sort (max1?u.17711)
FinEnum β: ?m.17705
β] : FinEnum: Sort ?u.17714 → Sort (max1?u.17714)
FinEnum (Sum: Type ?u.17716 → Type ?u.17715 → Type (max?u.17716?u.17715)
Sum α: Type u
α β: ?m.17705
β) :=
  ofList: {α : Type ?u.17721} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList ((toList: (α : Type ?u.17806) → [inst : FinEnum α] → List α
toList α: Type u
α).map: {α : Type ?u.17812} → {β : Type ?u.17811} → (α → β) → List α → List β
map Sum.inl: {α : Type ?u.17820} → {β : Type ?u.17819} → α → α ⊕ β
Sum.inl ++ (toList: (α : Type ?u.17827) → [inst : FinEnum α] → List α
toList β: Type ?u.17715
β).map: {α : Type ?u.17832} → {β : Type ?u.17831} → (α → β) → List α → List β
map Sum.inr: {α : Type ?u.17840} → {β : Type ?u.17839} → β → α ⊕ β
Sum.inr) fun x: ?m.17896
x => by
Goals accomplished! 🐙 α: Type u

β✝: α → Type v

β: Type ?u.17715

inst✝¹: FinEnum α

inst✝: FinEnum β

x: α ⊕ β

x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)cases x: α ⊕ β
xα: Type u

β✝: α → Type v

β: Type ?u.17715

inst✝¹: FinEnum α

inst✝: FinEnum β

val✝: α

inlSum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
α: Type u

β✝: α → Type v

β: Type ?u.17715

inst✝¹: FinEnum α

inst✝: FinEnum β

val✝: β

inrSum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β) α: Type u

β✝: α → Type v

β: Type ?u.17715

inst✝¹: FinEnum α

inst✝: FinEnum β

x: α ⊕ β

x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)<;>α: Type u

β✝: α → Type v

β: Type ?u.17715

inst✝¹: FinEnum α

inst✝: FinEnum β

val✝: α

inlSum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
α: Type u

β✝: α → Type v

β: Type ?u.17715

inst✝¹: FinEnum α

inst✝: FinEnum β

val✝: β

inrSum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β) α: Type u

β✝: α → Type v

β: Type ?u.17715

inst✝¹: FinEnum α

inst✝: FinEnum β

x: α ⊕ β

x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)simp
Goals accomplished! 🐙
#align fin_enum.sum FinEnum.sum: {α : Type u} → {β : Type u_1} → [inst : FinEnum α] → [inst : FinEnum β] → FinEnum (α ⊕ β)
FinEnum.sum

instance fin: {n : ℕ} → FinEnum (Fin n)
fin {n: ℕ
n} : FinEnum: Sort ?u.29329 → Sort (max1?u.29329)
FinEnum (Fin: ℕ → Type
Fin n: ?m.29326
n) :=
  ofList: {α : Type ?u.29332} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList (List.finRange: (n : ℕ) → List (Fin n)
List.finRange _: ℕ
_) (by
Goals accomplished! 🐙 α: Type u

β: α → Type v

n: ℕ

∀ (x : Fin n), x ∈ List.finRange nsimp
Goals accomplished! 🐙)
#align fin_enum.fin FinEnum.fin: {n : ℕ} → FinEnum (Fin n)
FinEnum.fin

instance Quotient.enum: [inst : FinEnum α] → (s : Setoid α) → [inst : DecidableRel fun x x_1 => x ≈ x_1] → FinEnum (Quotient s)
Quotient.enum [FinEnum: Sort ?u.32009 → Sort (max1?u.32009)
FinEnum α: Type u
α] (s: Setoid α
s : Setoid: Sort ?u.32012 → Sort (max1?u.32012)
Setoid α: Type u
α) [DecidableRel: {α : Sort ?u.32015} → (α → α → Prop) → Sort (max1?u.32015)
DecidableRel ((· ≈ ·): α → α → Sort ?u.32028
(· ≈ ·) : α: Type u
α → α: Type u
α → Prop: Type
Prop)] :
    FinEnum: Sort ?u.32058 → Sort (max1?u.32058)
FinEnum (Quotient: {α : Sort ?u.32059} → Setoid α → Sort ?u.32059
Quotient s: Setoid α
s) :=
  FinEnum.ofSurjective: {α : Type ?u.32069} →
  {β : Type ?u.32068} → (f : β → α) → [inst : DecidableEq α] → [inst : FinEnum β] → Surjective f → FinEnum α
FinEnum.ofSurjective Quotient.mk'': {α : Sort ?u.32073} → {s₁ : Setoid α} → α → Quotient s₁
Quotient.mk'' fun x: ?m.32084
x => Quotient.inductionOn: ∀ {α : Sort ?u.32086} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s),
  (∀ (a : α), motive (Quotient.mk s a)) → motive q
Quotient.inductionOn x: ?m.32084
x fun x: ?m.32233
x => ⟨x: ?m.32233
x, rfl: ∀ {α : Sort ?u.32244} {a : α}, a = a
rfl⟩
#align fin_enum.quotient.enum FinEnum.Quotient.enum: {α : Type u} → [inst : FinEnum α] → (s : Setoid α) → [inst : DecidableRel fun x x_1 => x ≈ x_1] → FinEnum (Quotient s)
FinEnum.Quotient.enum

/-- enumerate all finite sets of a given type -/
def Finset.enum: [inst : DecidableEq α] → List α → List (Finset α)
Finset.enum [DecidableEq: Sort ?u.32394 → Sort (max1?u.32394)
DecidableEq α: Type u
α] : List: Type ?u.32404 → Type ?u.32404
List α: Type u
α → List: Type ?u.32406 → Type ?u.32406
List (Finset: Type ?u.32407 → Type ?u.32407
Finset α: Type u
α)
  | [] => [∅: ?m.32428
∅]
  | x: α
x :: xs: List α
xs => do
    let r: ?m.32585
r ← Finset.enum: [inst : DecidableEq α] → List α → List (Finset α)
Finset.enum xs: List α
xs
    [r: ?m.32585
r, {x: α
x} ∪ r: ?m.32585
r]
#align fin_enum.finset.enum FinEnum.Finset.enum: {α : Type u} → [inst : DecidableEq α] → List α → List (Finset α)
FinEnum.Finset.enum

@[simp]
theorem Finset.mem_enum: ∀ {α : Type u} [inst : DecidableEq α] (s : Finset α) (xs : List α), s ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs
Finset.mem_enum [DecidableEq: Sort ?u.33067 → Sort (max1?u.33067)
DecidableEq α: Type u
α] (s: Finset α
s : Finset: Type ?u.33076 → Type ?u.33076
Finset α: Type u
α) (xs: List α
xs : List: Type ?u.33079 → Type ?u.33079
List α: Type u
α) :
    s: Finset α
s ∈ Finset.enum: {α : Type ?u.33088} → [inst : DecidableEq α] → List α → List (Finset α)
Finset.enum xs: List α
xs ↔ ∀ x: ?m.33219
x ∈ s: Finset α
s, x: ?m.33219
x ∈ xs: List α
xs := by
Goals accomplished! 🐙
  α: Type u

β: α → Type v

inst✝: DecidableEq α

s: Finset α

xs: List α

s ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xsinduction' xs: List α
xs with xs_hd: ?m.33300
xs_hd generalizing s: Finset α
sα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝, s: Finset α

nils ∈ enum [] ↔ ∀ (x : α), x ∈ s → x ∈ []
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

conss ∈ enum (xs_hd :: tail✝) ↔ ∀ (x : α), x ∈ s → x ∈ xs_hd :: tail✝ α: Type u

β: α → Type v

inst✝: DecidableEq α

s: Finset α

xs: List α

s ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs<;>α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝, s: Finset α

nils ∈ enum [] ↔ ∀ (x : α), x ∈ s → x ∈ []
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

conss ∈ enum (xs_hd :: tail✝) ↔ ∀ (x : α), x ∈ s → x ∈ xs_hd :: tail✝ α: Type u

β: α → Type v

inst✝: DecidableEq α

s: Finset α

xs: List α

s ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xssimp [*, Finset.enum: {α : Type ?u.35032} → [inst : DecidableEq α] → List α → List (Finset α)
Finset.enum]α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
  α: Type u

β: α → Type v

inst✝: DecidableEq α

s: Finset α

xs: List α

s ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝, s: Finset α

nils = ∅ ↔ ∀ (x : α), x ∈ s → False α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝, s: Finset α

nils = ∅ ↔ ∀ (x : α), x ∈ s → False
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝simp [Finset.eq_empty_iff_forall_not_mem: ∀ {α : Type ?u.51711} {s : Finset α}, s = ∅ ↔ ∀ (x : α), ¬x ∈ s
Finset.eq_empty_iff_forall_not_mem]
Goals accomplished! 🐙
  α: Type u

β: α → Type v

inst✝: DecidableEq α

s: Finset α

xs: List α

s ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝ α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝constructorα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mp(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
    α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mp(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝ α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mp(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)rintro ⟨a, h, h'⟩: (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
⟨a: Finset α
a⟨a, h, h'⟩: (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
, h: ∀ (x : α), x ∈ a → x ∈ tail✝
h⟨a, h, h'⟩: (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
, h': s = a ∨ s = {xs_hd} ∪ a
h'⟨a, h, h'⟩: (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
⟩ x: α
x hx: x ∈ s
hxα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

h': s = a ∨ s = {xs_hd} ∪ a

x: α

hx: x ∈ s

cons.mp.intro.introx = xs_hd ∨ x ∈ tail✝
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mp(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝cases' h': s = a ∨ s = {xs_hd} ∪ a
h' with _ h': ?m.52372
h' a bα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h✝: s = a

cons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h': s = {xs_hd} ∪ a

cons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mp(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h✝: s = a

cons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝ α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h✝: s = a

cons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h': s = {xs_hd} ∪ a

cons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝rightα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h✝: s = a

cons.mp.intro.intro.inl.hx ∈ tail✝
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h✝: s = a

cons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝apply h: ∀ (x : α), x ∈ a → x ∈ tail✝
hα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h✝: s = a

cons.mp.intro.intro.inl.h.ax ∈ a
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h✝: s = a

cons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝subst a: Finset α
aα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

x: α

hx: x ∈ s

h: ∀ (x : α), x ∈ s → x ∈ tail✝

cons.mp.intro.intro.inl.h.ax ∈ s
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h✝: s = a

cons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝exact hx: x ∈ s
hx
Goals accomplished! 🐙
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mp(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h': s = {xs_hd} ∪ a

cons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝ α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h': s = {xs_hd} ∪ a

cons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝simp only [h': ?m.52372
h', mem_union: ∀ {α : Type ?u.52458} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
mem_union, mem_singleton: ∀ {α : Type ?u.52491} {a b : α}, b ∈ {a} ↔ b = a
mem_singleton] at hx: x ∈ s
hx⊢α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

h': s = {xs_hd} ∪ a

hx: x = xs_hd ∨ x ∈ a

cons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h': s = {xs_hd} ∪ a

cons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝cases' hx: x = xs_hd ∨ x ∈ a
hx with hx: ?m.52712
hx hx': ?m.52713
hx'α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

h': s = {xs_hd} ∪ a

hx: x = xs_hd

cons.mp.intro.intro.inr.inlx = xs_hd ∨ x ∈ tail✝
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

h': s = {xs_hd} ∪ a

hx': x ∈ a

cons.mp.intro.intro.inr.inrx = xs_hd ∨ x ∈ tail✝
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h': s = {xs_hd} ∪ a

cons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

h': s = {xs_hd} ∪ a

hx: x = xs_hd

cons.mp.intro.intro.inr.inlx = xs_hd ∨ x ∈ tail✝ α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

h': s = {xs_hd} ∪ a

hx: x = xs_hd

cons.mp.intro.intro.inr.inlx = xs_hd ∨ x ∈ tail✝
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

h': s = {xs_hd} ∪ a

hx': x ∈ a

cons.mp.intro.intro.inr.inrx = xs_hd ∨ x ∈ tail✝exact Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl hx: ?m.52712
hx
Goals accomplished! 🐙
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

hx: x ∈ s

h': s = {xs_hd} ∪ a

cons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

h': s = {xs_hd} ∪ a

hx': x ∈ a

cons.mp.intro.intro.inr.inrx = xs_hd ∨ x ∈ tail✝ α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s, a: Finset α

h: ∀ (x : α), x ∈ a → x ∈ tail✝

x: α

h': s = {xs_hd} ∪ a

hx': x ∈ a

cons.mp.intro.intro.inr.inrx = xs_hd ∨ x ∈ tail✝exact Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr (h: ∀ (x : α), x ∈ a → x ∈ tail✝
h _: α
_ hx': ?m.52713
hx')
Goals accomplished! 🐙
    α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons(∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a) α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)intro h: ?b
hα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h: ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝

cons.mpr∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)exists s: Finset α
s \ ({xs_hd: ?m.33300
xs_hd} : Finset: Type ?u.52798 → Type ?u.52798
Finset α: Type u
α)α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h: ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝

cons.mpr(∀ (x : α), x ∈ s \ {xs_hd} → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)simp only [and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
and_imp, mem_sdiff: ∀ {α : Type ?u.52947} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s \ t ↔ a ∈ s ∧ ¬a ∈ t
mem_sdiff, mem_singleton: ∀ {α : Type ?u.52982} {a b : α}, b ∈ {a} ↔ b = a
mem_singleton]α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h: ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝

cons.mpr(∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)simp only [or_iff_not_imp_left: ∀ {a b : Prop}, a ∨ b ↔ ¬a → b
or_iff_not_imp_left] at h: ?b
hα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

cons.mpr(∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)exists h: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
hα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

cons.mprs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)by_cases h: ?m.53485
h : xs_hd: ?m.33300
xs_hd ∈ s: Finset α
sα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: xs_hd ∈ s

poss = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: xs_hd ∈ s

poss = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd} α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: xs_hd ∈ s

poss = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}have : {xs_hd: ?m.33300
xs_hd} ⊆ s: Finset α
sα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: xs_hd ∈ s

this{xs_hd} ⊆ s
α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: xs_hd ∈ s

this: {xs_hd} ⊆ s

poss = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: xs_hd ∈ s

poss = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}simp only [HasSubset.Subset: {α : Type ?u.53572} → [self : HasSubset α] → α → α → Prop
HasSubset.Subset, *, forall_eq: ∀ {α : Sort ?u.53574} {p : α → Prop} {a' : α}, (∀ (a : α), a = a' → p a) ↔ p a'
forall_eq, mem_singleton: ∀ {α : Type ?u.53589} {a b : α}, b ∈ {a} ↔ b = a
mem_singleton]α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: xs_hd ∈ s

this: {xs_hd} ⊆ s

poss = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: xs_hd ∈ s

poss = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}simp only [union_sdiff_of_subset: ∀ {α : Type ?u.53772} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → s ∪ t \ s = t
union_sdiff_of_subset this: {xs_hd} ⊆ s
this, or_true_iff: ∀ (p : Prop), p ∨ True ↔ True
or_true_iff, Finset.union_sdiff_of_subset: ∀ {α : Type ?u.53827} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → s ∪ t \ s = t
Finset.union_sdiff_of_subset,
          eq_self_iff_true: ∀ {α : Sort ?u.53850} (a : α), a = a ↔ True
eq_self_iff_true]
Goals accomplished! 🐙
      α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

cons.mpr(∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)·α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd} α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}leftα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

neg.hs = s \ {xs_hd}
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}symmα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

neg.hs \ {xs_hd} = s
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}simp only [sdiff_eq_self: ∀ {α : Type ?u.54080} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ \ s₂ = s₁ ↔ s₁ ∩ s₂ ⊆ ∅
sdiff_eq_self]α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

neg.hs ∩ {xs_hd} ⊆ ∅
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}intro a: α
aα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

a: α

neg.ha ∈ s ∩ {xs_hd} → a ∈ ∅
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}simp only [and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
and_imp, mem_inter: ∀ {α : Type ?u.54316} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finset α}, a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂
mem_inter, mem_singleton: ∀ {α : Type ?u.54349} {a b : α}, b ∈ {a} ↔ b = a
mem_singleton]α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

a: α

neg.ha ∈ s → a = xs_hd → a ∈ ∅
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}rintro h₀: a ∈ s
h₀ rfl: a = xs_hd
rflα: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

a: α

h₀: a ∈ s

h✝: ∀ (x : α), x ∈ s → ¬x = a → x ∈ tail✝

h: ¬a ∈ s

neg.ha ∈ ∅
        α: Type u

β: α → Type v

inst✝: DecidableEq α

s✝: Finset α

xs_hd: α

tail✝: List α

tail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝

s: Finset α

h✝: ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝

h: ¬xs_hd ∈ s

negs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}exact (h: ¬a ∈ s
h h₀: a ∈ s
h₀).elim: ∀ {C : Sort ?u.54583}, False → C
elim
Goals accomplished! 🐙
#align fin_enum.finset.mem_enum FinEnum.Finset.mem_enum: ∀ {α : Type u} [inst : DecidableEq α] (s : Finset α) (xs : List α), s ∈ Finset.enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs
FinEnum.Finset.mem_enum

instance Finset.finEnum: [inst : FinEnum α] → FinEnum (Finset α)
Finset.finEnum [FinEnum: Sort ?u.54806 → Sort (max1?u.54806)
FinEnum α: Type u
α] : FinEnum: Sort ?u.54809 → Sort (max1?u.54809)
FinEnum (Finset: Type ?u.54810 → Type ?u.54810
Finset α: Type u
α) :=
  ofList: {α : Type ?u.54813} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList (Finset.enum: {α : Type ?u.54895} → [inst : DecidableEq α] → List α → List (Finset α)
Finset.enum (toList: (α : Type ?u.54977) → [inst : FinEnum α] → List α
toList α: Type u
α)) (by
Goals accomplished! 🐙 α: Type u

β: α → Type v

inst✝: FinEnum α

∀ (x : Finset α), x ∈ enum (toList α)introα: Type u

β: α → Type v

inst✝: FinEnum α

x✝: Finset α

x✝ ∈ enum (toList α) α: Type u

β: α → Type v

inst✝: FinEnum α

∀ (x : Finset α), x ∈ enum (toList α);α: Type u

β: α → Type v

inst✝: FinEnum α

x✝: Finset α

x✝ ∈ enum (toList α) α: Type u

β: α → Type v

inst✝: FinEnum α

∀ (x : Finset α), x ∈ enum (toList α)simp
Goals accomplished! 🐙)
#align fin_enum.finset.fin_enum FinEnum.Finset.finEnum: {α : Type u} → [inst : FinEnum α] → FinEnum (Finset α)
FinEnum.Finset.finEnum

instance Subtype.finEnum: {α : Type u} → [inst : FinEnum α] → (p : α → Prop) → [inst : DecidablePred p] → FinEnum { x // p x }
Subtype.finEnum [FinEnum: Sort ?u.58275 → Sort (max1?u.58275)
FinEnum α: Type u
α] (p: α → Prop
p : α: Type u
α → Prop: Type
Prop) [DecidablePred: {α : Sort ?u.58282} → (α → Prop) → Sort (max1?u.58282)
DecidablePred p: α → Prop
p] : FinEnum: Sort ?u.58292 → Sort (max1?u.58292)
FinEnum { x: ?m.58296
x // p: α → Prop
p x: ?m.58296
x } :=
  ofList: {α : Type ?u.58306} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList ((toList: (α : Type ?u.58392) → [inst : FinEnum α] → List α
toList α: Type u
α).filterMap: {α : Type ?u.58396} → {β : Type ?u.58395} → (α → Option β) → List α → List β
filterMap fun x: ?m.58405
x => if h: ?m.58439
h : p: α → Prop
p x: ?m.58405
x then some: {α : Type ?u.58419} → α → Option α
some ⟨_: ?m.58427
_, h: ?m.58417
h⟩ else none: {α : Type ?u.58441} → Option α
none)
    (by
Goals accomplished! 🐙 α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

∀ (x : { x // p x }),
  x ∈ List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α)rintro ⟨x, h⟩: { x // p x }
⟨x: α
x⟨x, h⟩: { x // p x }
, h: p x
h⟨x, h⟩: { x // p x }
⟩α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

x: α

h: p x

mk{ val := x, property := h } ∈   List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α) α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

∀ (x : { x // p x }),
  x ∈ List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α);α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

x: α

h: p x

mk{ val := x, property := h } ∈   List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α) α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

∀ (x : { x // p x }),
  x ∈ List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α)simpα: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

x: α

h: p x

mk∃ a, (if h : p a then some { val := a, property := h } else none) = some { val := x, property := h } α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

∀ (x : { x // p x }),
  x ∈ List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α);α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

x: α

h: p x

mk∃ a, (if h : p a then some { val := a, property := h } else none) = some { val := x, property := h } α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

∀ (x : { x // p x }),
  x ∈ List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α)exists x: α
xα: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

x: α

h: p x

mk(if h : p x then some { val := x, property := h } else none) = some { val := x, property := h } α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

∀ (x : { x // p x }),
  x ∈ List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α);α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

x: α

h: p x

mk(if h : p x then some { val := x, property := h } else none) = some { val := x, property := h } α: Type u

β: α → Type v

inst✝¹: FinEnum α

p: α → Prop

inst✝: DecidablePred p

∀ (x : { x // p x }),
  x ∈ List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α)simp [*]
Goals accomplished! 🐙)
#align fin_enum.subtype.fin_enum FinEnum.Subtype.finEnum: {α : Type u} → [inst : FinEnum α] → (p : α → Prop) → [inst : DecidablePred p] → FinEnum { x // p x }
FinEnum.Subtype.finEnum

instance: {α : Type u} → (β : α → Type v) → [inst : FinEnum α] → [inst : (a : α) → FinEnum (β a)] → FinEnum (Sigma β)
instance (β: α → Type v
β : α: Type u
α → Type v: Type (v+1)
Type v) [FinEnum: Sort ?u.64034 → Sort (max1?u.64034)
FinEnum α: Type u
α] [∀ a: ?m.64038
a, FinEnum: Sort ?u.64041 → Sort (max1?u.64041)
FinEnum (β: α → Type v
β a: ?m.64038
a)] : FinEnum: Sort ?u.64045 → Sort (max1?u.64045)
FinEnum (Sigma: {α : Type ?u.64047} → (α → Type ?u.64046) → Type (max?u.64047?u.64046)
Sigma β: α → Type v
β) :=
  ofList: {α : Type ?u.64056} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList ((toList: (α : Type ?u.64138) → [inst : FinEnum α] → List α
toList α: Type u
α).bind: {α : Type ?u.64146} → {β : Type ?u.64145} → List α → (α → List β) → List β
bind fun a: ?m.64156
a => (toList: (α : Type ?u.64158) → [inst : FinEnum α] → List α
toList (β: α → Type v
β a: ?m.64156
a)).map: {α : Type ?u.64167} → {β : Type ?u.64166} → (α → β) → List α → List β
map <| Sigma.mk: {α : Type ?u.64175} → {β : α → Type ?u.64174} → (fst : α) → β fst → Sigma β
Sigma.mk a: ?m.64156
a)
    (by
Goals accomplished! 🐙 α: Type u

β✝, β: α → Type v

inst✝¹: FinEnum α

inst✝: (a : α) → FinEnum (β a)

∀ (x : Sigma β), x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a))intro x: Sigma β
xα: Type u

β✝, β: α → Type v

inst✝¹: FinEnum α

inst✝: (a : α) → FinEnum (β a)

x: Sigma β

x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a)) α: Type u

β✝, β: α → Type v

inst✝¹: FinEnum α

inst✝: (a : α) → FinEnum (β a)

∀ (x : Sigma β), x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a));α: Type u

β✝, β: α → Type v

inst✝¹: FinEnum α

inst✝: (a : α) → FinEnum (β a)

x: Sigma β

x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a)) α: Type u

β✝, β: α → Type v

inst✝¹: FinEnum α

inst✝: (a : α) → FinEnum (β a)

∀ (x : Sigma β), x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a))cases x: Sigma β
xα: Type u

β✝, β: α → Type v

inst✝¹: FinEnum α

inst✝: (a : α) → FinEnum (β a)

fst✝: α

snd✝: β fst✝

mk{ fst := fst✝, snd := snd✝ } ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a)) α: Type u

β✝, β: α → Type v

inst✝¹: FinEnum α

inst✝: (a : α) → FinEnum (β a)

∀ (x : Sigma β), x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a));α: Type u

β✝, β: α → Type v

inst✝¹: FinEnum α

inst✝: (a : α) → FinEnum (β a)

fst✝: α

snd✝: β fst✝

mk{ fst := fst✝, snd := snd✝ } ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a)) α: Type u

β✝, β: α → Type v

inst✝¹: FinEnum α

inst✝: (a : α) → FinEnum (β a)

∀ (x : Sigma β), x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a))simp
Goals accomplished! 🐙)

instance PSigma.finEnum: {α : Type u} → {β : α → Type v} → [inst : FinEnum α] → [inst : (a : α) → FinEnum (β a)] → FinEnum ((a : α) ×' β a)
PSigma.finEnum [FinEnum: Sort ?u.70850 → Sort (max1?u.70850)
FinEnum α: Type u
α] [∀ a: ?m.70854
a, FinEnum: Sort ?u.70857 → Sort (max1?u.70857)
FinEnum (β: α → Type v
β a: ?m.70854
a)] : FinEnum: Sort ?u.70861 → Sort (max1?u.70861)
FinEnum (Σ'a: ?m.70866
a, β: α → Type v
β a: ?m.70866
a) :=
  FinEnum.ofEquiv: (α : Sort ?u.70875) → {β : Sort ?u.70874} → [inst : FinEnum α] → β ≃ α → FinEnum β
FinEnum.ofEquiv _: Sort ?u.70875
_ (Equiv.psigmaEquivSigma: {α : Type ?u.70896} → (β : α → Type ?u.70895) → (i : α) ×' β i ≃ (i : α) × β i
Equiv.psigmaEquivSigma _: ?m.70897 → Type ?u.70895
_)
#align fin_enum.psigma.fin_enum FinEnum.PSigma.finEnum: {α : Type u} → {β : α → Type v} → [inst : FinEnum α] → [inst : (a : α) → FinEnum (β a)] → FinEnum ((a : α) ×' β a)
FinEnum.PSigma.finEnum

instance PSigma.finEnumPropLeft: {α : Prop} → {β : α → Type v} → [inst : (a : α) → FinEnum (β a)] → [inst : Decidable α] → FinEnum ((a : α) ×' β a)
PSigma.finEnumPropLeft {α: Prop
α : Prop: Type
Prop} {β: α → Type v
β : α: Prop
α → Type v: Type (v+1)
Type v} [∀ a: ?m.71042
a, FinEnum: Sort ?u.71045 → Sort (max1?u.71045)
FinEnum (β: α → Type v
β a: ?m.71042
a)] [Decidable: Prop → Type
Decidable α: Prop
α] :
    FinEnum: Sort ?u.71051 → Sort (max1?u.71051)
FinEnum (Σ'a: ?m.71056
a, β: α → Type v
β a: ?m.71056
a) :=
  if h: ?m.71753
h : α: Prop
α then ofList: {α : Type ?u.71075} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList ((toList: (α : Type ?u.71159) → [inst : FinEnum α] → List α
toList (β: α → Type v
β h: ?m.71073
h)).map: {α : Type ?u.71167} → {β : Type ?u.71166} → (α → β) → List α → List β
map <| PSigma.mk: {α : Sort ?u.71176} → {β : α → Sort ?u.71175} → (fst : α) → β fst → PSigma β
PSigma.mk h: ?m.71073
h) fun ⟨a: α
a, Ba: β a
Ba⟩ => by
Goals accomplished! 🐙 α✝: Type u

β✝: α✝ → Type v

α: Prop

β: α → Type v

inst✝¹: (a : α) → FinEnum (β a)

inst✝: Decidable α

h: α

x✝: (a : α) ×' β a

a: α

Ba: β a

{ fst := a, snd := Ba } ∈ List.map (PSigma.mk h) (toList (β h))simp
Goals accomplished! 🐙
  else ofList: {α : Type ?u.71755} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList []: List ?m.71838
[] fun ⟨a: α
a, Ba: β a
Ba⟩ => (h: ?m.71753
h a: α
a).elim: ∀ {C : Sort ?u.71873}, False → C
elim
#align fin_enum.psigma.fin_enum_prop_left FinEnum.PSigma.finEnumPropLeft: {α : Prop} → {β : α → Type v} → [inst : (a : α) → FinEnum (β a)] → [inst : Decidable α] → FinEnum ((a : α) ×' β a)
FinEnum.PSigma.finEnumPropLeft

instance PSigma.finEnumPropRight: {α : Type u} → {β : α → Prop} → [inst : FinEnum α] → [inst : (a : α) → Decidable (β a)] → FinEnum ((a : α) ×' β a)
PSigma.finEnumPropRight {β: α → Prop
β : α: Type u
α → Prop: Type
Prop} [FinEnum: Sort ?u.74269 → Sort (max1?u.74269)
FinEnum α: Type u
α] [∀ a: ?m.74273
a, Decidable: Prop → Type
Decidable (β: α → Prop
β a: ?m.74273
a)] :
    FinEnum: Sort ?u.74279 → Sort (max1?u.74279)
FinEnum (Σ'a: ?m.74284
a, β: α → Prop
β a: ?m.74284
a) :=
  FinEnum.ofEquiv: (α : Sort ?u.74294) → {β : Sort ?u.74293} → [inst : FinEnum α] → β ≃ α → FinEnum β
FinEnum.ofEquiv { a: ?m.74298
a // β: α → Prop
β a: ?m.74298
a }
    ⟨fun ⟨x: α
x, y: β x
y⟩ => ⟨x: α
x, y: β x
y⟩, fun ⟨x: α
x, y: β x
y⟩ => ⟨x: α
x, y: β x
y⟩, fun ⟨_, _⟩ => rfl: ∀ {α : Sort ?u.74627} {a : α}, a = a
rfl, fun ⟨_, _⟩ => rfl: ∀ {α : Sort ?u.74765} {a : α}, a = a
rfl⟩
#align fin_enum.psigma.fin_enum_prop_right FinEnum.PSigma.finEnumPropRight: {α : Type u} → {β : α → Prop} → [inst : FinEnum α] → [inst : (a : α) → Decidable (β a)] → FinEnum ((a : α) ×' β a)
FinEnum.PSigma.finEnumPropRight

instance PSigma.finEnumPropProp: {α : Prop} → {β : α → Prop} → [inst : Decidable α] → [inst : (a : α) → Decidable (β a)] → FinEnum ((a : α) ×' β a)
PSigma.finEnumPropProp {α: Prop
α : Prop: Type
Prop} {β: α → Prop
β : α: Prop
α → Prop: Type
Prop} [Decidable: Prop → Type
Decidable α: Prop
α] [∀ a: ?m.75132
a, Decidable: Prop → Type
Decidable (β: α → Prop
β a: ?m.75132
a)] :
    FinEnum: Sort ?u.75138 → Sort (max1?u.75138)
FinEnum (Σ'a: ?m.75143
a, β: α → Prop
β a: ?m.75143
a) :=
  if h: ?m.75197
h : ∃ a: ?m.75156
a, β: α → Prop
β a: ?m.75156
a then ofList: {α : Type ?u.75199} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList [⟨h: ?m.75197
h.fst: ∀ {b : Prop} {p : b → Prop}, Exists p → b
fst, h: ?m.75197
h.snd: ∀ {b : Prop} {p : b → Prop} (h : Exists p), p (_ : b)
snd⟩] (by
Goals accomplished! 🐙 α✝: Type u

β✝: α✝ → Type v

α: Prop

β: α → Prop

inst✝¹: Decidable α

inst✝: (a : α) → Decidable (β a)

h: ∃ a, β a

∀ (x : (a : α) ×' β a), x ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }]rintro ⟨⟩: (a : α) ×' β a
⟨⟩α✝: Type u

β✝: α✝ → Type v

α: Prop

β: α → Prop

inst✝¹: Decidable α

inst✝: (a : α) → Decidable (β a)

h: ∃ a, β a

fst✝: α

snd✝: β fst✝

mk{ fst := fst✝, snd := snd✝ } ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }] α✝: Type u

β✝: α✝ → Type v

α: Prop

β: α → Prop

inst✝¹: Decidable α

inst✝: (a : α) → Decidable (β a)

h: ∃ a, β a

∀ (x : (a : α) ×' β a), x ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }];α✝: Type u

β✝: α✝ → Type v

α: Prop

β: α → Prop

inst✝¹: Decidable α

inst✝: (a : α) → Decidable (β a)

h: ∃ a, β a

fst✝: α

snd✝: β fst✝

mk{ fst := fst✝, snd := snd✝ } ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }] α✝: Type u

β✝: α✝ → Type v

α: Prop

β: α → Prop

inst✝¹: Decidable α

inst✝: (a : α) → Decidable (β a)

h: ∃ a, β a

∀ (x : (a : α) ×' β a), x ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }]simp
Goals accomplished! 🐙)
  else ofList: {α : Type ?u.75616} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
ofList []: List ?m.75703
[] fun a: ?m.75705
a => (h: ?m.75614
h ⟨a: ?m.75705
a.fst: ∀ {α : Sort ?u.75716} {β : α → Sort ?u.75715}, PSigma β → α
fst, a: ?m.75705
a.snd: ∀ {α : Sort ?u.75721} {β : α → Sort ?u.75720} (self : PSigma β), β (_ : α)
snd⟩).elim: ∀ {C : Sort ?u.75725}, False → C
elim
#align fin_enum.psigma.fin_enum_prop_prop FinEnum.PSigma.finEnumPropProp: {α : Prop} → {β : α → Prop} → [inst : Decidable α] → [inst : (a : α) → Decidable (β a)] → FinEnum ((a : α) ×' β a)
FinEnum.PSigma.finEnumPropProp

instance: {α : Type u} → [inst : FinEnum α] → Fintype α
instance (priority := 100) [FinEnum: Sort ?u.76093 → Sort (max1?u.76093)
FinEnum α: Type u
α] : Fintype: Type ?u.76096 → Type ?u.76096
Fintype α: Type u
α where
  elems := univ: {α : Type ?u.76102} → [inst : Fintype α] → Finset α
univ.map: {α : Type ?u.76134} → {β : Type ?u.76133} → (α ↪ β) → Finset α → Finset β
map (Equiv: {α : Sort ?u.76142} → [self : FinEnum α] → α ≃ Fin (card α)
Equiv).symm: {α : Sort ?u.76163} → {β : Sort ?u.76162} → α ≃ β → β ≃ α
symm.toEmbedding: {α : Sort ?u.76169} → {β : Sort ?u.76168} → α ≃ β → α ↪ β
toEmbedding
  complete := by
Goals accomplished! 🐙 α: Type u

β: α → Type v

inst✝: FinEnum α

∀ (x : α), x ∈ map (Equiv.toEmbedding Equiv.symm) univintrosα: Type u

β: α → Type v

inst✝: FinEnum α

x✝: α

x✝ ∈ map (Equiv.toEmbedding Equiv.symm) univ α: Type u

β: α → Type v

inst✝: FinEnum α

∀ (x : α), x ∈ map (Equiv.toEmbedding Equiv.symm) univ;α: Type u

β: α → Type v

inst✝: FinEnum α

x✝: α

x✝ ∈ map (Equiv.toEmbedding Equiv.symm) univ α: Type u

β: α → Type v

inst✝: FinEnum α

∀ (x : α), x ∈ map (Equiv.toEmbedding Equiv.symm) univsimp
Goals accomplished! 🐙

/-- For `Pi.cons x xs y f` create a function where every `i ∈ xs` is mapped to `f i` and
`x` is mapped to `y`  -/
def Pi.cons: [inst : DecidableEq α] → (x : α) → (xs : List α) → β x → ((a : α) → a ∈ xs → β a) → (a : α) → a ∈ x :: xs → β a
Pi.cons [DecidableEq: Sort ?u.76508 → Sort (max1?u.76508)
DecidableEq α: Type u
α] (x: α
x : α: Type u
α) (xs: List α
xs : List: Type ?u.76519 → Type ?u.76519
List α: Type u
α) (y: β x
y : β: α → Type v
β x: α
x) (f: (a : α) → a ∈ xs → β a
f : ∀ a: ?m.76525
a, a: ?m.76525
a ∈ xs: List α
xs → β: α → Type v
β a: ?m.76525
a) :
    ∀ a: ?m.76562
a, a: ?m.76562
a ∈ (x: α
x :: xs: List α
xs : List: Type ?u.76584 → Type ?u.76584
List α: Type u
α) → β: α → Type v
β a: ?m.76562
a
  | b: α
b, h: b ∈ x :: xs
h => if h': ?m.76658
h' : b: α
b = x: α
x then cast: {α β : Sort ?u.76650} → α = β → α → β
cast (by
Goals accomplished! 🐙 α: Type u

β: α → Type v

inst✝: DecidableEq α

x: α

xs: List α

y: β x

f: (a : α) → a ∈ xs → β a

b: α

h: b ∈ x :: xs

h': b = x

β x = β brw [α: Type u

β: α → Type v

inst✝: DecidableEq α

x: α

xs: List α

y: β x

f: (a : α) → a ∈ xs → β a

b: α

h: b ∈ x :: xs

h': b = x

β x = β bh': b = x
h'α: Type u

β: α → Type v

inst✝: DecidableEq α

x: α

xs: List α

y: β x

f: (a : α) → a ∈ xs → β a

b: α

h: b ∈ x :: xs

h': b = x

β x = β x]
Goals accomplished! 🐙) y: β x
y else f: (a : α) → a ∈ xs → β a
f b: α
b (List.mem_of_ne_of_mem: ∀ {α : Type ?u.76660} {a y : α} {l : List α}, a ≠ y → a ∈ y :: l → a ∈ l
List.mem_of_ne_of_mem h': ?m.76658
h' h: b ∈ x :: xs
h)
#align fin_enum.pi.cons FinEnum.Pi.cons: {α : Type u} →
  {β : α → Type v} →
    [inst : DecidableEq α] → (x : α) → (xs : List α) → β x → ((a : α) → a ∈ xs → β a) → (a : α) → a ∈ x :: xs → β a
FinEnum.Pi.cons

/-- Given `f` a function whose domain is `x :: xs`, produce a function whose domain
is restricted to `xs`.  -/
def Pi.tail: {x : α} → {xs : List α} → ((a : α) → a ∈ x :: xs → β a) → (a : α) → a ∈ xs → β a
Pi.tail {x: α
x : α: Type u
α} {xs: List α
xs : List: Type ?u.76985 → Type ?u.76985
List α: Type u
α} (f: (a : α) → a ∈ x :: xs → β a
f : ∀ a: ?m.76989
a, a: ?m.76989
a ∈ (x: α
x :: xs: List α
xs : List: Type ?u.77011 → Type ?u.77011
List α: Type u
α) → β: α → Type v
β a: ?m.76989
a) : ∀ a: ?m.77030
a, a: ?m.77030
a ∈ xs: List α
xs → β: α → Type v
β a: ?m.77030
a
  | a: α
a, h: a ∈ xs
h => f: (a : α) → a ∈ x :: xs → β a
f a: α
a (List.mem_cons_of_mem: ∀ {α : Type ?u.77088} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: l
List.mem_cons_of_mem _: ?m.77089
_ h: a ∈ xs
h)
#align fin_enum.pi.tail FinEnum.Pi.tail: {α : Type u} → {β : α → Type v} → {x : α} → {xs : List α} → ((a : α) → a ∈ x :: xs → β a) → (a : α) → a ∈ xs → β a
FinEnum.Pi.tail

/-- `pi xs f` creates the list of functions `g` such that, for `x ∈ xs`, `g x ∈ f x` -/
def pi: {β : α → Type (maxuv)} →
  [inst : DecidableEq α] → (xs : List α) → ((a : α) → List (β a)) → List ((a : α) → a ∈ xs → β a)
pi {β: α → Type (maxuv)
β : α: Type u
α → Type max u v: Type ((maxuv)+1)
Type max u v} [DecidableEq: Sort ?u.77329 → Sort (max1?u.77329)
DecidableEq α: Type u
α] :
    ∀ xs: List α
xs : List: Type ?u.77339 → Type ?u.77339
List α: Type u
α, (∀ a: ?m.77344
a, List: Type ?u.77347 → Type ?u.77347
List (β: α → Type (maxuv)
β a: ?m.77344
a)) → List: Type ?u.77349 → Type ?u.77349
List (∀ a: ?m.77351
a, a: ?m.77351
a ∈ xs: List α
xs → β: α → Type (maxuv)
β a: ?m.77351
a)
  | [], _ => [fun x: ?m.77428
x h: ?m.77431
h => (List.not_mem_nil: ∀ {α : Type ?u.77433} (a : α), ¬a ∈ []
List.not_mem_nil x: ?m.77428
x h: ?m.77431
h).elim: {C : Sort ?u.77435} → False → C
elim]
  | x: α
x :: xs: List α
xs, fs: (a : α) → List (β a)
fs => FinEnum.Pi.cons: {α : Type ?u.77526} →
  {β : α → Type ?u.77525} →
    [inst : DecidableEq α] → (x : α) → (xs : List α) → β x → ((a : α) → a ∈ xs → β a) → (a : α) → a ∈ x :: xs → β a
FinEnum.Pi.cons x: α
x xs: List α
xs <$> fs: (a : α) → List (β a)
fs x: α
x <*> pi: {β : α → Type (maxuv)} →
  [inst : DecidableEq α] → (xs : List α) → ((a : α) → List (β a)) → List ((a : α) → a ∈ xs → β a)
pi xs: List α
xs fs: (a : α) → List (β a)
fs
#align fin_enum.pi FinEnum.pi: {α : Type u} →
  {β : α → Type (maxuv)} →
    [inst : DecidableEq α] → (xs : List α) → ((a : α) → List (β a)) → List ((a : α) → a ∈ xs → β a)
FinEnum.pi

theorem mem_pi: ∀ {β : α → Type (maxuu_1)} [inst : FinEnum α] [inst_1 : (a : α) → FinEnum (β a)] (xs