-- 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 : { w : InfinitePlace K // w.IsComplex } × Fin 2
inr :
  ∀ (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2),
    (↑((((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, j))) :
        ℂ) =
      HAdd.hAdd (α := ℂ)
        (∑ x_1 : { w : InfinitePlace K // w.IsReal },
          fromBlocks (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) (n := { w : InfinitePlace K // w.IsReal }) 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, j)) (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 }) 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, j)) (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 }) 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, j)) (Sum.inr (x_1, 1)) *
              x (ComplexEmbedding.conjugate (↑x_1 : 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 c)) :
      ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        fromBlocks (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) (n := { w : InfinitePlace K // w.IsReal }) 1 0
            0
            (submatrix
              (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I])
              Prod.swap Prod.swap)
            (Sum.inr 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)
              (n := { w : InfinitePlace K // w.IsReal }) 1 0 0
              (submatrix
                (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I])
                Prod.swap Prod.swap)
              (Sum.inr 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)
              (n := { w : InfinitePlace K // w.IsReal }) 1 0 0
              (submatrix
                (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I])
                Prod.swap Prod.swap)
              (Sum.inr c) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))

Tactic:
rcases c with ⟨w, j⟩