-- Mathlib/RingTheory/Complex.lean
theorem Algebra.leftMulMatrix_complex (z : ℂ) :
    Algebra.leftMulMatrix Complex.basisOneI z = !![z.re, -z.im; z.im, z.re]

Proof state:
case a.«_@».Mathlib.Data.Matrix.Defs._hyg.176.«0»
z : ℂ
i : Fin 2
⊢ ![z.re, z.im] i = ![![z.re, -z.im], ![z.im, z.re]] i 0

Tactic:
fin_cases i <;> rfl

Result:
no goals

Proof state:
case a.«_@».Mathlib.Data.Matrix.Defs._hyg.176.«0»
z : ℂ
i : Fin 2
⊢ ![z.re * (![1, I] ((fun i => i) ⟨0, ⋯⟩)).re - z.im * (![1, I] ((fun i => i) ⟨0, ⋯⟩)).im,
        z.re * (![1, I] ((fun i => i) ⟨0, ⋯⟩)).im + z.im * (![1, I] ((fun i => i) ⟨0, ⋯⟩)).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun i => i) ⟨0, ⋯⟩)

Tactic:
simp only [Fin.zero_eta, id_eq, Matrix.cons_val_zero, one_re, mul_one, one_im, mul_zero,
  sub_zero, zero_add, Matrix.cons_val_fin_one]

Result:
case a.«_@».Mathlib.Data.Matrix.Defs._hyg.176.«0»
z : ℂ
i : Fin 2
⊢ ![z.re, z.im] i = ![![z.re, -z.im], ![z.im, z.re]] i 0

Proof state:
case a
z : ℂ
i j : Fin 2
⊢ ![z.re * (![1, I] j).re - z.im * (![1, I] j).im, z.re * (![1, I] j).im + z.im * (![1, I] j).re] i =
    ![![z.re, -z.im], ![z.im, z.re]] i j

Tactic:
fin_cases j

Result:
case a.«_@».Mathlib.Data.Matrix.Defs._hyg.176.«0»
z : ℂ
i : Fin 2
⊢ ![z.re * (![1, I] ((fun i => i) ⟨0, ⋯⟩)).re - z.im * (![1, I] ((fun i => i) ⟨0, ⋯⟩)).im,
        z.re * (![1, I] ((fun i => i) ⟨0, ⋯⟩)).im + z.im * (![1, I] ((fun i => i) ⟨0, ⋯⟩)).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun i => i) ⟨0, ⋯⟩)

case a.«_@».Mathlib.Data.Matrix.Defs._hyg.176.«1»
z : ℂ
i : Fin 2
⊢ ![z.re * (![1, I] ((fun i => i) ⟨1, ⋯⟩)).re - z.im * (![1, I] ((fun i => i) ⟨1, ⋯⟩)).im,
        z.re * (![1, I] ((fun i => i) ⟨1, ⋯⟩)).im + z.im * (![1, I] ((fun i => i) ⟨1, ⋯⟩)).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun i => i) ⟨1, ⋯⟩)

Proof state:
case a
z : ℂ
i j : Fin 2
⊢ (leftMulMatrix basisOneI) z i j = !![z.re, -z.im; z.im, z.re] i j

Tactic:
rw [Algebra.leftMulMatrix_eq_repr_mul, Complex.coe_basisOneI_repr, Complex.coe_basisOneI, mul_re,
  mul_im, Matrix.of_apply]

Result:
case a
z : ℂ
i j : Fin 2
⊢ ![z.re * (![1, I] j).re - z.im * (![1, I] j).im, z.re * (![1, I] j).im + z.im * (![1, I] j).re] i =
    ![![z.re, -z.im], ![z.im, z.re]] i j

Proof state:
case a.«_@».Mathlib.Data.Matrix.Defs._hyg.176.«1»
z : ℂ
i : Fin 2
⊢ ![z.re * (![1, I] ((fun i => i) ⟨1, ⋯⟩)).re - z.im * (![1, I] ((fun i => i) ⟨1, ⋯⟩)).im,
        z.re * (![1, I] ((fun i => i) ⟨1, ⋯⟩)).im + z.im * (![1, I] ((fun i => i) ⟨1, ⋯⟩)).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun i => i) ⟨1, ⋯⟩)

Tactic:
simp only [Fin.mk_one, id_eq, Matrix.cons_val_one, Matrix.head_cons, I_re, mul_zero, I_im,
  mul_one, zero_sub, add_zero, Matrix.cons_val_fin_one]

Result:
case a.«_@».Mathlib.Data.Matrix.Defs._hyg.176.«1»
z : ℂ
i : Fin 2
⊢ ![-z.im, z.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1

Proof state:
case a.«_@».Mathlib.Data.Matrix.Defs._hyg.176.«1»
z : ℂ
i : Fin 2
⊢ ![-z.im, z.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1

Tactic:
fin_cases i <;> rfl

Result:
no goals

Proof state:
z : ℂ
⊢ (leftMulMatrix basisOneI) z = !![z.re, -z.im; z.im, z.re]

Tactic:
ext i j

Result:
case a
z : ℂ
i j : Fin 2
⊢ (leftMulMatrix basisOneI) z i j = !![z.re, -z.im; z.im, z.re] i j