case inl
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a : α
l : List α
h1 : p a = true
h : a ∈ a :: l
⊢ a ∈ filter p (a :: l)

case inr
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a x : α
l : List α
h✝ : a ∈ x :: l
h1 : p a = true
h : a ∈ l
⊢ a ∈ filter p (x :: l)
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a x : α
l : List α
h : a ∈ x :: l
h1 : p a = true
⊢ a ∈ filter p (x :: l)
rcases mem_cons.1 h with rfl | h
case inr
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a x : α
l : List α
h✝ : a ∈ x :: l
h1 : p a = true
h : a ∈ l
⊢ a ∈ filter p (x :: l)
case inl
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a : α
l : List α
h1 : p a = true
h : a ∈ a :: l
⊢ a ∈ filter p (a :: l)

case inr
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a x : α
l : List α
h✝ : a ∈ x :: l
h1 : p a = true
h : a ∈ l
⊢ a ∈ filter p (x :: l)
. simp [filter, h1]
no goals
case inr
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a x : α
l : List α
h✝ : a ∈ x :: l
h1 : p a = true
h : a ∈ l
⊢ a ∈ filter p (x :: l)
. rw [filter]
  cases p x <;> simp [mem_filter_of_mem h h1]
no goals
case inl
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a : α
l : List α
h1 : p a = true
h : a ∈ a :: l
⊢ a ∈ filter p (a :: l)
simp [filter, h1]
case inr
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a x : α
l : List α
h✝ : a ∈ x :: l
h1 : p a = true
h : a ∈ l
⊢ a ∈
    match p x with
    | true => x :: filter p l
    | false => filter p l
case inr
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a x : α
l : List α
h✝ : a ∈ x :: l
h1 : p a = true
h : a ∈ l
⊢ a ∈ filter p (x :: l)
rw [filter]
no goals
case inr
ι : Type ?u.372560
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a x : α
l : List α
h✝ : a ∈ x :: l
h1 : p a = true
h : a ∈ l
⊢ a ∈
    match p x with
    | true => x :: filter p l
    | false => filter p l
cases p x <;> simp [mem_filter_of_mem h h1]