case nil
ι : Type ?u.136885
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
p : α → Bool
⊢ map f (filter p []) = foldr (fun a bs => bif p a then f a :: bs else bs) [] []

case cons
ι : Type ?u.136885
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
p : α → Bool
head : α
tail : List α
tail_ih✝ : map f (filter p tail) = foldr (fun a bs => bif p a then f a :: bs else bs) [] tail
⊢ map f (filter p (head :: tail)) = foldr (fun a bs => bif p a then f a :: bs else bs) [] (head :: tail)
ι : Type ?u.136885
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
p : α → Bool
as : List α
⊢ map f (filter p as) = foldr (fun a bs => bif p a then f a :: bs else bs) [] as
induction' as with head tail
no goals
case nil
ι : Type ?u.136885
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
p : α → Bool
⊢ map f (filter p []) = foldr (fun a bs => bif p a then f a :: bs else bs) [] []
rfl
case cons
ι : Type ?u.136885
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
p : α → Bool
head : α
tail : List α
tail_ih✝ : map f (filter p tail) = foldr (fun a bs => bif p a then f a :: bs else bs) [] tail
⊢ map f (filter p (head :: tail)) =
    bif p head then f head :: foldr (fun a bs => bif p a then f a :: bs else bs) [] tail
    else foldr (fun a bs => bif p a then f a :: bs else bs) [] tail
case cons
ι : Type ?u.136885
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
p : α → Bool
head : α
tail : List α
tail_ih✝ : map f (filter p tail) = foldr (fun a bs => bif p a then f a :: bs else bs) [] tail
⊢ map f (filter p (head :: tail)) = foldr (fun a bs => bif p a then f a :: bs else bs) [] (head :: tail)
simp only [foldr]
no goals
case cons
ι : Type ?u.136885
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
p : α → Bool
head : α
tail : List α
tail_ih✝ : map f (filter p tail) = foldr (fun a bs => bif p a then f a :: bs else bs) [] tail
⊢ map f (filter p (head :: tail)) =
    bif p head then f head :: foldr (fun a bs => bif p a then f a :: bs else bs) [] tail
    else foldr (fun a bs => bif p a then f a :: bs else bs) [] tail
cases hp : p head <;> simp [filter, *]