no goals
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
⊢ elem a as = true → a ∈ as
match as with
| [] => simp [elem]
| a'::as =>
  simp [elem]
  split
  next h => intros; simp [BEq.beq] at h; subst h; apply Mem.head
  next _ => intro h; exact Mem.tail _ (mem_of_elem_eq_true h)
no goals
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as : List α
⊢ elem a nil = true → a ∈ nil
simp [elem]
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
⊢ (match a == a' with
      | true => true
      | false => elem a as) =
      true →
    a ∈ a' :: as
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
⊢ elem a (a' :: as) = true → a ∈ a' :: as
simp [elem]
case h_1
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = true
⊢ true = true → a ∈ a' :: as

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

case h_2
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
⊢ elem a as = true → a ∈ a' :: as
next h => intros; simp [BEq.beq] at h; subst h; apply Mem.head
no goals
case h_2
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
⊢ elem a as = true → a ∈ a' :: as
next _ => intro h; exact Mem.tail _ (mem_of_elem_eq_true h)
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
h : (a == a') = true
a✝ : true = true
⊢ a ∈ a' :: as
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
h : (a == a') = true
⊢ true = true → a ∈ a' :: as
intros
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
a✝ : true = true
h : a = a'
⊢ a ∈ a' :: as
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
h : (a == a') = true
a✝ : true = true
⊢ a ∈ a' :: as
simp [BEq.beq] at h
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ as : List α
x✝ : Bool
a✝ : true = true
⊢ a ∈ a :: as
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
a✝ : true = true
h : a = a'
⊢ a ∈ a' :: as
subst h
no goals
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ as : List α
x✝ : Bool
a✝ : true = true
⊢ a ∈ a :: as
apply Mem.head
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
h : elem a as = true
⊢ a ∈ a' :: as
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
⊢ elem a as = true → a ∈ a' :: as
intro h
no goals
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
h : elem a as = true
⊢ a ∈ a' :: as
exact Mem.tail _ (mem_of_elem_eq_true h)