no goals
ι : Type ?u.371648
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a b : α
l : List α
ain : a ∈ filter p (b :: l)
pb : p b = true
⊢ a ∈ b :: filter p l
simpa only [filter_cons_of_pos _ pb] using ain
ι : Type ?u.371648
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a b : α
l : List α
ain : a ∈ filter p (b :: l)
pb : p a = true
this : a ∈ b :: filter p l
h : a = b
⊢ p a = true
ι : Type ?u.371648
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a b : α
l : List α
ain : a ∈ filter p (b :: l)
pb : p b = true
this : a ∈ b :: filter p l
h : a = b
⊢ p a = true
rw [← h] at pb
no goals
ι : Type ?u.371648
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a b : α
l : List α
ain : a ∈ filter p (b :: l)
pb : p a = true
this : a ∈ b :: filter p l
h : a = b
⊢ p a = true
exact pb
ι : Type ?u.371648
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a b : α
l : List α
pb : ¬p b = true
ain : a ∈ filter p l
⊢ p a = true
ι : Type ?u.371648
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a b : α
l : List α
ain : a ∈ filter p (b :: l)
pb : ¬p b = true
⊢ p a = true
simp only [filter_cons_of_neg _ pb] at ain
no goals
ι : Type ?u.371648
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
a b : α
l : List α
pb : ¬p b = true
ain : a ∈ filter p l
⊢ p a = true
exact of_mem_filter ain