-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
      rexp
        (-(∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
            HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsReal } → ℝ) ↦
        ∏ w : { w : InfinitePlace K // w.IsReal }, rexp (-‖x w‖))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsComplex } → ℂ) ↦
        ∏ w : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x w‖))
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
      rexp
        (-∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
          -HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsReal } → ℝ) ↦
        ∏ w : { w : InfinitePlace K // w.IsReal }, rexp (-‖x w‖))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsComplex } → ℂ) ↦
        ∏ w : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x w‖))
simp_rw₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
      rexp
        (-∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
          HMul.hMul (α := ℝ) (-2) (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsReal } → ℝ) ↦
        ∏ w : { w : InfinitePlace K // w.IsReal }, rexp (-‖x w‖))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsComplex } → ℂ) ↦
        ∏ w : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x w‖))
simp_rw₃ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
      rexp
        (HAdd.hAdd (α := ℝ) (-∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖)
          (∑ i : { w : InfinitePlace K // w.IsComplex }, -2 * ‖x.2 i‖))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsReal } → ℝ) ↦
        ∏ w : { w : InfinitePlace K // w.IsReal }, rexp (-‖x w‖))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsComplex } → ℂ) ↦
        ∏ w : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x w‖))
simp_rw₄ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
      rexp
        (HAdd.hAdd (α := ℝ) (∑ x_1 : { w : InfinitePlace K // w.IsReal }, -‖x.1 x_1‖)
          (∑ i : { w : InfinitePlace K // w.IsComplex }, -2 * ‖x.2 i‖))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsReal } → ℝ) ↦
        ∏ w : { w : InfinitePlace K // w.IsReal }, rexp (-‖x w‖))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsComplex } → ℂ) ↦
        ∏ w : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x w‖))
simp_rw₅ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
      rexp (∑ x_1 : { w : InfinitePlace K // w.IsReal }, -‖x.1 x_1‖) *
        rexp (∑ i : { w : InfinitePlace K // w.IsComplex }, -2 * ‖x.2 i‖)) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsReal } → ℝ) ↦
        ∏ w : { w : InfinitePlace K // w.IsReal }, rexp (-‖x w‖))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsComplex } → ℂ) ↦
        ∏ w : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x w‖))
simp_rw₆ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
      HMul.hMul (α := ℝ) (∏ x_1 : { w : InfinitePlace K // w.IsReal }, rexp (-‖x.1 x_1‖))
        (∏ x_1 : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x.2 x_1‖))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsReal } → ℝ) ↦
        ∏ w : { w : InfinitePlace K // w.IsReal }, rexp (-‖x w‖))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsComplex } → ℂ) ↦
        ∏ w : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x w‖))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsReal } → ℝ) ↦
        ∏ w : { w : InfinitePlace K // w.IsReal }, rexp (-‖x w‖))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : { w : InfinitePlace K // w.IsComplex } → ℂ) ↦
        ∏ w : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x w‖))
have simp_rw₇ : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
    HMul.hMul (α := ℝ) (∏ x_1 : { w : InfinitePlace K // w.IsReal }, rexp (-‖x.1 x_1‖))
      (∏ x_1 : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖x.2 x_1‖)))
  (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.prod volume volume)
    fun (z : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) ↦
    HMul.hMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsReal }, rexp (-‖z.1 w‖))
      (∏ w : { w : InfinitePlace K // w.IsComplex }, rexp (-2 * ‖z.2 w‖)))
Tactic: simp_rw [convexBodySumFun_apply', neg_add, ← neg_mul, Finset.mul_sum,
          ← Finset.sum_neg_distrib, exp_add, exp_sum, ← integral_prod_mul, volume_eq_prod]