Theorem: List.length_zip_flat_index (MLIR/Util/KDTensor.lean)

State before:
α : Type u_1
xs : List α
⊢ length (zipFlatIndex xs) = length xs
Tactic:
apply Eq.symm
State after:
case h
α : Type u_1
xs : List α
⊢ length xs = length (zipFlatIndex xs)

State before:
case h
α : Type u_1
xs : List α
⊢ length xs = length (zipFlatIndex xs)
Tactic:
apply zip_flat_index_go_length
State after:
no goals