-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_eq_foldl (f : α → Array β) (l : Array α) :
    l.flatMap f = l.foldl (fun acc a => acc ++ f a) #[]

Proof state:
case mk.cons
α : Type u_1
β : Type u_2
f : α → Array β
a : α
l : List α
ih :
  ∀ (l' : List β),
    (List.foldl (fun acc a => acc ++ (f a).toList) l' l).toArray = List.foldl (fun acc a => acc ++ f a) l'.toArray l
l' : List β
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) l' (a :: l)).toArray =
    List.foldl (fun acc a => acc ++ f a) l'.toArray (a :: l)

Tactic:
simp [ih ((l' ++ (f a).toList)), toArray_append]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ ∀ (l' : List β),
    (List.foldl (fun acc a => acc ++ (f a).toList) l' l).toArray = List.foldl (fun acc a => acc ++ f a) l'.toArray l

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  intro l'
  simp [ih ((l' ++ (f a).toList)), toArray_append]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
l : Array α
⊢ flatMap f l = foldl (fun acc a => acc ++ f a) #[] l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ flatMap f { toList := l } = foldl (fun acc a => acc ++ f a) #[] { toList := l }

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ flatMap f { toList := l } = foldl (fun acc a => acc ++ f a) #[] { toList := l }

Tactic:
simp only [List.flatMap_toArray, List.flatMap_eq_foldl, size_toArray, List.foldl_toArray']

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) [] l).toArray = List.foldl (fun acc a => acc ++ f a) #[] l

Proof state:
case mk.cons
α : Type u_1
β : Type u_2
f : α → Array β
a : α
l : List α
ih :
  ∀ (l' : List β),
    (List.foldl (fun acc a => acc ++ (f a).toList) l' l).toArray = List.foldl (fun acc a => acc ++ f a) l'.toArray l
⊢ ∀ (l' : List β),
    (List.foldl (fun acc a => acc ++ (f a).toList) l' (a :: l)).toArray =
      List.foldl (fun acc a => acc ++ f a) l'.toArray (a :: l)

Tactic:
intro l'

Result:
case mk.cons
α : Type u_1
β : Type u_2
f : α → Array β
a : α
l : List α
ih :
  ∀ (l' : List β),
    (List.foldl (fun acc a => acc ++ (f a).toList) l' l).toArray = List.foldl (fun acc a => acc ++ f a) l'.toArray l
l' : List β
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) l' (a :: l)).toArray =
    List.foldl (fun acc a => acc ++ f a) l'.toArray (a :: l)

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) [] l).toArray = List.foldl (fun acc a => acc ++ f a) #[] l

Tactic:
suffices ∀ l', (List.foldl (fun acc a => acc ++ (f a).toList) l' l).toArray =
    List.foldl (fun acc a => acc ++ f a) l'.toArray l by
  simpa using this []

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ ∀ (l' : List β),
    (List.foldl (fun acc a => acc ++ (f a).toList) l' l).toArray = List.foldl (fun acc a => acc ++ f a) l'.toArray l

Proof state:
case mk.nil
α : Type u_1
β : Type u_2
f : α → Array β
⊢ ∀ (l' : List β),
    (List.foldl (fun acc a => acc ++ (f a).toList) l' []).toArray = List.foldl (fun acc a => acc ++ f a) l'.toArray []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
this :
  ∀ (l' : List β),
    (List.foldl (fun acc a => acc ++ (f a).toList) l' l).toArray = List.foldl (fun acc a => acc ++ f a) l'.toArray l
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) [] l).toArray = List.foldl (fun acc a => acc ++ f a) #[] l

Tactic:
simpa using this []

Result:
no goals