-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_flatten {l : Array (Array α)} :
    l.flatten.toList = (l.toList.map toList).flatten

Proof state:
α : Type u_1
l : Array (Array α)
⊢ l.flatten.toList = (List.map toList l.toList).flatten

Tactic:
dsimp [flatten]

Result:
α : Type u_1
l : Array (Array α)
⊢ (foldl (fun r a => r ++ a) #[] l).toList = (List.map toList l.toList).flatten

Proof state:
case refine_4
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
this : ∀ (a : Array α), (List.foldl ?refine_1 a l).toList = a.toList ++ ?refine_2
⊢ (List.foldl (fun r a => r ++ a) #[] l).toList = (List.map toList l).flatten

case refine_1
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
a : Array α
⊢ Array α → Array α → Array α

case refine_2
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
a : Array α
⊢ List α

case refine_3
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
⊢ ∀ (a : Array α), (List.foldl ?refine_1 a l).toList = a.toList ++ ?refine_2

Tactic:
exact this #[]

Result:
case refine_3
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
⊢ ∀ (a : Array α), (List.foldl (fun r a => r ++ a) a l).toList = a.toList ++ (List.map toList l).flatten

Proof state:
case refine_3.nil
α : Type u_1
l : Array (Array α)
⊢ ∀ (a : Array α), (List.foldl (fun r a => r ++ a) a []).toList = a.toList ++ (List.map toList []).flatten

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : Array (Array α)
⊢ (foldl (fun r a => r ++ a) #[] l).toList = (List.map toList l.toList).flatten

Tactic:
simp only [← foldl_toList]

Result:
α : Type u_1
l : Array (Array α)
⊢ (List.foldl (fun r a => r ++ a) #[] l.toList).toList = (List.map toList l.toList).flatten

Proof state:
case refine_3.cons
α : Type u_1
l : Array (Array α)
h : Array α
tail✝ : List (Array α)
tail_ih✝ :
  ∀ (a : Array α), (List.foldl (fun r a => r ++ a) a tail✝).toList = a.toList ++ (List.map toList tail✝).flatten
⊢ ∀ (a : Array α),
    (List.foldl (fun r a => r ++ a) a (h :: tail✝)).toList = a.toList ++ (List.map toList (h :: tail✝)).flatten

Tactic:
induction h.toList <;> simp [*]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
⊢ ∀ (a : Array α), (List.foldl (fun r a => r ++ a) a l).toList = a.toList ++ (List.map toList l).flatten

Tactic:
induction l with
| nil => simp
| cons h => induction h.toList <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
⊢ (List.foldl (fun r a => r ++ a) #[] l).toList = (List.map toList l).flatten

Tactic:
have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_

Result:
case refine_4
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
this : ∀ (a : Array α), (List.foldl ?refine_1 a l).toList = a.toList ++ ?refine_2
⊢ (List.foldl (fun r a => r ++ a) #[] l).toList = (List.map toList l).flatten

case refine_1
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
a : Array α
⊢ Array α → Array α → Array α

case refine_2
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
a : Array α
⊢ List α

case refine_3
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
⊢ ∀ (a : Array α), (List.foldl ?refine_1 a l).toList = a.toList ++ ?refine_2

Proof state:
α : Type u_1
l : Array (Array α)
⊢ (List.foldl (fun r a => r ++ a) #[] l.toList).toList = (List.map toList l.toList).flatten

Tactic:
generalize l.toList = l

Result:
α : Type u_1
l✝ : Array (Array α)
l : List (Array α)
⊢ (List.foldl (fun r a => r ++ a) #[] l).toList = (List.map toList l).flatten