-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatten_append (L₁ : Vector (Vector α n) m₁) (L₂ : Vector (Vector α n) m₂) :
    flatten (L₁ ++ L₂) = (flatten L₁ ++ flatten L₂).cast (by simp [Nat.add_mul])

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

Tactic:
simp

Result:
no goals

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

Tactic:
induction L₂ using vector₂_induction

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

Proof state:
α : Type ?u.298205
n m₁ m₂ : Nat
L₁ : Vector (Vector α n) m₁
L₂ : Vector (Vector α n) m₂
⊢ m₁ * n + m₂ * n = (m₁ + m₂) * n

Tactic:
simp [Nat.add_mul]

Result:
no goals

Proof state:
α : Type u_1
n m₁ m₂ : Nat
L₁ : Vector (Vector α n) m₁
L₂ : Vector (Vector α n) m₂
⊢ (L₁ ++ L₂).flatten = Vector.cast ⋯ (L₁.flatten ++ L₂.flatten)

Tactic:
induction L₁ using vector₂_induction

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