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)

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
α : 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)
induction' xs with xs_hd xs_tl xs_ih <;> simp [pi, -List.map_eq_map, monad_norm, functor_norm]
no goals
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)
ext (a⟨⟩)
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
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
exists Pi.cons xs_hd xs_tl (f _ (List.mem_cons_self _ _))
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
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
constructor
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
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
exact ⟨_, rfl⟩
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)
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
exists Pi.tail f
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)

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)
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)
constructor
no goals
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)
apply xs_ih
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
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)
ext (x h)
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)
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
simp [Pi.cons]
case cons.right.right.h.h.inl
α : 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))

case cons.right.right.h.h.inr
α : 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)
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)
split_ifs
case cons.right.right.h.h.inl
α : 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))
case cons.right.right.h.h.inl
α : 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))
subst x
no goals
case cons.right.right.h.h.inl
α : 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))
rfl
no goals
case cons.right.right.h.h.inr
α : 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)
rfl