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

State before:
n m : ℕ
ix : TensorIndex2D n m
⊢ TensorIndex2D.transpose (TensorIndex2D.transpose ix) = ix
Tactic:
cases ix
State after:
case mk
n m ix0✝ ix1✝ : ℕ
IX0✝ : ix0✝ < n
IX1✝ : ix1✝ < m
⊢ TensorIndex2D.transpose (TensorIndex2D.transpose { ix0 := ix0✝, ix1 := ix1✝, IX0 := IX0✝, IX1 := IX1✝ }) =
    { ix0 := ix0✝, ix1 := ix1✝, IX0 := IX0✝, IX1 := IX1✝ }

State before:
n m ix0 ix1 : ℕ
IX0 : ix0 < n
IX1 : ix1 < m
⊢ TensorIndex2D.transpose (TensorIndex2D.transpose { ix0 := ix0, ix1 := ix1, IX0 := IX0, IX1 := IX1 }) =
    { ix0 := ix0, ix1 := ix1, IX0 := IX0, IX1 := IX1 }
Tactic:
case mk ix0 ix1 IX0 IX1 => {
  simp[TensorIndex2D.transpose];
}
State after:
no goals

State before:
n m ix0 ix1 : ℕ
IX0 : ix0 < n
IX1 : ix1 < m
⊢ TensorIndex2D.transpose (TensorIndex2D.transpose { ix0 := ix0, ix1 := ix1, IX0 := IX0, IX1 := IX1 }) =
    { ix0 := ix0, ix1 := ix1, IX0 := IX0, IX1 := IX1 }
Tactic:
simp[TensorIndex2D.transpose]
State after:
no goals