-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem stdBasis_repr_eq_matrixToStdBasis_mul (x : (K →+* ℂ) → ℂ)
    (hx : ∀ φ, conj (x φ) = x (ComplexEmbedding.conjugate φ)) (c : index K) :
    ((stdBasis K).repr (commMap K x) c : ℂ) =
      (matrixToStdBasis K *ᵥ (x ∘ (indexEquiv K))) c

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : { w // w.IsComplex } × Fin 2
⊢ ↑(((stdBasis K).repr (fun w => (x (↑w).embedding).re, fun w => x (↑w).embedding)) (Sum.inr c)) =
    ∑ x_1 : { w // w.IsReal },
        fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inr c) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1 : { w // w.IsComplex },
        (fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr c) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr c) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
rcases c with ⟨w, j⟩

Result:
case inr.mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
j : Fin 2
⊢ ↑(((stdBasis K).repr (fun w => (x (↑w).embedding).re, fun w => x (↑w).embedding)) (Sum.inr (w, j))) =
    ∑ x_1 : { w // w.IsReal },
        fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inr (w, j)) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1 : { w // w.IsComplex },
        (fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, j)) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, j)) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(((stdBasis K).repr (fun w => (x (↑w).embedding).re, fun w => x (↑w).embedding)) (Sum.inl w)) =
    ∑ x_1 : { w // w.IsReal },
        fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inl w) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1 : { w // w.IsComplex },
        (fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
simp_rw [stdBasis_apply_isReal, fromBlocks_apply₁₁, fromBlocks_apply₁₂,
  one_apply, Matrix.zero_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_univ, ite_true,
  add_zero, sum_const_zero, add_zero, ← conj_eq_iff_re, hx (embedding w.val),
  conjugate_embedding_eq_of_isReal w.prop]

Result:
no goals

Proof state:
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 ((commMap K) x)) c) = (matrixToStdBasis K *ᵥ x ∘ ⇑(indexEquiv 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]

Result:
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 : { w // w.IsReal },
        fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap) c
            (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1 : { w // w.IsComplex },
        (fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap) c
              (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap) c
              (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Proof state:
case inr.mk.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
⊢ ↑(((stdBasis K).repr (fun w => (x (↑w).embedding).re, fun w => x (↑w).embedding))
        (Sum.inr (w, (fun i => i) ⟨0, ⋯⟩))) =
    ∑ x_1 : { w // w.IsReal },
        fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inr (w, (fun i => i) ⟨0, ⋯⟩)) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1 : { w // w.IsComplex },
        (fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, (fun i => i) ⟨0, ⋯⟩)) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, (fun i => i) ⟨0, ⋯⟩)) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
simp only [Fin.zero_eta, Fin.isValue, id_eq, stdBasis_apply_isComplex_fst, re_eq_add_conj,
  mul_neg, fromBlocks_apply₂₁, zero_apply, zero_mul, sum_const_zero, fromBlocks_apply₂₂,
  submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply, cons_val', cons_val_zero,
  empty_val', cons_val_fin_one, ite_mul, cons_val_one, head_cons, sum_add_distrib, sum_ite_eq,
  mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]

Result:
case inr.mk.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
⊢ (x (↑w).embedding + (starRingEnd ℂ) (x (↑w).embedding)) / 2 =
    2⁻¹ * x (↑w).embedding + 2⁻¹ * (starRingEnd ℂ) (x (↑w).embedding)