Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦
                  of
                    (vecCons (vecCons (2⁻¹ • 1) (vecCons (2⁻¹ • 1) (2⁻¹ • ![])))
                      (vecCons (vecCons (2⁻¹ • -I) (vecCons (2⁻¹ • I) (2⁻¹ • ![]))) (2⁻¹ • ![])))).submatrix
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0
              ((blockDiagonal fun x ↦
                    of
                      (vecCons (vecCons (2⁻¹ • 1) (vecCons (2⁻¹ • 1) (2⁻¹ • ![])))
                        (vecCons (vecCons (2⁻¹ • -I) (vecCons (2⁻¹ • I) (2⁻¹ • ![]))) (2⁻¹ • ![])))).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0
              ((blockDiagonal fun x ↦
                    of
                      (vecCons (vecCons (2⁻¹ • 1) (vecCons (2⁻¹ • 1) (2⁻¹ • ![])))
                        (vecCons (vecCons (2⁻¹ • -I) (vecCons (2⁻¹ • I) (2⁻¹ • ![]))) (2⁻¹ • ![])))).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
smul_eq_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦
                  of
                    (vecCons (vecCons (2⁻¹ * 1) (vecCons (2⁻¹ * 1) (2⁻¹ • ![])))
                      (vecCons (vecCons (2⁻¹ * -I) (vecCons (2⁻¹ * I) (2⁻¹ • ![]))) (2⁻¹ • ![])))).submatrix
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0
              ((blockDiagonal fun x ↦
                    of
                      (vecCons (vecCons (2⁻¹ * 1) (vecCons (2⁻¹ * 1) (2⁻¹ • ![])))
                        (vecCons (vecCons (2⁻¹ * -I) (vecCons (2⁻¹ * I) (2⁻¹ • ![]))) (2⁻¹ • ![])))).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0
              ((blockDiagonal fun x ↦
                    of
                      (vecCons (vecCons (2⁻¹ * 1) (vecCons (2⁻¹ * 1) (2⁻¹ • ![])))
                        (vecCons (vecCons (2⁻¹ * -I) (vecCons (2⁻¹ * I) (2⁻¹ • ![]))) (2⁻¹ • ![])))).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))