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

Proof state:
case of
α : Type u_1
xss : List (List (List α))
⊢ (List.map (fun xs => List.map List.toArray xs) xss).flatten.toArray.flatten =
    (map flatten (List.map List.toArray (List.map (fun xs => List.map List.toArray xs) xss)).toArray).flatten

Tactic:
have : (xss.map (fun xs => xs.map List.toArray)).flatten = xss.flatten.map List.toArray := by
  induction xss with
  | nil => simp
  | cons xs xss ih =>
    simp only [List.map_cons, List.flatten_cons, ih, List.map_append]

Result:
case of
α : Type u_1
xss : List (List (List α))
this : (List.map (fun xs => List.map List.toArray xs) xss).flatten = List.map List.toArray xss.flatten
⊢ (List.map (fun xs => List.map List.toArray xs) xss).flatten.toArray.flatten =
    (map flatten (List.map List.toArray (List.map (fun xs => List.map List.toArray xs) xss)).toArray).flatten

Proof state:
case of
α : Type u_1
xss : List (List (List α))
this : (List.map (fun xs => List.map List.toArray xs) xss).flatten = List.map List.toArray xss.flatten
⊢ (List.map List.flatten xss).flatten.toArray = (map (fun x => x.flatten.toArray) xss.toArray).flatten

Tactic:
rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map]

Result:
no goals

Proof state:
case cons
α : Type u_1
xs : List (List α)
xss : List (List (List α))
ih : (List.map (fun xs => List.map List.toArray xs) xss).flatten = List.map List.toArray xss.flatten
⊢ (List.map (fun xs => List.map List.toArray xs) (xs :: xss)).flatten = List.map List.toArray (xs :: xss).flatten

Tactic:
simp only [List.map_cons, List.flatten_cons, ih, List.map_append]

Result:
no goals

Proof state:
α : Type u_1
L : Array (Array (Array α))
⊢ L.flatten.flatten = (map flatten L).flatten

Tactic:
induction L using array₃_induction with
| of xss =>
  rw [flatten_toArray_map]
  have : (xss.map (fun xs => xs.map List.toArray)).flatten = xss.flatten.map List.toArray := by
    induction xss with
    | nil => simp
    | cons xs xss ih =>
      simp only [List.map_cons, List.flatten_cons, ih, List.map_append]
  rw [this, flatten_toArray_map, List.flatten_flatten, ← List.map_toArray, Array.map_map,
    ← List.map_toArray, map_map, Function.comp_def]
  simp only [Function.comp_apply, flatten_toArray_map]
  rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map]

Result:
no goals

Proof state:
case of
α : Type u_1
xss : List (List (List α))
this : (List.map (fun xs => List.map List.toArray xs) xss).flatten = List.map List.toArray xss.flatten
⊢ (List.map (fun xs => List.map List.toArray xs) xss).flatten.toArray.flatten =
    (map flatten (List.map List.toArray (List.map (fun xs => List.map List.toArray xs) xss)).toArray).flatten

Tactic:
rw [this, flatten_toArray_map, List.flatten_flatten, ← List.map_toArray, Array.map_map,
  ← List.map_toArray, map_map, Function.comp_def]

Result:
case of
α : Type u_1
xss : List (List (List α))
this : (List.map (fun xs => List.map List.toArray xs) xss).flatten = List.map List.toArray xss.flatten
⊢ (List.map List.flatten xss).flatten.toArray =
    (map (fun x => (flatten ∘ List.toArray) (List.map List.toArray x)) xss.toArray).flatten

Proof state:
case nil
α : Type u_1
⊢ (List.map (fun xs => List.map List.toArray xs) []).flatten = List.map List.toArray [].flatten

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xss : List (List (List α))
⊢ (List.map (fun xs => List.map List.toArray xs) xss).flatten = List.map List.toArray xss.flatten

Tactic:
induction xss with
| nil => simp
| cons xs xss ih =>
  simp only [List.map_cons, List.flatten_cons, ih, List.map_append]

Result:
no goals

Proof state:
case of
α : Type u_1
xss : List (List (List α))
this : (List.map (fun xs => List.map List.toArray xs) xss).flatten = List.map List.toArray xss.flatten
⊢ (List.map List.flatten xss).flatten.toArray =
    (map (fun x => (flatten ∘ List.toArray) (List.map List.toArray x)) xss.toArray).flatten

Tactic:
simp only [Function.comp_apply, flatten_toArray_map]

Result:
case of
α : Type u_1
xss : List (List (List α))
this : (List.map (fun xs => List.map List.toArray xs) xss).flatten = List.map List.toArray xss.flatten
⊢ (List.map List.flatten xss).flatten.toArray = (map (fun x => x.flatten.toArray) xss.toArray).flatten

Proof state:
case of
α : Type u_1
xss : List (List (List α))
⊢ (List.map List.toArray (List.map (fun xs => List.map List.toArray xs) xss)).toArray.flatten.flatten =
    (map flatten (List.map List.toArray (List.map (fun xs => List.map List.toArray xs) xss)).toArray).flatten

Tactic:
rw [flatten_toArray_map]

Result:
case of
α : Type u_1
xss : List (List (List α))
⊢ (List.map (fun xs => List.map List.toArray xs) xss).flatten.toArray.flatten =
    (map flatten (List.map List.toArray (List.map (fun xs => List.map List.toArray xs) xss)).toArray).flatten