diff --git a/TensorLib/ByteArray.lean b/TensorLib/ByteArray.lean
index b786d9c..76d37c5 100644
--- a/TensorLib/ByteArray.lean
+++ b/TensorLib/ByteArray.lean
@@ -14,6 +14,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 -/
 
+import Batteries.Data.ByteArray
 import Plausible
 import TensorLib.Bytes
 import TensorLib.Common
@@ -169,9 +170,6 @@ def _root_.ByteArray.replicate (n : Nat) (v : UInt8) : ByteArray := Id.run do
 
 #guard ByteArray.replicate 5 7 == ⟨ #[7, 7, 7, 7, 7] ⟩
 
-@[simp] theorem _root_.ByteArray.size_push (a : ByteArray) (b : UInt8) : (a.push b).size = a.size + 1 :=
-  Array.size_push ..
-
 private theorem _root_.ByteArray.replicateSizeAux (arr : ByteArray) (xs : List a) (v : UInt8) : (List.foldl (fun b _ => b.push v) arr xs).size = arr.size + xs.length := by
   revert arr
   induction xs <;> simp
diff --git a/TensorLib/Iterator.lean b/TensorLib/Iterator.lean
index a9ebb57..8dc9753 100644
--- a/TensorLib/Iterator.lean
+++ b/TensorLib/Iterator.lean
@@ -219,7 +219,7 @@ instance instPairCarry [inst1 : Iterator i1 v1] [inst2 : Iterator i2 v2] : Itera
     | .some l => some (l, r)
     | .none =>
       let l := inst1.reset l
-       match inst2.next r with
+      match inst2.next r with
       | .none => .none
       | .some r => .some (l, r)