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

Proof state:
α : Type ?u.303784
n m : Nat
L : Vector (Vector α n) m
l : Vector α n
⊢ m * n + n = (m + 1) * n

Tactic:
simp [Nat.add_mul]

Result:
no goals

Proof state:
case of
α : Type u_1
n m : Nat
l : Vector α 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 := ⋯ }.push
        l).flatten =
    Vector.cast ⋯
      ({
            toArray :=
              Array.map
                (fun x =>
                  match x with
                  | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
                xss✝.attach,
            size_toArray := ⋯ }.flatten ++
        l)

Tactic:
rcases l with ⟨l⟩

Result:
case of.mk
α : Type u_1
n m : Nat
xss✝ : Array (Array α)
h₁✝ : xss✝.size = m
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = n
l : Array α
size_toArray✝ : l.size = n
⊢ ({
            toArray :=
              Array.map
                (fun x =>
                  match x with
                  | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
                xss✝.attach,
            size_toArray := ⋯ }.push
        { toArray := l, size_toArray := 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 := l, size_toArray := size_toArray✝ })

Proof state:
case of.mk
α : Type u_1
n m : Nat
xss✝ : Array (Array α)
h₁✝ : xss✝.size = m
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = n
l : Array α
size_toArray✝ : l.size = n
⊢ ({
            toArray :=
              Array.map
                (fun x =>
                  match x with
                  | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
                xss✝.attach,
            size_toArray := ⋯ }.push
        { toArray := l, size_toArray := 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 := l, size_toArray := size_toArray✝ })

Tactic:
simp [Array.flatten_push]

Result:
no goals

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

Tactic:
induction L using vector₂_induction

Result:
case of
α : Type u_1
n m : Nat
l : Vector α 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 := ⋯ }.push
        l).flatten =
    Vector.cast ⋯
      ({
            toArray :=
              Array.map
                (fun x =>
                  match x with
                  | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
                xss✝.attach,
            size_toArray := ⋯ }.flatten ++
        l)