Theorem: Test.all_deforestation (Evaluation/FunctionalProgramming.lean)

State before:
α : Sort u_1
⊢ ∀ (p : α → Bool) (xs : List α), all p xs = all' p xs
Tactic:
intros p xs
State after:
α : Sort u_1
p : α → Bool
xs : List α
⊢ all p xs = all' p xs

State before:
α : Sort u_1
p : α → Bool
xs : List α
⊢ all p xs = all' p xs
Tactic:
induction xs with
| nil => simp [all, all', List.foldr, List.map]
| cons a as ih => simp [all, all', List.foldr, List.map, ih]
State after:
no goals

State before:
case nil
α : Sort u_1
p : α → Bool
⊢ all p [] = all' p []
Tactic:
simp [all, all', List.foldr, List.map]
State after:
no goals

State before:
case cons
α : Sort u_1
p : α → Bool
a : α
as : List α
ih : all p as = all' p as
⊢ all p (a::as) = all' p (a::as)
Tactic:
simp [all, all', List.foldr, List.map, ih]
State after:
case cons
α : Sort u_1
p : α → Bool
a : α
as : List α
ih : all p as = all' p as
⊢ (p a && List.foldr and true (List.map p as)) = (p a && all' p as)