case a.h
i j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) i j = ↑Matrix.of ![![1, 0], ![0, -1]] i j
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) = ↑Matrix.of ![![1, 0], ![0, -1]]
ext (i j)
no goals
case a.h
i j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) i j = ↑Matrix.of ![![1, 0], ![0, -1]] i j
fin_cases i <;> fin_cases j <;> simp [LinearMap.toMatrix_apply]