private def bufferLines (buf : ViE.FileBuffer) : Array String := Id.run do
  let mut lines : Array String := #[]
  for i in [0:buf.lineCount] do
    lines := lines.push ((ViE.getLineFromBuffer buf ⟨i⟩).getD "")
  return lines

private def bufferLines (buf : ViE.FileBuffer) : Array String :=
  -- Building all lines via repeated getLineRange is costly (O(lines * tree walk)).
  -- Convert once and split to avoid hammering findNthNewlineLeafCore.
  let lines := (buf.table.toString.splitOn "\n").toArray
  if lines.size == buf.lineCount then
    lines
  else if lines.size < buf.lineCount then
    lines ++ Array.replicate (buf.lineCount - lines.size) ""
  else
    lines.extract 0 buf.lineCount

theorem validNodeArity_mkInternal_root_of_eq
    (children : Array ViE.PieceTree)
    (vc : Array ViE.PieceTree) (s : ViE.Stats) (sm : ViE.SearchBloom) (im : ViE.InternalMeta)
    (heq : ViE.PieceTree.mkInternal children = ViE.PieceTree.internal vc s sm im)
    (hsize : 1 ≤ vc.size ∧ vc.size ≤ ViE.NodeCapacity)
    (hchildren : ViE.PieceTree.validNodeArityList vc.toList) :
    ViE.PieceTree.validNodeArity (ViE.PieceTree.mkInternal children) true := by
  rw [heq]
  simp [ViE.PieceTree.validNodeArity, hsize, hchildren]
theorem validNodeArity_mkInternal_nonroot_of_eq
    (children : Array ViE.PieceTree)
    (vc : Array ViE.PieceTree) (s : ViE.Stats) (sm : ViE.SearchBloom) (im : ViE.InternalMeta)
    (heq : ViE.PieceTree.mkInternal children = ViE.PieceTree.internal vc s sm im)
    (hsize : 2 ≤ vc.size ∧ vc.size ≤ ViE.NodeCapacity)
    (hchildren : ViE.PieceTree.validNodeArityList vc.toList) :
    ViE.PieceTree.validNodeArity (ViE.PieceTree.mkInternal children) false := by
  rw [heq]
  simp [ViE.PieceTree.validNodeArity, hsize, hchildren]