-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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.IsReal }
inl :
  (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        fromBlocks (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) (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.inl w) (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)
              (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.inl w) (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)
              (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.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
inl₁ :
  (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
    HAdd.hAdd (α := ℂ) (∑ x_1 : { w : InfinitePlace K // w.IsReal }, 1 w 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)
              (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.inl w) (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)
              (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.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
inl₂ :
  (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
    HAdd.hAdd (α := ℂ) (∑ x_1 : { w : InfinitePlace K // w.IsReal }, 1 w x_1 * x (↑x_1 : InfinitePlace K).embedding)
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        (0 w (x_1, 0) * x (↑x_1 : InfinitePlace K).embedding +
          0 w (x_1, 1) * x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
inl₃ :
  (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal }, (if w = x_1 then 1 else 0) * x (↑x_1 : InfinitePlace K).embedding)
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        (0 w (x_1, 0) * x (↑x_1 : InfinitePlace K).embedding +
          0 w (x_1, 1) * x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
inl₄ :
  (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal }, (if w = x_1 then 1 else 0) * x (↑x_1 : InfinitePlace K).embedding)
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        (0 * x (↑x_1 : InfinitePlace K).embedding +
          0 * x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
inl₅ :
  (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        if w = x_1 then 1 * x (↑x_1 : InfinitePlace K).embedding else 0 * x (↑x_1 : InfinitePlace K).embedding)
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        (0 * x (↑x_1 : InfinitePlace K).embedding +
          0 * x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
inl₆ :
  (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        if w = x_1 then x (↑x_1 : InfinitePlace K).embedding else 0 * x (↑x_1 : InfinitePlace K).embedding)
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        (0 * x (↑x_1 : InfinitePlace K).embedding +
          0 * x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
inl₇ :
  (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal }, if w = x_1 then x (↑x_1 : InfinitePlace K).embedding else 0)
      (∑ x : { w : InfinitePlace K // w.IsComplex }, HAdd.hAdd (α := ℂ) 0 0)
inl₈ :
  (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
    (if Membership.mem (γ := Finset { w : InfinitePlace K // w.IsReal }) univ w then x (↑w : InfinitePlace K).embedding
      else 0) +
      ∑ x : { w : InfinitePlace K // w.IsComplex }, HAdd.hAdd (α := ℂ) 0 0
⊢ (↑((((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.inl w)) :
      ℂ) =
    HAdd.hAdd (α := ℂ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        fromBlocks (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) (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.inl w) (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)
              (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.inl w) (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)
              (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.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
have inl₉ : (↑(x (↑w : InfinitePlace K).embedding).re : ℂ) =
  (if True then x (↑w : InfinitePlace K).embedding else 0) +
    ∑ x : { w : InfinitePlace K // w.IsComplex }, HAdd.hAdd (α := ℂ) 0 0
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]