-- Mathlib/.lake/packages/batteries/Batteries/Data/List/ArrayMap.lean
theorem toArrayMap_toList (l : List α) (f : α → β ) : (l.toArrayMap f).toList = l.map f

Proof state:
case cons
α : Type u
β : Type v
f : α → β
head : α
tail : List α
tail_ih : ∀ (arr : Array β), (foldl (fun acc x => acc.push (f x)) arr tail).toList = arr.toList ++ map f tail
arr : Array β
this : arr.toList ++ f head :: map f tail = (arr.push (f head)).toList ++ map f tail
⊢ (foldl (fun acc x => acc.push (f x)) arr (head :: tail)).toList = arr.toList ++ map f (head :: tail)

Tactic:
rw [List.foldl_cons, List.map_cons, this, ← tail_ih]

Result:
no goals

Proof state:
α : Type u
β : Type v
l : List α
f : α → β
⊢ (l.toArrayMap f).toList = map f l

Tactic:
suffices ∀ arr : Array β, (l.foldl (init := arr) fun acc x => acc.push (f x)).toList
    = arr.toList ++ l.map f from
  this #[]

Result:
α : Type u
β : Type v
l : List α
f : α → β
⊢ ∀ (arr : Array β), (foldl (fun acc x => acc.push (f x)) arr l).toList = arr.toList ++ map f l

Proof state:
case cons
α : Type u
β : Type v
f : α → β
head : α
tail : List α
tail_ih : ∀ (arr : Array β), (foldl (fun acc x => acc.push (f x)) arr tail).toList = arr.toList ++ map f tail
⊢ ∀ (arr : Array β),
    (foldl (fun acc x => acc.push (f x)) arr (head :: tail)).toList = arr.toList ++ map f (head :: tail)

Tactic:
intro arr

Result:
case cons
α : Type u
β : Type v
f : α → β
head : α
tail : List α
tail_ih : ∀ (arr : Array β), (foldl (fun acc x => acc.push (f x)) arr tail).toList = arr.toList ++ map f tail
arr : Array β
⊢ (foldl (fun acc x => acc.push (f x)) arr (head :: tail)).toList = arr.toList ++ map f (head :: tail)

Proof state:
case cons
α : Type u
β : Type v
f : α → β
head : α
tail : List α
tail_ih : ∀ (arr : Array β), (foldl (fun acc x => acc.push (f x)) arr tail).toList = arr.toList ++ map f tail
arr : Array β
⊢ (foldl (fun acc x => acc.push (f x)) arr (head :: tail)).toList = arr.toList ++ map f (head :: tail)

Tactic:
have : arr.toList ++ f head :: map f tail = (arr.push (f head)).toList ++ map f tail := by simp

Result:
case cons
α : Type u
β : Type v
f : α → β
head : α
tail : List α
tail_ih : ∀ (arr : Array β), (foldl (fun acc x => acc.push (f x)) arr tail).toList = arr.toList ++ map f tail
arr : Array β
this : arr.toList ++ f head :: map f tail = (arr.push (f head)).toList ++ map f tail
⊢ (foldl (fun acc x => acc.push (f x)) arr (head :: tail)).toList = arr.toList ++ map f (head :: tail)

Proof state:
α : Type u
β : Type v
f : α → β
head : α
tail : List α
tail_ih : ∀ (arr : Array β), (foldl (fun acc x => acc.push (f x)) arr tail).toList = arr.toList ++ map f tail
arr : Array β
⊢ arr.toList ++ f head :: map f tail = (arr.push (f head)).toList ++ map f tail

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
f : α → β
⊢ ∀ (arr : Array β), (foldl (fun acc x => acc.push (f x)) arr []).toList = arr.toList ++ map f []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
l : List α
f : α → β
⊢ ∀ (arr : Array β), (foldl (fun acc x => acc.push (f x)) arr l).toList = arr.toList ++ map f l

Tactic:
induction l with
| nil => simp
| cons head tail tail_ih =>
  intro arr
  have : arr.toList ++ f head :: map f tail = (arr.push (f head)).toList ++ map f tail := by simp
  rw [List.foldl_cons, List.map_cons, this, ← tail_ih]

Result:
no goals