ι : Type ?u.380238
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p : α → Bool
l l' : List α
h : l ⊆ l'
x : α
hx : x ∈ filter p l
⊢ x ∈ filter p l'
ι : Type ?u.380238
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p : α → Bool
l l' : List α
h : l ⊆ l'
⊢ filter p l ⊆ filter p l'
intro x hx
ι : Type ?u.380238
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p : α → Bool
l l' : List α
h : l ⊆ l'
x : α
hx : x ∈ l ∧ p x = true
⊢ x ∈ l' ∧ p x = true
ι : Type ?u.380238
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p : α → Bool
l l' : List α
h : l ⊆ l'
x : α
hx : x ∈ filter p l
⊢ x ∈ filter p l'
rw [mem_filter] at hx⊢
no goals
ι : Type ?u.380238
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p : α → Bool
l l' : List α
h : l ⊆ l'
x : α
hx : x ∈ l ∧ p x = true
⊢ x ∈ l' ∧ p x = true
exact ⟨h hx.left, hx.right⟩