Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case «0».«0»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re]
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨0, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨0, ⋯⟩))
      ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re]
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨1, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨1, ⋯⟩))
      ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«0»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re]
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨0, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨0, ⋯⟩))
      ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«1»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re]
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨1, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨1, ⋯⟩))
      ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re]
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨0, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨0, ⋯⟩))
      ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re]
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨1, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨1, ⋯⟩))
      ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«0»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re]
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨0, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨0, ⋯⟩))
      ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«1»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re]
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨1, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨1, ⋯⟩))
      ((fun i ↦ i) ⟨1, ⋯⟩)