Theorem: shapeProd.cons_unfold (MLIR/Util/KDTensor.lean)

State before:
⊢ ∀ (x : ℕ) (xs : List ℕ), shapeProd (x :: xs) = x * shapeProd xs
Tactic:
intros x xs
State after:
x : ℕ
xs : List ℕ
⊢ shapeProd (x :: xs) = x * shapeProd xs

State before:
x : ℕ
xs : List ℕ
⊢ shapeProd (x :: xs) = x * shapeProd xs
Tactic:
simp [shapeProd, List.foldr]
State after:
no goals