-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
rw :
  ENNReal.ofReal (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
rw₁ :
  ENNReal.ofReal (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K /
          (↑(finrank ℚ K).factorial : ℝ≥0)) :
      ℝ≥0∞)
rw₂ :
  ENNReal.ofReal (HPow.hPow (α := ℝ) 2 (nrRealPlaces K)) * ENNReal.ofReal ((π / 2) ^ nrComplexPlaces K) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K /
          (↑(finrank ℚ K).factorial : ℝ≥0)) :
      ℝ≥0∞)
rw₃ :
  ENNReal.ofReal 2 ^ nrRealPlaces K * ENNReal.ofReal ((π / 2) ^ nrComplexPlaces K) / (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K /
          (↑(finrank ℚ K).factorial : ℝ≥0)) :
      ℝ≥0∞)
rw₄ :
  ENNReal.ofReal 2 ^ nrRealPlaces K * ENNReal.ofReal (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K /
          (↑(finrank ℚ K).factorial : ℝ≥0)) :
      ℝ≥0∞)
rw₅ :
  ENNReal.ofReal 2 ^ nrRealPlaces K * (ENNReal.ofReal π / ENNReal.ofReal 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K /
          (↑(finrank ℚ K).factorial : ℝ≥0)) :
      ℝ≥0∞)
rw₆ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (ENNReal.ofReal π / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K /
          (↑(finrank ℚ K).factorial : ℝ≥0)) :
      ℝ≥0∞)
rw₇ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (ENNReal.ofReal (↑NNReal.pi : ℝ) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K /
          (↑(finrank ℚ K).factorial : ℝ≥0)) :
      ℝ≥0∞)
rw₈ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K /
          (↑(finrank ℚ K).factorial : ℝ≥0)) :
      ℝ≥0∞)
rw₉ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K) : ℝ≥0∞) /
      (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ≥0∞)
rw₁₀ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑((NNReal.pi / 2) ^ nrComplexPlaces K) : ℝ≥0∞) /
      (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ≥0∞)
rw₁₁ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑2 : ℝ≥0∞) ^ nrRealPlaces K * (↑((NNReal.pi / 2) ^ nrComplexPlaces K) : ℝ≥0∞) /
      (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ≥0∞)
rw₁₂ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑2 : ℝ≥0∞) ^ nrRealPlaces K * (↑(NNReal.pi / 2) : ℝ≥0∞) ^ nrComplexPlaces K /
      (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ≥0∞)
rw₁₃ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑(NNReal.pi / 2) : ℝ≥0∞) ^ nrComplexPlaces K /
      (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ≥0∞)
rw₁₄ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / (↑2 : ℝ≥0∞)) ^ nrComplexPlaces K /
      (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ≥0∞)
rw₁₅ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ≥0∞)
rw₁₆ rw₁₇ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ((↑NNReal.pi : ℝ≥0∞) / 2) ^ nrComplexPlaces K /
      (↑(finrank ℚ K).factorial : ℝ≥0∞)
⊢ ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)

Tactic:
rw [this, convexBodySumFactor, ofReal_mul (by positivity), ofReal_pow zero_le_two,
        ofReal_pow (by positivity), ofReal_div_of_pos zero_lt_two, ofReal_ofNat,
        ← NNReal.coe_real_pi, ofReal_coe_nnreal, coe_div (Nat.cast_ne_zero.mpr
        (Nat.factorial_ne_zero _)), coe_mul, coe_pow, coe_pow, coe_ofNat, coe_div two_ne_zero,
        coe_ofNat, coe_natCast]

Premises used: Iff.mpr, ENNReal.ofReal_div_of_pos, ENNReal.ofReal_mul, ENNReal.ofReal_ofNat, NNReal.coe_real_pi, two_ne_zero, ENNReal.coe_mul, Nat.factorial_ne_zero, ENNReal.ofReal_coe_nnreal, ENNReal.coe_pow, zero_le_two, zero_lt_two, ENNReal.coe_ofNat, ENNReal.coe_natCast, ENNReal.ofReal_pow, NumberField.mixedEmbedding.convexBodySumFactor, ENNReal.coe_div, Nat.cast_ne_zero