-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
simp_rw :
  (↑((((Basis.repr (stdBasis K) :
                  (a : mixedSpace K) →
                    { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2 →₀ ℝ)
                (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (x (↑w : InfinitePlace K).embedding).re,
                  fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ x (↑w : InfinitePlace K).embedding) :
              { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2 →₀ ℝ) :
            (a : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) → ℝ)
          c) :
      ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        fromBlocks (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) 1 0 0
            (submatrix
              (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I])
              Prod.swap Prod.swap)
            c (Sum.inl x_1) *
          x (↑x_1 : InfinitePlace K).embedding)
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        (fromBlocks (l := { w : InfinitePlace K // w.IsReal }) (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) 1 0
              0
              (submatrix
                (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I])
                Prod.swap Prod.swap)
              c (Sum.inr (x_1, 0)) *
            x (↑x_1 : InfinitePlace K).embedding +
          fromBlocks (l := { w : InfinitePlace K // w.IsReal }) (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) 1
              0 0
              (submatrix
                (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I])
                Prod.swap Prod.swap)
              c (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
⊢ (↑((((Basis.repr (stdBasis K) : (a : mixedSpace K) → index K →₀ ℝ)
                ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) :
              index K →₀ ℝ) :
            (a : index K) → ℝ)
          c) :
      ℂ) =
    (matrixToStdBasis K *ᵥ x ∘ (⇑(indexEquiv K) : (a : index K) → K →+* ℂ)) c

Tactic:
simp_rw [commMap, matrixToStdBasis, LinearMap.coe_mk, AddHom.coe_mk,
    mulVec, dotProduct, Function.comp_apply, index, Fintype.sum_sum_type,
    diagonal_one, reindex_apply, ← univ_product_univ, sum_product,
    indexEquiv_apply_isReal, Fin.sum_univ_two, indexEquiv_apply_isComplex_fst,
    indexEquiv_apply_isComplex_snd, smul_of, smul_cons, smul_eq_mul,
    mul_one, Matrix.smul_empty, Equiv.prodComm_symm, Equiv.coe_prodComm]

Premises used: LinearMap.coe_mk, dotProduct, Matrix.smul_empty, Fintype.sum_sum_type, Matrix.smul_of, Matrix.reindex_apply, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_fst, Finset.univ_product_univ, NumberField.mixedEmbedding.index, NumberField.mixedEmbedding.commMap, Equiv.prodComm_symm, Equiv.coe_prodComm, Matrix.diagonal_one, NumberField.mixedEmbedding.indexEquiv_apply_isReal, Matrix.smul_cons, NumberField.mixedEmbedding.matrixToStdBasis, Function.comp_apply, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_snd, smul_eq_mul, mul_one, AddHom.coe_mk, Fin.sum_univ_two, Finset.sum_product, Matrix.mulVec