-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem unattach_flatten {p : α → Prop} {l : Vector (Vector { x // p x } n) n} :
    l.flatten.unattach = (l.map unattach).flatten

Proof state:
case of
α : Type u_1
n : Nat
p : α → Prop
xss✝ : Array (Array { x // p x })
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array { x // p x }), xs ∈ xss✝ → xs.size = n
⊢ (Array.map (Array.map fun x => x.val) xss✝).flatten = (Array.map (fun l => Array.map (fun x => x.val) l) xss✝).flatten

Tactic:
rfl

Result:
no goals

Proof state:
case of
α : Type u_1
n : Nat
p : α → Prop
xss✝ : Array (Array { x // p x })
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array { x // p x }), xs ∈ xss✝ → xs.size = n
⊢ map (fun x => x.val)
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten =
    (map (fun l => map (fun x => x.val) l)
        {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }).flatten

Tactic:
simp only [flatten_mk, Array.map_map, Function.comp_apply, Array.map_subtype,
  Array.unattach_attach, Array.map_id_fun', id_eq, map_mk, Array.map_flatten, map_subtype,
  map_id_fun', unattach_mk, eq_mk]

Result:
case of
α : Type u_1
n : Nat
p : α → Prop
xss✝ : Array (Array { x // p x })
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array { x // p x }), xs ∈ xss✝ → xs.size = n
⊢ (Array.map (Array.map fun x => x.val) xss✝).flatten = (Array.map Array.unattach xss✝).flatten

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector (Vector { x // p x } n) n
⊢ map (fun x => x.val) l.flatten = (map (fun l => map (fun x => x.val) l) l).flatten

Tactic:
cases l using vector₂_induction

Result:
case of
α : Type u_1
n : Nat
p : α → Prop
xss✝ : Array (Array { x // p x })
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array { x // p x }), xs ∈ xss✝ → xs.size = n
⊢ map (fun x => x.val)
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten =
    (map (fun l => map (fun x => x.val) l)
        {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }).flatten

Proof state:
case of
α : Type u_1
n : Nat
p : α → Prop
xss✝ : Array (Array { x // p x })
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array { x // p x }), xs ∈ xss✝ → xs.size = n
⊢ (Array.map (Array.map fun x => x.val) xss✝).flatten = (Array.map Array.unattach xss✝).flatten

Tactic:
unfold Array.unattach

Result:
case of
α : Type u_1
n : Nat
p : α → Prop
xss✝ : Array (Array { x // p x })
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array { x // p x }), xs ∈ xss✝ → xs.size = n
⊢ (Array.map (Array.map fun x => x.val) xss✝).flatten = (Array.map (fun l => Array.map (fun x => x.val) l) xss✝).flatten

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector (Vector { x // p x } n) n
⊢ l.flatten.unattach = (map unattach l).flatten

Tactic:
unfold unattach

Result:
α : Type u_1
n : Nat
p : α → Prop
l : Vector (Vector { x // p x } n) n
⊢ map (fun x => x.val) l.flatten = (map (fun l => map (fun x => x.val) l) l).flatten