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.
```/-
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.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.2SortSort _: 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: ℕ → TypeFin 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.249List α: Type uα) (h: ∀ (x : α), x ∈ xsh : ∀ x: αx : α: Type uα, x: αx ∈ xs: List αxs) (h': List.Nodup xsh' : List.Nodup: {α : Type ?u.285} → List α → PropList.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.319x => ⟨xs: List αxs.indexOf: {α : Type ?u.326} → [inst : BEq α] → α → List α → ℕindexOf x: ?m.319x, byGoals accomplished! 🐙 α: Type uβ: α → Type vinst✝: DecidableEq αxs: List αh: ∀ (x : α), x ∈ xsh': List.Nodup xsx: αList.indexOf x xs < List.length xsrw [α: Type uβ: α → Type vinst✝: DecidableEq αxs: List αh: ∀ (x : α), x ∈ xsh': List.Nodup xsx: α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 ∈ lList.indexOf_lt_lengthα: Type uβ: α → Type vinst✝: DecidableEq αxs: List αh: ∀ (x : α), x ∈ xsh': List.Nodup xsx: αx ∈ xs]α: Type uβ: α → Type vinst✝: DecidableEq αxs: List αh: ∀ (x : α), x ∈ xsh': List.Nodup xsx: αx ∈ xs α: Type uβ: α → Type vinst✝: DecidableEq αxs: List αh: ∀ (x : α), x ∈ xsh': List.Nodup xsx: αList.indexOf x xs < List.length xs;α: Type uβ: α → Type vinst✝: DecidableEq αxs: List αh: ∀ (x : α), x ∈ xsh': List.Nodup xsx: αx ∈ xs α: Type uβ: α → Type vinst✝: DecidableEq αxs: List αh: ∀ (x : α), x ∈ xsh': List.Nodup xsx: αList.indexOf x xs < List.length xsapply h: ∀ (x : α), x ∈ xshGoals accomplished! 🐙⟩, fun ⟨i: ℕi, h: i < List.length xsh⟩ =>
xs: List αxs.nthLe: {α : Type ?u.410} → (l : List α) → (n : ℕ) → n < List.length l → αnthLe _: ℕ_ h: i < List.length xsh, fun x: ?m.487x => byGoals accomplished! 🐙 α: Type uβ: α → Type vinst✝: DecidableEq αxs: List αh: ∀ (x : α), x ∈ xsh': List.Nodup xsx: α(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) =   xsimpGoals accomplished! 🐙, fun ⟨i: ℕi, h: i < List.length xsh⟩ => byGoals accomplished! 🐙
α: Type uβ: α → Type vinst✝: DecidableEq αxs: List αh✝: ∀ (x : α), x ∈ xsh': List.Nodup xsx✝: 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.2724List α: Type uα) (h: ∀ (x : α), x ∈ xsh : ∀ 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 (byGoals accomplished! 🐙 α: Type uβ: α → Type vinst✝: 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.5238List α: ?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α := byGoals accomplished! 🐙
α: Type uβ: α → Type vinst✝: FinEnum αx: αx ∈ toList αsimp [toList: (α : Type ?u.5491) → [inst : FinEnum α] → List αtoList]α: Type uβ: α → Type vinst✝: FinEnum αx: α∃ a, ↑Equiv.symm a = x α: Type uβ: α → Type vinst✝: FinEnum αx: αx ∈ toList α;α: Type uβ: α → Type vinst✝: FinEnum αx: α∃ a, ↑Equiv.symm a = x α: Type uβ: α → Type vinst✝: FinEnum αx: αx ∈ toList αexists Equiv: {α : Sort ?u.8962} → [self : FinEnum α] → α ≃ Fin (card α)Equiv x: αxα: Type uβ: α → Type vinst✝: FinEnum αx: α↑Equiv.symm (↑Equiv x) = x α: Type uβ: α → Type vinst✝: FinEnum αx: αx ∈ toList α;α: Type uβ: α → Type vinst✝: FinEnum αx: α↑Equiv.symm (↑Equiv x) = x α: Type uβ: α → Type vinst✝: FinEnum αx: αx ∈ toList αsimpGoals 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 α → PropList.Nodup (toList: (α : Type ?u.9193) → [inst : FinEnum α] → List αtoList α: Type uα) := byGoals accomplished! 🐙
α: Type uβ: α → Type vinst✝: FinEnum αList.Nodup (toList α)simp [toList: (α : Type ?u.9205) → [inst : FinEnum α] → List αtoList]α: Type uβ: α → Type vinst✝: FinEnum αList.Nodup (List.map (↑Equiv.symm) (List.finRange (card α))) α: Type uβ: α → Type vinst✝: FinEnum αList.Nodup (toList α);α: Type uβ: α → Type vinst✝: FinEnum αList.Nodup (List.map (↑Equiv.symm) (List.finRange (card α))) α: Type uβ: α → Type vinst✝: 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 vinst✝: FinEnum αhfInjective ↑Equiv.symmα: Type uβ: α → Type vinst✝: FinEnum αaList.Nodup (List.finRange (card α)) <;> [α: Type uβ: α → Type vinst✝: FinEnum αList.Nodup (List.map (↑Equiv.symm) (List.finRange (card α)))apply Equiv.injective: ∀ {α : Sort ?u.9362} {β : Sort ?u.9361} (e : α ≃ β), Injective ↑eEquiv.injectiveGoals accomplished! 🐙; α: Type uβ: α → Type vinst✝: FinEnum αList.Nodup (List.map (↑Equiv.symm) (List.finRange (card α)))apply List.nodup_finRange: ∀ (n : ℕ), List.Nodup (List.finRange n)List.nodup_finRangeGoals 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 fh : Surjective: {α : Sort ?u.9436} → {β : Sort ?u.9435} → (α → β) → PropSurjective 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) (byGoals accomplished! 🐙 α: Type uβ✝: α → Type vβ: Type ?u.9537f: β → αinst✝¹: DecidableEq αinst✝: FinEnum βh: Surjective f∀ (x : α), x ∈ List.map f (toList β)introα: Type uβ✝: α → Type vβ: Type ?u.9537f: β → αinst✝¹: DecidableEq αinst✝: FinEnum βh: Surjective fx✝: αx✝ ∈ List.map f (toList β) α: Type uβ✝: α → Type vβ: Type ?u.9537f: β → αinst✝¹: DecidableEq αinst✝: FinEnum βh: Surjective f∀ (x : α), x ∈ List.map f (toList β);α: Type uβ✝: α → Type vβ: Type ?u.9537f: β → αinst✝¹: DecidableEq αinst✝: FinEnum βh: Surjective fx✝: αx✝ ∈ List.map f (toList β) α: Type uβ✝: α → Type vβ: Type ?u.9537f: β → αinst✝¹: DecidableEq αinst✝: FinEnum βh: Surjective f∀ (x : α), x ∈ List.map f (toList β)simpα: Type uβ✝: α → Type vβ: Type ?u.9537f: β → αinst✝¹: DecidableEq αinst✝: FinEnum βh: Surjective fx✝: α∃ a, f a = x✝ α: Type uβ✝: α → Type vβ: Type ?u.9537f: β → αinst✝¹: DecidableEq αinst✝: FinEnum βh: Surjective f∀ (x : α), x ∈ List.map f (toList β);α: Type uβ✝: α → Type vβ: Type ?u.9537f: β → αinst✝¹: DecidableEq αinst✝: FinEnum βh: Surjective fx✝: α∃ a, f a = x✝ α: Type uβ✝: α → Type vβ: Type ?u.9537f: β → αinst✝¹: DecidableEq αinst✝: FinEnum βh: Surjective f∀ (x : α), x ∈ List.map f (toList β)exact h: Surjective fh _: α_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 fh : Injective: {α : Sort ?u.13163} → {β : Sort ?u.13162} → (α → β) → PropInjective 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))
(byGoals accomplished! 🐙
α✝: Type uβ✝: α✝ → Type vα: Type ?u.13181β: Type ?u.13263f: α → β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.13263f: α → βinst✝¹: DecidableEq αinst✝: FinEnum βh: Injective fx: αx ∈ List.filterMap (partialInv f) (toList β)
α✝: Type uβ✝: α✝ → Type vα: Type ?u.13181β: Type ?u.13263f: α → β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 ↔ ptrue_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 bList.mem_filterMap]α✝: Type uβ✝: α✝ → Type vα: Type ?u.13181β: Type ?u.13263f: α → βinst✝¹: DecidableEq αinst✝: FinEnum βh: Injective fx: α∃ a, partialInv f a = some x
α✝: Type uβ✝: α✝ → Type vα: Type ?u.13181β: Type ?u.13263f: α → β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.13263f: α → βinst✝¹: DecidableEq αinst✝: FinEnum βh: Injective fx: αpartialInv f (f x) = some x
α✝: Type uβ✝: α✝ → Type vα: Type ?u.13181β: Type ?u.13263f: α → βinst✝¹: DecidableEq αinst✝: FinEnum βh: Injective f∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)simp only [h: Injective fh, Function.partialInv_left: ∀ {α : Type ?u.13632} {β : Sort ?u.13633} {f : α → β}, Injective f → ∀ (x : α), partialInv f (f x) = some xFunction.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 PEmptypempty : FinEnum: Sort ?u.13742 → Sort (max1?u.13742)FinEnum PEmpty: Sort ?u.13743PEmpty :=
ofList: {α : Type ?u.13745} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum αofList []: List ?m.13828[] fun x: ?m.13831x => PEmpty.elim: ∀ {C : Sort ?u.13834}, PEmpty → CPEmpty.elim x: ?m.13831x
#align fin_enum.pempty FinEnum.pempty: FinEnum PEmptyFinEnum.pempty

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

instance punit: FinEnum PUnitpunit : FinEnum: Sort ?u.14099 → Sort (max1?u.14099)FinEnum PUnit: Sort ?u.14100PUnit :=
ofList: {α : Type ?u.14102} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum αofList [PUnit.unit: PUnitPUnit.unit] fun x: ?m.14191x => byGoals accomplished! 🐙 α: Type uβ: α → Type vx: PUnitx ∈ [PUnit.unit]cases x: PUnitxα: Type uβ: α → Type vunitPUnit.unit ∈ [PUnit.unit] α: Type uβ: α → Type vx: PUnitx ∈ [PUnit.unit];α: Type uβ: α → Type vunitPUnit.unit ∈ [PUnit.unit] α: Type uβ: α → Type vx: PUnitx ∈ [PUnit.unit]simpGoals accomplished! 🐙
#align fin_enum.punit FinEnum.punit: FinEnum PUnitFinEnum.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.14508x => byGoals accomplished! 🐙 α: Type uβ✝: α → Type vβ: Type ?u.14483inst✝¹: FinEnum αinst✝: FinEnum βx: α × βx ∈ toList α ×ˢ toList βcases x: α × βxα: Type uβ✝: α → Type vβ: Type ?u.14483inst✝¹: FinEnum αinst✝: FinEnum βfst✝: αsnd✝: βmk(fst✝, snd✝) ∈ toList α ×ˢ toList β α: Type uβ✝: α → Type vβ: Type ?u.14483inst✝¹: FinEnum αinst✝: FinEnum βx: α × βx ∈ toList α ×ˢ toList β;α: Type uβ✝: α → Type vβ: Type ?u.14483inst✝¹: FinEnum αinst✝: FinEnum βfst✝: αsnd✝: βmk(fst✝, snd✝) ∈ toList α ×ˢ toList β α: Type uβ✝: α → Type vβ: Type ?u.14483inst✝¹: FinEnum αinst✝: FinEnum βx: α × βx ∈ toList α ×ˢ toList βsimpGoals 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.17896x => byGoals accomplished! 🐙 α: Type uβ✝: α → Type vβ: Type ?u.17715inst✝¹: FinEnum αinst✝: FinEnum βx: α ⊕ βx ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)cases x: α ⊕ βxα: Type uβ✝: α → Type vβ: Type ?u.17715inst✝¹: FinEnum αinst✝: FinEnum βval✝: αinlSum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)α: Type uβ✝: α → Type vβ: Type ?u.17715inst✝¹: FinEnum αinst✝: FinEnum βval✝: βinrSum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β) α: Type uβ✝: α → Type vβ: Type ?u.17715inst✝¹: FinEnum αinst✝: FinEnum βx: α ⊕ βx ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)<;>α: Type uβ✝: α → Type vβ: Type ?u.17715inst✝¹: FinEnum αinst✝: FinEnum βval✝: αinlSum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)α: Type uβ✝: α → Type vβ: Type ?u.17715inst✝¹: FinEnum αinst✝: FinEnum βval✝: βinrSum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β) α: Type uβ✝: α → Type vβ: Type ?u.17715inst✝¹: FinEnum αinst✝: FinEnum βx: α ⊕ βx ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)simpGoals 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: ℕ → TypeFin n: ?m.29326n) :=
ofList: {α : Type ?u.29332} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum αofList (List.finRange: (n : ℕ) → List (Fin n)List.finRange _: ℕ_) (byGoals accomplished! 🐙 α: Type uβ: α → Type vn: ℕ∀ (x : Fin n), x ∈ List.finRange nsimpGoals 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: TypeProp)] :
FinEnum: Sort ?u.32058 → Sort (max1?u.32058)FinEnum (Quotient: {α : Sort ?u.32059} → Setoid α → Sort ?u.32059Quotient 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.32084x => Quotient.inductionOn: ∀ {α : Sort ?u.32086} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s),
(∀ (a : α), motive (Quotient.mk s a)) → motive qQuotient.inductionOn x: ?m.32084x fun x: ?m.32233x => ⟨x: ?m.32233x, rfl: ∀ {α : Sort ?u.32244} {a : α}, a = arfl⟩
#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.32404List α: Type uα → List: Type ?u.32406 → Type ?u.32406List (Finset: Type ?u.32407 → Type ?u.32407Finset α: Type uα)
| [] => [∅: ?m.32428∅]
| x: αx :: xs: List αxs => do
let r: ?m.32585r ← Finset.enum: [inst : DecidableEq α] → List α → List (Finset α)Finset.enum xs: List αxs
[r: ?m.32585r, {x: αx} ∪ r: ?m.32585r]
#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 ∈ xsFinset.mem_enum [DecidableEq: Sort ?u.33067 → Sort (max1?u.33067)DecidableEq α: Type uα] (s: Finset αs : Finset: Type ?u.33076 → Type ?u.33076Finset α: Type uα) (xs: List αxs : List: Type ?u.33079 → Type ?u.33079List α: Type uα) :
s: Finset αs ∈ Finset.enum: {α : Type ?u.33088} → [inst : DecidableEq α] → List α → List (Finset α)Finset.enum xs: List αxs ↔ ∀ x: ?m.33219x ∈ s: Finset αs, x: ?m.33219x ∈ xs: List αxs := byGoals accomplished! 🐙
α: Type uβ: α → Type vinst✝: DecidableEq αs: Finset αxs: List αs ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xsinduction' xs: List αxs with xs_hd: ?m.33300xs_hd generalizing s: Finset αsα: Type uβ: α → Type vinst✝: DecidableEq αs✝, s: Finset αnils ∈ enum [] ↔ ∀ (x : α), x ∈ s → x ∈ []α: Type uβ: α → Type vinst✝: 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 vinst✝: DecidableEq αs: Finset αxs: List αs ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs<;>α: Type uβ: α → Type vinst✝: DecidableEq αs✝, s: Finset αnils ∈ enum [] ↔ ∀ (x : α), x ∈ s → x ∈ []α: Type uβ: α → Type vinst✝: 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 vinst✝: 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 vinst✝: 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 vinst✝: DecidableEq αs: Finset αxs: List αs ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs·α: Type uβ: α → Type vinst✝: DecidableEq αs✝, s: Finset αnils = ∅ ↔ ∀ (x : α), x ∈ s → False α: Type uβ: α → Type vinst✝: DecidableEq αs✝, s: Finset αnils = ∅ ↔ ∀ (x : α), x ∈ s → Falseα: Type uβ: α → Type vinst✝: 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 ∈ sFinset.eq_empty_iff_forall_not_mem]Goals accomplished! 🐙
α: Type uβ: α → Type vinst✝: DecidableEq αs: Finset αxs: List αs ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs·α: Type uβ: α → Type vinst✝: 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 vinst✝: 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 vinst✝: 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 vinst✝: 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 vinst✝: 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 vinst✝: 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 vinst✝: 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 vinst✝: 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} ∪ ah'⟨a, h, h'⟩: (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)⟩ x: αx hx: x ∈ shxα: Type uβ: α → Type vinst✝: 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} ∪ ax: αhx: x ∈ scons.mp.intro.introx = xs_hd ∨ x ∈ tail✝
α: Type uβ: α → Type vinst✝: 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} ∪ ah' with _ h': ?m.52372h' a bα: Type uβ: α → Type vinst✝: 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 ∈ sh✝: s = acons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝α: Type uβ: α → Type vinst✝: 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 ∈ sh': s = {xs_hd} ∪ acons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝
α: Type uβ: α → Type vinst✝: 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 vinst✝: 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 ∈ sh✝: s = acons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝ α: Type uβ: α → Type vinst✝: 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 ∈ sh✝: s = acons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝α: Type uβ: α → Type vinst✝: 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 ∈ sh': s = {xs_hd} ∪ acons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝rightα: Type uβ: α → Type vinst✝: 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 ∈ sh✝: s = acons.mp.intro.intro.inl.hx ∈ tail✝
α: Type uβ: α → Type vinst✝: 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 ∈ sh✝: s = acons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝apply h: ∀ (x : α), x ∈ a → x ∈ tail✝hα: Type uβ: α → Type vinst✝: 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 ∈ sh✝: s = acons.mp.intro.intro.inl.h.ax ∈ a
α: Type uβ: α → Type vinst✝: 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 ∈ sh✝: s = acons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝subst a: Finset αaα: Type uβ: α → Type vinst✝: DecidableEq αs✝: Finset αxs_hd: αtail✝: List αtail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝s: Finset αx: αhx: x ∈ sh: ∀ (x : α), x ∈ s → x ∈ tail✝cons.mp.intro.intro.inl.h.ax ∈ s
α: Type uβ: α → Type vinst✝: 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 ∈ sh✝: s = acons.mp.intro.intro.inlx = xs_hd ∨ x ∈ tail✝exact hx: x ∈ shxGoals accomplished! 🐙
α: Type uβ: α → Type vinst✝: 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 vinst✝: 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 ∈ sh': s = {xs_hd} ∪ acons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝ α: Type uβ: α → Type vinst✝: 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 ∈ sh': s = {xs_hd} ∪ acons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝simp only [h': ?m.52372h', mem_union: ∀ {α : Type ?u.52458} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ tmem_union, mem_singleton: ∀ {α : Type ?u.52491} {a b : α}, b ∈ {a} ↔ b = amem_singleton] at hx: x ∈ shx⊢α: Type uβ: α → Type vinst✝: 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} ∪ ahx: x = xs_hd ∨ x ∈ acons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝
α: Type uβ: α → Type vinst✝: 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 ∈ sh': s = {xs_hd} ∪ acons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝cases' hx: x = xs_hd ∨ x ∈ ahx with hx: ?m.52712hx hx': ?m.52713hx'α: Type uβ: α → Type vinst✝: 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} ∪ ahx: x = xs_hdcons.mp.intro.intro.inr.inlx = xs_hd ∨ x ∈ tail✝α: Type uβ: α → Type vinst✝: 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} ∪ ahx': x ∈ acons.mp.intro.intro.inr.inrx = xs_hd ∨ x ∈ tail✝
α: Type uβ: α → Type vinst✝: 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 ∈ sh': s = {xs_hd} ∪ acons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝·α: Type uβ: α → Type vinst✝: 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} ∪ ahx: x = xs_hdcons.mp.intro.intro.inr.inlx = xs_hd ∨ x ∈ tail✝ α: Type uβ: α → Type vinst✝: 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} ∪ ahx: x = xs_hdcons.mp.intro.intro.inr.inlx = xs_hd ∨ x ∈ tail✝α: Type uβ: α → Type vinst✝: 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} ∪ ahx': x ∈ acons.mp.intro.intro.inr.inrx = xs_hd ∨ x ∈ tail✝exact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl hx: ?m.52712hxGoals accomplished! 🐙
α: Type uβ: α → Type vinst✝: 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 ∈ sh': s = {xs_hd} ∪ acons.mp.intro.intro.inrx = xs_hd ∨ x ∈ tail✝·α: Type uβ: α → Type vinst✝: 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} ∪ ahx': x ∈ acons.mp.intro.intro.inr.inrx = xs_hd ∨ x ∈ tail✝ α: Type uβ: α → Type vinst✝: 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} ∪ ahx': x ∈ acons.mp.intro.intro.inr.inrx = xs_hd ∨ x ∈ tail✝exact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (h: ∀ (x : α), x ∈ a → x ∈ tail✝h _: α_ hx': ?m.52713hx')Goals accomplished! 🐙
α: Type uβ: α → Type vinst✝: 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 vinst✝: 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 vinst✝: 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: ?bhα: Type uβ: α → Type vinst✝: 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 vinst✝: 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.33300xs_hd} : Finset: Type ?u.52798 → Type ?u.52798Finset α: Type uα)α: Type uβ: α → Type vinst✝: 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 vinst✝: 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 → cand_imp, mem_sdiff: ∀ {α : Type ?u.52947} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s \ t ↔ a ∈ s ∧ ¬a ∈ tmem_sdiff, mem_singleton: ∀ {α : Type ?u.52982} {a b : α}, b ∈ {a} ↔ b = amem_singleton]α: Type uβ: α → Type vinst✝: 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 vinst✝: 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 → bor_iff_not_imp_left] at h: ?bhα: Type uβ: α → Type vinst✝: 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 vinst✝: 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 vinst✝: 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 vinst✝: 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.53485h : xs_hd: ?m.33300xs_hd ∈ s: Finset αsα: Type uβ: α → Type vinst✝: 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 ∈ sposs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}α: Type uβ: α → Type vinst✝: 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 ∈ snegs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
α: Type uβ: α → Type vinst✝: 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 vinst✝: 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 ∈ sposs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd} α: Type uβ: α → Type vinst✝: 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 ∈ sposs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}α: Type uβ: α → Type vinst✝: 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 ∈ snegs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}have : {xs_hd: ?m.33300xs_hd} ⊆ s: Finset αsα: Type uβ: α → Type vinst✝: 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 ∈ sthis{xs_hd} ⊆ sα: Type uβ: α → Type vinst✝: 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 ∈ sthis: {xs_hd} ⊆ sposs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
α: Type uβ: α → Type vinst✝: 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 ∈ sposs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}simp only [HasSubset.Subset: {α : Type ?u.53572} → [self : HasSubset α] → α → α → PropHasSubset.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 = amem_singleton]α: Type uβ: α → Type vinst✝: 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 ∈ sthis: {xs_hd} ⊆ sposs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
α: Type uβ: α → Type vinst✝: 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 ∈ sposs = 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 = tunion_sdiff_of_subset this: {xs_hd} ⊆ sthis, or_true_iff: ∀ (p : Prop), p ∨ True ↔ Trueor_true_iff, Finset.union_sdiff_of_subset: ∀ {α : Type ?u.53827} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → s ∪ t \ s = tFinset.union_sdiff_of_subset,
eq_self_iff_true: ∀ {α : Sort ?u.53850} (a : α), a = a ↔ Trueeq_self_iff_true]Goals accomplished! 🐙
α: Type uβ: α → Type vinst✝: 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 vinst✝: 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 ∈ snegs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd} α: Type uβ: α → Type vinst✝: 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 ∈ snegs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}leftα: Type uβ: α → Type vinst✝: 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 ∈ sneg.hs = s \ {xs_hd}
α: Type uβ: α → Type vinst✝: 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 ∈ snegs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}symmα: Type uβ: α → Type vinst✝: 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 ∈ sneg.hs \ {xs_hd} = s
α: Type uβ: α → Type vinst✝: 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 ∈ snegs = 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 vinst✝: 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 ∈ sneg.hs ∩ {xs_hd} ⊆ ∅
α: Type uβ: α → Type vinst✝: 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 ∈ snegs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}intro a: αaα: Type uβ: α → Type vinst✝: 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 ∈ sa: αneg.ha ∈ s ∩ {xs_hd} → a ∈ ∅
α: Type uβ: α → Type vinst✝: 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 ∈ snegs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}simp only [and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → cand_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 = amem_singleton]α: Type uβ: α → Type vinst✝: 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 ∈ sa: αneg.ha ∈ s → a = xs_hd → a ∈ ∅
α: Type uβ: α → Type vinst✝: 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 ∈ snegs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}rintro h₀: a ∈ sh₀ rfl: a = xs_hdrflα: Type uβ: α → Type vinst✝: DecidableEq αs✝: Finset αtail✝: List αtail_ih✝: ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝s: Finset αa: αh₀: a ∈ sh✝: ∀ (x : α), x ∈ s → ¬x = a → x ∈ tail✝h: ¬a ∈ sneg.ha ∈ ∅
α: Type uβ: α → Type vinst✝: 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 ∈ snegs = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}exact (h: ¬a ∈ sh h₀: a ∈ sh₀).elim: ∀ {C : Sort ?u.54583}, False → CelimGoals 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 ∈ xsFinEnum.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.54810Finset α: 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α)) (byGoals accomplished! 🐙 α: Type uβ: α → Type vinst✝: FinEnum α∀ (x : Finset α), x ∈ enum (toList α)introα: Type uβ: α → Type vinst✝: FinEnum αx✝: Finset αx✝ ∈ enum (toList α) α: Type uβ: α → Type vinst✝: FinEnum α∀ (x : Finset α), x ∈ enum (toList α);α: Type uβ: α → Type vinst✝: FinEnum αx✝: Finset αx✝ ∈ enum (toList α) α: Type uβ: α → Type vinst✝: FinEnum α∀ (x : Finset α), x ∈ enum (toList α)simpGoals 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: α → Propp : α: Type uα → Prop: TypeProp) [DecidablePred: {α : Sort ?u.58282} → (α → Prop) → Sort (max1?u.58282)DecidablePred p: α → Propp] : FinEnum: Sort ?u.58292 → Sort (max1?u.58292)FinEnum { x: ?m.58296x // p: α → Propp x: ?m.58296x } :=
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.58405x => if h: ?m.58439h : p: α → Propp x: ?m.58405x then some: {α : Type ?u.58419} → α → Option αsome ⟨_: ?m.58427_, h: ?m.58417h⟩ else none: {α : Type ?u.58441} → Option αnone)
(byGoals accomplished! 🐙 α: Type uβ: α → Type vinst✝¹: FinEnum αp: α → Propinst✝: 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 xh⟨x, h⟩: { x // p x }⟩α: Type uβ: α → Type vinst✝¹: FinEnum αp: α → Propinst✝: DecidablePred px: αh: p xmk{ val := x, property := h } ∈   List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α) α: Type uβ: α → Type vinst✝¹: FinEnum αp: α → Propinst✝: 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 vinst✝¹: FinEnum αp: α → Propinst✝: DecidablePred px: αh: p xmk{ val := x, property := h } ∈   List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α) α: Type uβ: α → Type vinst✝¹: FinEnum αp: α → Propinst✝: 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 vinst✝¹: FinEnum αp: α → Propinst✝: DecidablePred px: αh: p xmk∃ a, (if h : p a then some { val := a, property := h } else none) = some { val := x, property := h } α: Type uβ: α → Type vinst✝¹: FinEnum αp: α → Propinst✝: 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 vinst✝¹: FinEnum αp: α → Propinst✝: DecidablePred px: αh: p xmk∃ a, (if h : p a then some { val := a, property := h } else none) = some { val := x, property := h } α: Type uβ: α → Type vinst✝¹: FinEnum αp: α → Propinst✝: 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 vinst✝¹: FinEnum αp: α → Propinst✝: DecidablePred px: αh: p xmk(if h : p x then some { val := x, property := h } else none) = some { val := x, property := h } α: Type uβ: α → Type vinst✝¹: FinEnum αp: α → Propinst✝: 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 vinst✝¹: FinEnum αp: α → Propinst✝: DecidablePred px: αh: p xmk(if h : p x then some { val := x, property := h } else none) = some { val := x, property := h } α: Type uβ: α → Type vinst✝¹: FinEnum αp: α → Propinst✝: 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.64038a, FinEnum: Sort ?u.64041 → Sort (max1?u.64041)FinEnum (β: α → Type vβ a: ?m.64038a)] : 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.64156a => (toList: (α : Type ?u.64158) → [inst : FinEnum α] → List αtoList (β: α → Type vβ a: ?m.64156a)).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.64156a)
(byGoals accomplished! 🐙 α: Type uβ✝, β: α → Type vinst✝¹: 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 vinst✝¹: FinEnum αinst✝: (a : α) → FinEnum (β a)x: Sigma βx ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a)) α: Type uβ✝, β: α → Type vinst✝¹: FinEnum αinst✝: (a : α) → FinEnum (β a)∀ (x : Sigma β), x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a));α: Type uβ✝, β: α → Type vinst✝¹: FinEnum αinst✝: (a : α) → FinEnum (β a)x: Sigma βx ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a)) α: Type uβ✝, β: α → Type vinst✝¹: 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 vinst✝¹: 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 vinst✝¹: FinEnum αinst✝: (a : α) → FinEnum (β a)∀ (x : Sigma β), x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a));α: Type uβ✝, β: α → Type vinst✝¹: 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 vinst✝¹: FinEnum αinst✝: (a : α) → FinEnum (β a)∀ (x : Sigma β), x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a))simpGoals 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.70854a, FinEnum: Sort ?u.70857 → Sort (max1?u.70857)FinEnum (β: α → Type vβ a: ?m.70854a)] : FinEnum: Sort ?u.70861 → Sort (max1?u.70861)FinEnum (Σ'a: ?m.70866a, β: α → Type vβ a: ?m.70866a) :=
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 : α) × β iEquiv.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: TypeProp} {β: α → Type vβ : α: Propα → Type v: Type (v+1)Type v} [∀ a: ?m.71042a, FinEnum: Sort ?u.71045 → Sort (max1?u.71045)FinEnum (β: α → Type vβ a: ?m.71042a)] [Decidable: Prop → TypeDecidable α: Propα] :
FinEnum: Sort ?u.71051 → Sort (max1?u.71051)FinEnum (Σ'a: ?m.71056a, β: α → Type vβ a: ?m.71056a) :=
if h: ?m.71753h : α: 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.71073h)).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.71073h) fun ⟨a: αa, Ba: β aBa⟩ => byGoals accomplished! 🐙 α✝: Type uβ✝: α✝ → Type vα: Propβ: α → Type vinst✝¹: (a : α) → FinEnum (β a)inst✝: Decidable αh: αx✝: (a : α) ×' β aa: αBa: β a{ fst := a, snd := Ba } ∈ List.map (PSigma.mk h) (toList (β h))simpGoals accomplished! 🐙
else ofList: {α : Type ?u.71755} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum αofList []: List ?m.71838[] fun ⟨a: αa, Ba: β aBa⟩ => (h: ?m.71753h a: αa).elim: ∀ {C : Sort ?u.71873}, False → Celim
#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: TypeProp} [FinEnum: Sort ?u.74269 → Sort (max1?u.74269)FinEnum α: Type uα] [∀ a: ?m.74273a, Decidable: Prop → TypeDecidable (β: α → Propβ a: ?m.74273a)] :
FinEnum: Sort ?u.74279 → Sort (max1?u.74279)FinEnum (Σ'a: ?m.74284a, β: α → Propβ a: ?m.74284a) :=
FinEnum.ofEquiv: (α : Sort ?u.74294) → {β : Sort ?u.74293} → [inst : FinEnum α] → β ≃ α → FinEnum βFinEnum.ofEquiv { a: ?m.74298a // β: α → Propβ a: ?m.74298a }
⟨fun ⟨x: αx, y: β xy⟩ => ⟨x: αx, y: β xy⟩, fun ⟨x: αx, y: β xy⟩ => ⟨x: αx, y: β xy⟩, fun ⟨_, _⟩ => rfl: ∀ {α : Sort ?u.74627} {a : α}, a = arfl, fun ⟨_, _⟩ => rfl: ∀ {α : Sort ?u.74765} {a : α}, a = arfl⟩
#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: TypeProp} {β: α → Propβ : α: Propα → Prop: TypeProp} [Decidable: Prop → TypeDecidable α: Propα] [∀ a: ?m.75132a, Decidable: Prop → TypeDecidable (β: α → Propβ a: ?m.75132a)] :
FinEnum: Sort ?u.75138 → Sort (max1?u.75138)FinEnum (Σ'a: ?m.75143a, β: α → Propβ a: ?m.75143a) :=
if h: ?m.75197h : ∃ a: ?m.75156a, β: α → Propβ a: ?m.75156a then ofList: {α : Type ?u.75199} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum αofList [⟨h: ?m.75197h.fst: ∀ {b : Prop} {p : b → Prop}, Exists p → bfst, h: ?m.75197h.snd: ∀ {b : Prop} {p : b → Prop} (h : Exists p), p (_ : b)snd⟩] (byGoals accomplished! 🐙 α✝: Type uβ✝: α✝ → Type vα: Propβ: α → Propinst✝¹: Decidable αinst✝: (a : α) → Decidable (β a)h: ∃ a, β a∀ (x : (a : α) ×' β a), x ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }]rintro ⟨⟩: (a : α) ×' β a⟨⟩α✝: Type uβ✝: α✝ → Type vα: Propβ: α → Propinst✝¹: Decidable αinst✝: (a : α) → Decidable (β a)h: ∃ a, β afst✝: αsnd✝: β fst✝mk{ fst := fst✝, snd := snd✝ } ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }] α✝: Type uβ✝: α✝ → Type vα: Propβ: α → Propinst✝¹: Decidable αinst✝: (a : α) → Decidable (β a)h: ∃ a, β a∀ (x : (a : α) ×' β a), x ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }];α✝: Type uβ✝: α✝ → Type vα: Propβ: α → Propinst✝¹: Decidable αinst✝: (a : α) → Decidable (β a)h: ∃ a, β afst✝: αsnd✝: β fst✝mk{ fst := fst✝, snd := snd✝ } ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }] α✝: Type uβ✝: α✝ → Type vα: Propβ: α → Propinst✝¹: Decidable αinst✝: (a : α) → Decidable (β a)h: ∃ a, β a∀ (x : (a : α) ×' β a), x ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }]simpGoals accomplished! 🐙)
else ofList: {α : Type ?u.75616} → [inst : DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum αofList []: List ?m.75703[] fun a: ?m.75705a => (h: ?m.75614h ⟨a: ?m.75705a.fst: ∀ {α : Sort ?u.75716} {β : α → Sort ?u.75715}, PSigma β → αfst, a: ?m.75705a.snd: ∀ {α : Sort ?u.75721} {β : α → Sort ?u.75720} (self : PSigma β), β (_ : α)snd⟩).elim: ∀ {C : Sort ?u.75725}, False → Celim
#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.76096Fintype α: 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 := byGoals accomplished! 🐙 α: Type uβ: α → Type vinst✝: FinEnum α∀ (x : α), x ∈ map (Equiv.toEmbedding Equiv.symm) univintrosα: Type uβ: α → Type vinst✝: FinEnum αx✝: αx✝ ∈ map (Equiv.toEmbedding Equiv.symm) univ α: Type uβ: α → Type vinst✝: FinEnum α∀ (x : α), x ∈ map (Equiv.toEmbedding Equiv.symm) univ;α: Type uβ: α → Type vinst✝: FinEnum αx✝: αx✝ ∈ map (Equiv.toEmbedding Equiv.symm) univ α: Type uβ: α → Type vinst✝: FinEnum α∀ (x : α), x ∈ map (Equiv.toEmbedding Equiv.symm) univsimpGoals 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 → β aPi.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.76519List α: Type uα) (y: β xy : β: α → Type vβ x: αx) (f: (a : α) → a ∈ xs → β af : ∀ a: ?m.76525a, a: ?m.76525a ∈ xs: List αxs → β: α → Type vβ a: ?m.76525a) :
∀ a: ?m.76562a, a: ?m.76562a ∈ (x: αx :: xs: List αxs : List: Type ?u.76584 → Type ?u.76584List α: Type uα) → β: α → Type vβ a: ?m.76562a
| b: αb, h: b ∈ x :: xsh => if h': ?m.76658h' : b: αb = x: αx then cast: {α β : Sort ?u.76650} → α = β → α → βcast (byGoals accomplished! 🐙 α: Type uβ: α → Type vinst✝: DecidableEq αx: αxs: List αy: β xf: (a : α) → a ∈ xs → β ab: αh: b ∈ x :: xsh': b = xβ x = β brw [α: Type uβ: α → Type vinst✝: DecidableEq αx: αxs: List αy: β xf: (a : α) → a ∈ xs → β ab: αh: b ∈ x :: xsh': b = xβ x = β bh': b = xh'α: Type uβ: α → Type vinst✝: DecidableEq αx: αxs: List αy: β xf: (a : α) → a ∈ xs → β ab: αh: b ∈ x :: xsh': b = xβ x = β x]Goals accomplished! 🐙) y: β xy else f: (a : α) → a ∈ xs → β af b: αb (List.mem_of_ne_of_mem: ∀ {α : Type ?u.76660} {a y : α} {l : List α}, a ≠ y → a ∈ y :: l → a ∈ lList.mem_of_ne_of_mem h': ?m.76658h' h: b ∈ x :: xsh)
#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 → β aFinEnum.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 → β aPi.tail {x: αx : α: Type uα} {xs: List αxs : List: Type ?u.76985 → Type ?u.76985List α: Type uα} (f: (a : α) → a ∈ x :: xs → β af : ∀ a: ?m.76989a, a: ?m.76989a ∈ (x: αx :: xs: List αxs : List: Type ?u.77011 → Type ?u.77011List α: Type uα) → β: α → Type vβ a: ?m.76989a) : ∀ a: ?m.77030a, a: ?m.77030a ∈ xs: List αxs → β: α → Type vβ a: ?m.77030a
| a: αa, h: a ∈ xsh => f: (a : α) → a ∈ x :: xs → β af a: αa (List.mem_cons_of_mem: ∀ {α : Type ?u.77088} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: lList.mem_cons_of_mem _: ?m.77089_ h: a ∈ xsh)
#align fin_enum.pi.tail FinEnum.Pi.tail: {α : Type u} → {β : α → Type v} → {x : α} → {xs : List α} → ((a : α) → a ∈ x :: xs → β a) → (a : α) → a ∈ xs → β aFinEnum.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.77339List α: Type uα, (∀ a: ?m.77344a, List: Type ?u.77347 → Type ?u.77347List (β: α → Type (maxuv)β a: ?m.77344a)) → List: Type ?u.77349 → Type ?u.77349List (∀ a: ?m.77351a, a: ?m.77351a ∈ xs: List αxs → β: α → Type (maxuv)β a: ?m.77351a)
| [], _ => [fun x: ?m.77428x h: ?m.77431h => (List.not_mem_nil: ∀ {α : Type ?u.77433} (a : α), ¬a ∈ []List.not_mem_nil x: ?m.77428x h: ?m.77431h).elim: {C : Sort ?u.77435} → False → Celim]
| 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 → β aFinEnum.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```