-- 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
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∞)
⊢ ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have 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∞)
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]