-- 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.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)

Tactic:
field_simp

Result:
no goals

Proof state:
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))

Tactic:
fin_cases j

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 }
⊢ ↑(((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))

case inr.mk.«1»
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) ⟨1, ⋯⟩))) =
    ∑ 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) ⟨1, ⋯⟩)) (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) ⟨1, ⋯⟩)) (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) ⟨1, ⋯⟩)) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Proof state:
case inr.mk.«1»
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) ⟨1, ⋯⟩))) =
    ∑ 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) ⟨1, ⋯⟩)) (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) ⟨1, ⋯⟩)) (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) ⟨1, ⋯⟩)) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
simp only [Fin.mk_one, Fin.isValue, id_eq, stdBasis_apply_isComplex_snd, im_eq_sub_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, cons_val_one, head_fin_const, ite_mul, neg_mul, head_cons,
  sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]

Result:
case inr.mk.«1»
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 * I) =
    -(2⁻¹ * I * x (↑w).embedding) + 2⁻¹ * I * (starRingEnd ℂ) (x (↑w).embedding)

Proof state:
case inr.mk.«1»
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 * I⁻¹ * (1 / 2) + (starRingEnd ℂ) (x (↑w).embedding) * I⁻¹ * (-1 / 2) =
    x (↑w).embedding * I * (-1 / 2) + (starRingEnd ℂ) (x (↑w).embedding) * I * (1 / 2)

Tactic:
field_simp

Result:
no goals

Proof state:
case inr.mk.«1»
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 * I) =
    -(2⁻¹ * I * x (↑w).embedding) + 2⁻¹ * I * (starRingEnd ℂ) (x (↑w).embedding)

Tactic:
ring_nf

Result:
case inr.mk.«1»
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 * I⁻¹ * (1 / 2) + (starRingEnd ℂ) (x (↑w).embedding) * I⁻¹ * (-1 / 2) =
    x (↑w).embedding * I * (-1 / 2) + (starRingEnd ℂ) (x (↑w).embedding) * I * (1 / 2)