Theorem: reshape_self (MLIR/Dialects/BuiltinModel.lean)

State before:
τ : MLIRTy
D : DimList
H₁ H₂ : known D = true
Hprod : prod D = prod D
t : RankedTensor D τ
⊢ reshape D H₁ H₂ Hprod t = t
Tactic:
simp [reshape, dim_known_project_eq H₁ t.h_refines]
State after:
no goals