. rw [←dim_known_project_eq _ t.h_refines] <;> simp
case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ [α, n] = t.toTensor.shape

case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ List.remap
      (List.remap t.toTensor.data (transpose_remap α n)
        (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
      (transpose_remap n α)
      (_ :
        ∀ (n_1 : ℕ),
          n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
            transpose_remap n α n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ),
                      i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))) =
    t.toTensor.data
case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ List.remap
      (List.remap t.toTensor.data (transpose_remap α n)
        (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
      (transpose_remap n α)
      (_ :
        ∀ (n_1 : ℕ),
          n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
            transpose_remap n α n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ),
                      i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))) =
    t.toTensor.data