no goals
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
h : a ∈ as
⊢ elem a as = true
induction h with
| head _ => simp [elem]
| tail _ _ ih => simp [elem]; split; rfl; assumption
no goals
case head
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as as✝ : List α
⊢ elem a (a :: as✝) = true
simp [elem]
case tail
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
⊢ (match a == b✝ with
    | true => true
    | false => elem a as✝) =
    true
case tail
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
⊢ elem a (b✝ :: as✝) = true
simp [elem]
case tail.h_1
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = true
⊢ true = true

case tail.h_2
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = false
⊢ elem a as✝ = true
case tail
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
⊢ (match a == b✝ with
    | true => true
    | false => elem a as✝) =
    true
split
case tail.h_2
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = false
⊢ elem a as✝ = true
case tail.h_1
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = true
⊢ true = true

case tail.h_2
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = false
⊢ elem a as✝ = true
rfl
no goals
case tail.h_2
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = false
⊢ elem a as✝ = true
assumption