-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_filter_eq_foldl (f : α → β) (p : α → Bool) (l : Array α) :
    map f (filter p l) = foldl (fun y x => bif p x then y.push (f x) else y) #[] l

Proof state:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : List α
⊢ (map f (filter p { toList := l })).toList =
    (foldl (fun y x => bif p x then y.push (f x) else y) #[] { toList := l }).toList

Tactic:
simp only [size_toArray, List.filter_toArray', List.map_toArray, List.foldl_toArray']

Result:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : List α
⊢ List.map f (List.filter p l) = (List.foldl (fun y x => bif p x then y.push (f x) else y) #[] l).toList

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : Array α
⊢ map f (filter p l) = foldl (fun y x => bif p x then y.push (f x) else y) #[] l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : List α
⊢ map f (filter p { toList := l }) = foldl (fun y x => bif p x then y.push (f x) else y) #[] { toList := l }

Proof state:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : List α
⊢ List.map f (List.filter p l.reverse.reverse) =
    (List.foldl (fun y x => bif p x then y.push (f x) else y) #[] l.reverse.reverse).toList

Tactic:
generalize l.reverse = l

Result:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l✝ l : List α
⊢ List.map f (List.filter p l.reverse) = (List.foldl (fun y x => bif p x then y.push (f x) else y) #[] l.reverse).toList

Proof state:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : List α
⊢ List.map f (List.filter p l) = (List.foldl (fun y x => bif p x then y.push (f x) else y) #[] l).toList

Tactic:
rw [← List.reverse_reverse l]

Result:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : List α
⊢ List.map f (List.filter p l.reverse.reverse) =
    (List.foldl (fun y x => bif p x then y.push (f x) else y) #[] l.reverse.reverse).toList

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : List α
⊢ map f (filter p { toList := l }) = foldl (fun y x => bif p x then y.push (f x) else y) #[] { toList := l }

Tactic:
apply ext'

Result:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : List α
⊢ (map f (filter p { toList := l })).toList =
    (foldl (fun y x => bif p x then y.push (f x) else y) #[] { toList := l }).toList

Proof state:
case mk.h.cons
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l✝ : List α
x : α
l : List α
ih : (List.map f (List.filter p l)).reverse = (List.foldr (fun x y => bif p x then y.push (f x) else y) #[] l).toList
⊢ (List.map f (List.filter p (x :: l))).reverse =
    (List.foldr (fun x y => bif p x then y.push (f x) else y) #[] (x :: l)).toList

Tactic:
simp only [List.filter_cons, List.foldr_cons]

Result:
case mk.h.cons
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l✝ : List α
x : α
l : List α
ih : (List.map f (List.filter p l)).reverse = (List.foldr (fun x y => bif p x then y.push (f x) else y) #[] l).toList
⊢ (List.map f (if p x = true then x :: List.filter p l else List.filter p l)).reverse =
    (bif p x then (List.foldr (fun x y => bif p x then y.push (f x) else y) #[] l).push (f x)
      else List.foldr (fun x y => bif p x then y.push (f x) else y) #[] l).toList

Proof state:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l✝ l : List α
⊢ List.map f (List.filter p l.reverse) = (List.foldl (fun y x => bif p x then y.push (f x) else y) #[] l.reverse).toList

Tactic:
simp only [List.filter_reverse, List.map_reverse, List.foldl_reverse]

Result:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l✝ l : List α
⊢ (List.map f (List.filter p l)).reverse = (List.foldr (fun x y => bif p x then y.push (f x) else y) #[] l).toList

Proof state:
case mk.h.cons
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l✝ : List α
x : α
l : List α
ih : (List.map f (List.filter p l)).reverse = (List.foldr (fun x y => bif p x then y.push (f x) else y) #[] l).toList
⊢ (List.map f (if p x = true then x :: List.filter p l else List.filter p l)).reverse =
    (bif p x then (List.foldr (fun x y => bif p x then y.push (f x) else y) #[] l).push (f x)
      else List.foldr (fun x y => bif p x then y.push (f x) else y) #[] l).toList

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case mk.h.nil
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l : List α
⊢ (List.map f (List.filter p [])).reverse = (List.foldr (fun x y => bif p x then y.push (f x) else y) #[] []).toList

Tactic:
rfl

Result:
no goals

Proof state:
case mk.h
α : Type u_1
β : Type u_2
f : α → β
p : α → Bool
l✝ l : List α
⊢ (List.map f (List.filter p l)).reverse = (List.foldr (fun x y => bif p x then y.push (f x) else y) #[] l).toList

Tactic:
induction l with
| nil => rfl
| cons x l ih =>
  simp only [List.filter_cons, List.foldr_cons]
  split <;> simp_all

Result:
no goals