[GOAL]
z : ℂ
⊢ ↑(leftMulMatrix basisOneI) z = ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
z : ℂ
i j : Fin 2
⊢ ↑(leftMulMatrix basisOneI) z i j = ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] i j
[PROOFSTEP]
rw [Algebra.leftMulMatrix_eq_repr_mul, Complex.coe_basisOneI_repr, Complex.coe_basisOneI, mul_re, mul_im,
  Matrix.of_apply]
[GOAL]
case a.h
z : ℂ
i j : Fin 2
⊢ Matrix.vecCons (z.re * (Matrix.vecCons 1 ![I] j).re - z.im * (Matrix.vecCons 1 ![I] j).im)
      ![z.re * (Matrix.vecCons 1 ![I] j).im + z.im * (Matrix.vecCons 1 ![I] j).re] i =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head
z : ℂ
i : Fin 2
⊢ Matrix.vecCons
      (z.re * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).re -
        z.im * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).im)
      ![z.re * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).im +
          z.im * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).re]
      i =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp only [Fin.mk_zero, Matrix.cons_val_zero, one_re, mul_one, one_im, mul_zero, sub_zero, zero_add]
[GOAL]
case a.h.head
z : ℂ
i : Fin 2
⊢ Matrix.vecCons z.re ![z.im] i = Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i 0
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head.head
z : ℂ
⊢ Matrix.vecCons z.re ![z.im] { val := 0, isLt := (_ : 0 < 2) } =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] { val := 0, isLt := (_ : 0 < 2) } 0
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
z : ℂ
⊢ Matrix.vecCons z.re ![z.im] { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } 0
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head
z : ℂ
i : Fin 2
⊢ Matrix.vecCons
      (z.re * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).re -
        z.im * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).im)
      ![z.re * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).im +
          z.im * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).re]
      i =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp only [Fin.mk_one, Matrix.cons_val_one, Matrix.head_cons, I_re, mul_zero, I_im, mul_one, zero_sub, add_zero]
[GOAL]
case a.h.tail.head
z : ℂ
i : Fin 2
⊢ Matrix.vecCons (-z.im) ![z.re] i = Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i 1
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.tail.head.head
z : ℂ
⊢ Matrix.vecCons (-z.im) ![z.re] { val := 0, isLt := (_ : 0 < 2) } =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] { val := 0, isLt := (_ : 0 < 2) } 1
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
z : ℂ
⊢ Matrix.vecCons (-z.im) ![z.re] { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1
[PROOFSTEP]
rfl
[GOAL]
z : ℂ
⊢ ↑(trace ℝ ℂ) z = 2 * z.re
[PROOFSTEP]
rw [Algebra.trace_eq_matrix_trace Complex.basisOneI, Algebra.leftMulMatrix_complex, Matrix.trace_fin_two]
[GOAL]
z : ℂ
⊢ ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 0 0 + ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 1 1 = 2 * z.re
[PROOFSTEP]
exact (two_mul _).symm
[GOAL]
z : ℂ
⊢ ↑(norm ℝ) z = ↑normSq z
[PROOFSTEP]
rw [Algebra.norm_eq_matrix_det Complex.basisOneI, Algebra.leftMulMatrix_complex, Matrix.det_fin_two, normSq_apply]
[GOAL]
z : ℂ
⊢ ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 0 0 * ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 1 1 -
      ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 0 1 * ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 1 0 =
    z.re * z.re + z.im * z.im
[PROOFSTEP]
simp
