-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
simp_rw :
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₁ :
  HAdd.hAdd (α := ℝ)
      (∑ w : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ w : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₂ :
  HAdd.hAdd (α := ℝ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑1 : ℝ) : ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ w : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₃ :
  HAdd.hAdd (α := ℝ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑1 : ℝ) : ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑2 : ℝ) : ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₄ :
  HAdd.hAdd (α := ℝ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑2 : ℝ) : ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₅ :
  HAdd.hAdd (α := ℝ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal }, (normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑2 : ℝ) : ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₆ :
  HAdd.hAdd (α := ℝ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal }, (normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₇ :
  HAdd.hAdd (α := ℝ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (↑x_1 : InfinitePlace K) ⋯)‖)
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
⊢ convexBodySumFun x =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
have simp_rw₈ : HAdd.hAdd (α := ℝ)
    (∑ x_1 : { w : InfinitePlace K // w.IsReal },
      ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (↑x_1 : InfinitePlace K) sorry)‖)
    (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
      2 * ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (↑x_1 : InfinitePlace K) sorry)‖) =
  ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
    HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
Tactic: simp_rw [convexBodySumFun_apply, sum_eq_sum_add_sum, mult_isReal, mult_isComplex,
    Nat.cast_one, one_mul, Nat.cast_ofNat, normAtPlace_apply_of_isReal (Subtype.prop _),
    normAtPlace_apply_of_isComplex (Subtype.prop _), Finset.mul_sum]