Theorem: Tensor.map_shape (MLIR/Dialects/BuiltinModel.lean)

State before:
σ τ : MLIRTy
v : Tensor σ
f : MLIRType.eval σ → MLIRType.eval τ
⊢ v.shape = (map v f).shape
Tactic:
simp [Tensor.map]
State after:
no goals