case cons
ι : Type ?u.369991
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ = foldr (fun a out => bif p a then a :: out else out) [] tail✝
⊢ (match p head✝ with
    | true => head✝ :: foldr (fun a out => bif p a then a :: out else out) [] tail✝
    | false => foldr (fun a out => bif p a then a :: out else out) [] tail✝) =
    bif p head✝ then head✝ :: foldr (fun a out => bif p a then a :: out else out) [] tail✝
    else foldr (fun a out => bif p a then a :: out else out) [] tail✝
ι : Type ?u.369991
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p : α → Bool
l : List α
⊢ filter p l = foldr (fun a out => bif p a then a :: out else out) [] l
induction l <;> simp [*, filter]
no goals
case cons
ι : Type ?u.369991
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ = foldr (fun a out => bif p a then a :: out else out) [] tail✝
⊢ (match p head✝ with
    | true => head✝ :: foldr (fun a out => bif p a then a :: out else out) [] tail✝
    | false => foldr (fun a out => bif p a then a :: out else out) [] tail✝) =
    bif p head✝ then head✝ :: foldr (fun a out => bif p a then a :: out else out) [] tail✝
    else foldr (fun a out => bif p a then a :: out else out) [] tail✝
rfl