-- 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 φ)
w : { w : InfinitePlace K // w.IsComplex }
inr :
  HSub.hSub (β := ℂ) (x (↑w : InfinitePlace K).embedding)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) /
      (2 * I) =
    -(2⁻¹ * I * x (↑w : InfinitePlace K).embedding) +
      HMul.hMul (β := ℂ) (2⁻¹ * I) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ)
⊢ (↑((((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) → ℝ)
          (Sum.inr (w, (fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))) :
      ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        fromBlocks (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) (n := { w : InfinitePlace K // w.IsReal })
            (o := { 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)
            (Sum.inr (w, (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) (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)
              (n := { w : InfinitePlace K // w.IsReal }) (o := { 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)
              (Sum.inr (w, (fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) (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)
              (n := { w : InfinitePlace K // w.IsReal }) (o := { 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)
              (Sum.inr (w, (fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))

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

Premises used: Finset.mem_univ, Fin.mk_one, Matrix.fromBlocks_apply₂₂, Matrix.zero_apply, Finset.sum_add_distrib, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, MulZeroClass.zero_mul, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.empty_val', Prod.swap_prod_mk, Matrix.cons_val_fin_one, Matrix.fromBlocks_apply₂₁, Matrix.of_apply, NumberField.InfinitePlace.embedding, zero_add, Finset.sum_const_zero, Fin.isValue, ite_mul, Complex.im_eq_sub_conj, reduceIte, neg_mul, Matrix.submatrix_apply, Subtype.val, Matrix.blockDiagonal_apply, Finset.sum_ite_eq, mul_neg, Matrix.cons_val'