no goals
a : { x // x ∈ circle }
⊢ (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0
simp [pow_two, ← normSq_apply]
case a.h
a : { x // x ∈ circle }
i j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (↑(↑rotation a).toLinearEquiv) i j =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0)) i j
a : { x // x ∈ circle }
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) ↑(↑rotation a).toLinearEquiv =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0))
ext (i j)
case a.h
a : { x // x ∈ circle }
i j : Fin 2
⊢ Matrix.vecCons ((↑a).re * (Matrix.vecCons 1 ![I] j).re - (↑a).im * (Matrix.vecCons 1 ![I] j).im)
      ![(↑a).re * (Matrix.vecCons 1 ![I] j).im + (↑a).im * (Matrix.vecCons 1 ![I] j).re] i =
    Matrix.vecCons (Matrix.vecCons (↑a).re ![-(↑a).im] j) (fun i => Matrix.vecCons (↑a).im ![(↑a).re] j) i
case a.h
a : { x // x ∈ circle }
i j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (↑(↑rotation a).toLinearEquiv) i j =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0)) i j
simp [LinearMap.toMatrix_apply]
no goals
case a.h
a : { x // x ∈ circle }
i j : Fin 2
⊢ Matrix.vecCons ((↑a).re * (Matrix.vecCons 1 ![I] j).re - (↑a).im * (Matrix.vecCons 1 ![I] j).im)
      ![(↑a).re * (Matrix.vecCons 1 ![I] j).im + (↑a).im * (Matrix.vecCons 1 ![I] j).re] i =
    Matrix.vecCons (Matrix.vecCons (↑a).re ![-(↑a).im] j) (fun i => Matrix.vecCons (↑a).im ![(↑a).re] j) i
fin_cases i <;> fin_cases j <;> simp