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

State before:
t : Tensor2D
⊢ Tensor2D.transpose (Tensor2D.transpose t) = t
Tactic:
cases t
State after:
case mk
size0✝ size1✝ : ℕ
data✝ : TensorIndex2D size0✝ size1✝ → ℤ
⊢ Tensor2D.transpose (Tensor2D.transpose { size0 := size0✝, size1 := size1✝, data := data✝ }) =
    { size0 := size0✝, size1 := size1✝, data := data✝ }

State before:
size0 size1 : ℕ
data : TensorIndex2D size0 size1 → ℤ
⊢ Tensor2D.transpose (Tensor2D.transpose { size0 := size0, size1 := size1, data := data }) =
    { size0 := size0, size1 := size1, data := data }
Tactic:
case mk size0 size1 data => {
 simp[Tensor2D.transpose];
 simp[transpose_index_twice_is_id];
}
State after:
no goals

State before:
size0 size1 : ℕ
data : TensorIndex2D size0 size1 → ℤ
⊢ Tensor2D.transpose (Tensor2D.transpose { size0 := size0, size1 := size1, data := data }) =
    { size0 := size0, size1 := size1, data := data }
Tactic:
simp[Tensor2D.transpose]
State after:
size0 size1 : ℕ
data : TensorIndex2D size0 size1 → ℤ
⊢ (fun ix => data (TensorIndex2D.transpose (TensorIndex2D.transpose ix))) = data

State before:
size0 size1 : ℕ
data : TensorIndex2D size0 size1 → ℤ
⊢ (fun ix => data (TensorIndex2D.transpose (TensorIndex2D.transpose ix))) = data
Tactic:
simp[transpose_index_twice_is_id]
State after:
no goals