Theorem: shapeProd_cons_prod (MLIR/Util/KDTensor.lean)

State before:
x y : ℕ
zs : List ℕ
⊢ shapeProd (x :: y :: zs) = shapeProd (x * y :: zs)
Tactic:
simp [Nat.mul_assoc]
State after:
no goals