[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : List.Nodup xs
x : α
⊢ List.indexOf x xs < List.length xs
[PROOFSTEP]
rw [List.indexOf_lt_length]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : List.Nodup xs
x : α
⊢ x ∈ xs
[PROOFSTEP]
apply h
[GOAL]
α : 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) =
    x
[PROOFSTEP]
simp
[GOAL]
α : 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 }
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
⊢ ∀ (x : α), x ∈ List.dedup xs
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ x ∈ toList α
[PROOFSTEP]
simp [toList]
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ ∃ a, ↑equiv.symm a = x
[PROOFSTEP]
exists equiv x
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ ↑equiv.symm (↑equiv x) = x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (toList α)
[PROOFSTEP]
simp [toList]
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (List.map (↑equiv.symm) (List.finRange (card α)))
[PROOFSTEP]
apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (List.map (↑equiv.symm) (List.finRange (card α)))
[PROOFSTEP]
apply List.Nodup.map
[GOAL]
case hf
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ Injective ↑equiv.symm
[PROOFSTEP]
apply Equiv.injective
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (List.finRange (card α))
[PROOFSTEP]
apply List.nodup_finRange
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.8688
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
⊢ ∀ (x : α), x ∈ List.map f (toList β)
[PROOFSTEP]
intro
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.8688
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
x✝ : α
⊢ x✝ ∈ List.map f (toList β)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.8688
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
x✝ : α
⊢ ∃ a, f a = x✝
[PROOFSTEP]
exact h _
[GOAL]
α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.11794
β : Type ?u.11876
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
⊢ ∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)
[PROOFSTEP]
intro x
[GOAL]
α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.11794
β : Type ?u.11876
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
x : α
⊢ x ∈ List.filterMap (partialInv f) (toList β)
[PROOFSTEP]
simp only [mem_toList, true_and_iff, List.mem_filterMap]
[GOAL]
α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.11794
β : Type ?u.11876
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
x : α
⊢ ∃ a, partialInv f a = some x
[PROOFSTEP]
use f x
[GOAL]
case h
α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.11794
β : Type ?u.11876
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
x : α
⊢ partialInv f (f x) = some x
[PROOFSTEP]
simp only [h, Function.partialInv_left]
[GOAL]
α : Type u
β : α → Type v
x : PUnit
⊢ x ∈ [PUnit.unit]
[PROOFSTEP]
cases x
[GOAL]
case unit
α : Type u
β : α → Type v
⊢ PUnit.unit ∈ [PUnit.unit]
[PROOFSTEP]
simp
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.13079
inst✝¹ : FinEnum α
inst✝ : FinEnum β
x : α × β
⊢ x ∈ toList α ×ˢ toList β
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u
β✝ : α → Type v
β : Type ?u.13079
inst✝¹ : FinEnum α
inst✝ : FinEnum β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ∈ toList α ×ˢ toList β
[PROOFSTEP]
simp
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.16461
inst✝¹ : FinEnum α
inst✝ : FinEnum β
x : α ⊕ β
⊢ x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
β✝ : α → Type v
β : Type ?u.16461
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : α
⊢ Sum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
β✝ : α → Type v
β : Type ?u.16461
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : β
⊢ Sum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
n : ℕ
⊢ ∀ (x : Fin n), x ∈ List.finRange n
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finset α
xs : List α
⊢ s ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs
[PROOFSTEP]
induction' xs with xs_hd generalizing s
[GOAL]
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ s : Finset α
⊢ s ∈ enum [] ↔ ∀ (x : α), x ∈ s → x ∈ []
[PROOFSTEP]
simp [*, Finset.enum]
[GOAL]
case cons
α : 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 α
⊢ s ∈ enum (xs_hd :: tail✝) ↔ ∀ (x : α), x ∈ s → x ∈ xs_hd :: tail✝
[PROOFSTEP]
simp [*, Finset.enum]
[GOAL]
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ s : Finset α
⊢ s = ∅ ↔ ∀ (x : α), x ∈ s → False
[PROOFSTEP]
simp [Finset.eq_empty_iff_forall_not_mem]
[GOAL]
case cons
α : 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 α
⊢ (∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
constructor
[GOAL]
case cons.mp
α : 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 α
⊢ (∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
rintro ⟨a, h, h'⟩ x hx
[GOAL]
case cons.mp.intro.intro
α : 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
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
cases' h' with _ h' a b
[GOAL]
case cons.mp.intro.intro.inl
α : 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
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
right
[GOAL]
case cons.mp.intro.intro.inl.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
⊢ x ∈ tail✝
[PROOFSTEP]
apply h
[GOAL]
case cons.mp.intro.intro.inl.h.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
⊢ x ∈ a
[PROOFSTEP]
subst a
[GOAL]
case cons.mp.intro.intro.inl.h.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✝
⊢ x ∈ s
[PROOFSTEP]
exact hx
[GOAL]
case cons.mp.intro.intro.inr
α : 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
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
simp only [h', mem_union, mem_singleton] at hx ⊢
[GOAL]
case cons.mp.intro.intro.inr
α : 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
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
cases' hx with hx hx'
[GOAL]
case cons.mp.intro.intro.inr.inl
α : 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 = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
exact Or.inl hx
[GOAL]
case cons.mp.intro.intro.inr.inr
α : 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
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
exact Or.inr (h _ hx')
[GOAL]
case cons.mpr
α : 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 : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
[PROOFSTEP]
intro h
[GOAL]
case cons.mpr
α : 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✝
⊢ ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
[PROOFSTEP]
exists s \ ({ xs_hd } : Finset α)
[GOAL]
case cons.mpr
α : 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✝
⊢ (∀ (x : α), x ∈ s \ {xs_hd} → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
[PROOFSTEP]
simp only [and_imp, mem_sdiff, mem_singleton]
[GOAL]
case cons.mpr
α : 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✝
⊢ (∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
[PROOFSTEP]
simp only [or_iff_not_imp_left] at h 
[GOAL]
case cons.mpr
α : 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✝
⊢ (∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
[PROOFSTEP]
exists h
[GOAL]
case cons.mpr
α : 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✝
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
by_cases h : xs_hd ∈ s
[GOAL]
case pos
α : 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
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
have : { xs_hd } ⊆ s
[GOAL]
case this
α : 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
⊢ {xs_hd} ⊆ s
case pos
α : 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
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
simp only [HasSubset.Subset, *, forall_eq, mem_singleton]
[GOAL]
case pos
α : 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
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
simp only [union_sdiff_of_subset this, or_true_iff, Finset.union_sdiff_of_subset, eq_self_iff_true]
[GOAL]
case neg
α : 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
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
left
[GOAL]
case neg.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✝
h : ¬xs_hd ∈ s
⊢ s = s \ {xs_hd}
[PROOFSTEP]
symm
[GOAL]
case neg.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✝
h : ¬xs_hd ∈ s
⊢ s \ {xs_hd} = s
[PROOFSTEP]
simp only [sdiff_eq_self]
[GOAL]
case neg.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✝
h : ¬xs_hd ∈ s
⊢ s ∩ {xs_hd} ⊆ ∅
[PROOFSTEP]
intro a
[GOAL]
case neg.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✝
h : ¬xs_hd ∈ s
a : α
⊢ a ∈ s ∩ {xs_hd} → a ∈ ∅
[PROOFSTEP]
simp only [and_imp, mem_inter, mem_singleton]
[GOAL]
case neg.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✝
h : ¬xs_hd ∈ s
a : α
⊢ a ∈ s → a = xs_hd → a ∈ ∅
[PROOFSTEP]
rintro h₀ rfl
[GOAL]
case neg.h
α : 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
⊢ a ∈ ∅
[PROOFSTEP]
exact (h h₀).elim
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ ∀ (x : Finset α), x ∈ enum (toList α)
[PROOFSTEP]
intro
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x✝ : Finset α
⊢ x✝ ∈ enum (toList α)
[PROOFSTEP]
simp
[GOAL]
α : 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 α)
[PROOFSTEP]
rintro ⟨x, h⟩
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
x : α
h : p x
⊢ { val := x, property := h } ∈
    List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α)
[PROOFSTEP]
simp
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
x : α
h : p x
⊢ ∃ a, (if h : p a then some { val := a, property := h } else none) = some { val := x, property := h }
[PROOFSTEP]
exists x
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
x : α
h : p x
⊢ (if h : p x then some { val := x, property := h } else none) = some { val := x, property := h }
[PROOFSTEP]
simp [*]
[GOAL]
α : 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))
[PROOFSTEP]
intro x
[GOAL]
α : 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))
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a))
[PROOFSTEP]
simp
[GOAL]
α✝ : 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))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ a, β a
⊢ ∀ (x : (a : α) ×' β a), x ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }]
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ a, β a
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }]
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ ∀ (x : α), x ∈ map (Equiv.toEmbedding equiv.symm) univ
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x✝ : α
⊢ x✝ ∈ map (Equiv.toEmbedding equiv.symm) univ
[PROOFSTEP]
simp
[GOAL]
α : 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 = β b
[PROOFSTEP]
rw [h']
[GOAL]
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f : (a : α) → a ∈ xs → β a
⊢ f ∈ pi xs fun x => toList (β x)
[PROOFSTEP]
induction' xs with xs_hd xs_tl xs_ih
[GOAL]
case nil
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
f : (a : α) → a ∈ [] → β a
⊢ f ∈ pi [] fun x => toList (β x)
[PROOFSTEP]
simp [pi, -List.map_eq_map, monad_norm, functor_norm]
[GOAL]
case cons
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ f ∈ pi (xs_hd :: xs_tl) fun x => toList (β x)
[PROOFSTEP]
simp [pi, -List.map_eq_map, monad_norm, functor_norm]
[GOAL]
case nil
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
f : (a : α) → a ∈ [] → β a
⊢ f = fun x h => False.elim (_ : False)
[PROOFSTEP]
ext a ⟨⟩
[GOAL]
case cons
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ ∃ a, (∃ a_1, a = Pi.cons xs_hd xs_tl a_1) ∧ ∃ a_1, (a_1 ∈ pi xs_tl fun x => toList (β x)) ∧ f = a a_1
[PROOFSTEP]
exists Pi.cons xs_hd xs_tl (f _ (List.mem_cons_self _ _))
[GOAL]
case cons
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ (∃ a, Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) = Pi.cons xs_hd xs_tl a) ∧
    ∃ a, (a ∈ pi xs_tl fun x => toList (β x)) ∧ f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) a
[PROOFSTEP]
constructor
[GOAL]
case cons.left
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ ∃ a, Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) = Pi.cons xs_hd xs_tl a
case cons.right
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ ∃ a, (a ∈ pi xs_tl fun x => toList (β x)) ∧ f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) a
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
case cons.right
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ ∃ a, (a ∈ pi xs_tl fun x => toList (β x)) ∧ f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) a
[PROOFSTEP]
exists Pi.tail f
[GOAL]
case cons.right
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ (Pi.tail f ∈ pi xs_tl fun x => toList (β x)) ∧
    f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) (Pi.tail f)
[PROOFSTEP]
constructor
[GOAL]
case cons.right.left
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ Pi.tail f ∈ pi xs_tl fun x => toList (β x)
[PROOFSTEP]
apply xs_ih
[GOAL]
case cons.right.right
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) (Pi.tail f)
[PROOFSTEP]
ext x h
[GOAL]
case cons.right.right.h.h
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
x : α
h : x ∈ xs_hd :: xs_tl
⊢ f x h = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) (Pi.tail f) x h
[PROOFSTEP]
simp [Pi.cons]
[GOAL]
case cons.right.right.h.h
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
x : α
h : x ∈ xs_hd :: xs_tl
⊢ f x h =
    if h' : x = xs_hd then cast (_ : β xs_hd = β x) (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl))
    else Pi.tail f x (_ : x ∈ xs_tl)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
x : α
h : x ∈ xs_hd :: xs_tl
h✝ : x = xs_hd
⊢ f x h = cast (_ : β xs_hd = β x) (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl))
[PROOFSTEP]
subst x
[GOAL]
case pos
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
h : xs_hd ∈ xs_hd :: xs_tl
⊢ f xs_hd h = cast (_ : β xs_hd = β xs_hd) (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl))
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
x : α
h : x ∈ xs_hd :: xs_tl
h✝ : ¬x = xs_hd
⊢ f x h = Pi.tail f x (_ : x ∈ xs_tl)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β✝ : α → Type v
β : α → Type (max u v)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ f ∈ enum β
[PROOFSTEP]
simp [pi.enum]
[GOAL]
α : Type u
β✝ : α → Type v
β : α → Type (max u v)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ ∃ a, (a ∈ pi (toList α) fun x => toList (β x)) ∧ (fun x => a x (_ : x ∈ toList α)) = f
[PROOFSTEP]
refine' ⟨fun a _ => f a, mem_pi _ _, rfl⟩
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
⊢ ∀ (x : (hp : p) → α hp), x ∈ List.map (fun x x_1 => x) (toList (α hp))
[PROOFSTEP]
intro x
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ x ∈ List.map (fun x x_1 => x) (toList (α hp))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ ∃ a, (fun x => a) = x
[PROOFSTEP]
exact ⟨x hp, rfl⟩
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
⊢ ∀ (x : (hp : p) → α hp), x ∈ [fun hp' => False.elim (_ : False)]
[PROOFSTEP]
intro
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
x✝ : (hp : p) → α hp
⊢ x✝ ∈ [fun hp' => False.elim (_ : False)]
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
x✝ : (hp : p) → α hp
⊢ x✝ = fun hp' => False.elim (_ : False)
[PROOFSTEP]
ext hp'
[GOAL]
case h
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
x✝ : (hp : p) → α hp
hp' : p
⊢ x✝ hp' = False.elim (_ : False)
[PROOFSTEP]
cases hp hp'
