awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
⊢ ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have 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∞)
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]
-- 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∞)
⊢ ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have 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∞)
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]
-- 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∞)
⊢ 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) * (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∞)
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]
-- 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∞)
⊢ 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) * (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∞)
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]
-- 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
⊢ ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have inr : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) =
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
Tactic: suffices ∫ x : mixedSpace K, exp (-convexBodySumFun x) =
        (2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K by
      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]
-- 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
⊢ (@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 : (@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‖))
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]
-- 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‖))
⊢ (@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₁ : (@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‖))
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]
-- 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‖))
⊢ (@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₂ : (@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‖))
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]
-- 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
⊢ 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‖)) =
    HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-|x|))
        (nrRealPlaces K) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-2 * ‖x‖))
        (nrComplexPlaces K)
have rw : HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-‖x‖))
      (card.{u_1} { w : InfinitePlace K // w.IsReal }) *
    HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-2 * ‖x‖))
      (card.{u_1} { w : InfinitePlace K // w.IsComplex }) =
  HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-|x|))
      (nrRealPlaces K) *
    HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-2 * ‖x‖))
      (nrComplexPlaces K)
Tactic: rw [integral_fintype_prod_volume_eq_pow (fun x => exp (-‖x‖)),
          integral_fintype_prod_volume_eq_pow (fun x => exp (-2 * ‖x‖))]
-- 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
⊢ HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-|x|))
        (nrRealPlaces K) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-2 * ‖x‖))
        (nrComplexPlaces K) =
    (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) 2 (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K
have rw : HMul.hMul (α := ℝ) 2
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (x : ℝ) ↦ rexp (-x)) ^
      nrRealPlaces K *
    HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-2 * ‖x‖))
      (nrComplexPlaces K) =
  HMul.hMul (α := ℝ) 2
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (x : ℝ) ↦
          rexp (-HPow.hPow (β := ℝ) x 1)) ^
      nrRealPlaces K *
    HPow.hPow (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-2 * HPow.hPow (β := ℝ) ‖x‖ 1))
      (nrComplexPlaces K)
Tactic: rw [integral_comp_abs (f := fun x => exp (-x)), ← integral_exp_neg_rpow zero_lt_one,
          ← Complex.integral_exp_neg_mul_rpow le_rfl zero_lt_two]
-- 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
⊢ (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) 2 (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
have simp_rw : (2 * Gamma (HAdd.hAdd (α := ℝ) 1 1)) ^ nrRealPlaces K *
    (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * Gamma (HAdd.hAdd (α := ℝ) 2 1)) ^ nrComplexPlaces K =
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
Tactic: simp_rw [div_one, one_add_one_eq_two, Gamma_add_one two_ne_zero, Gamma_two, mul_one,
          mul_assoc, ← Real.rpow_add_one two_ne_zero, show (-2 : ℝ) + 1 = -1 by norm_num,
          Real.rpow_neg_one, div_eq_mul_inv]
-- 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 :
  (2 * Gamma (HAdd.hAdd (α := ℝ) 1 1)) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * Gamma (HAdd.hAdd (α := ℝ) 2 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
⊢ (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) 2 (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
have simp_rw₁ : (2 * Gamma 2) ^ nrRealPlaces K *
    (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * Gamma (HAdd.hAdd (α := ℝ) 2 1)) ^ nrComplexPlaces K =
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
Tactic: simp_rw [div_one, one_add_one_eq_two, Gamma_add_one two_ne_zero, Gamma_two, mul_one,
          mul_assoc, ← Real.rpow_add_one two_ne_zero, show (-2 : ℝ) + 1 = -1 by norm_num,
          Real.rpow_neg_one, div_eq_mul_inv]
-- 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 :
  (2 * Gamma (HAdd.hAdd (α := ℝ) 1 1)) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * Gamma (HAdd.hAdd (α := ℝ) 2 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₁ :
  (2 * Gamma 2) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * Gamma (HAdd.hAdd (α := ℝ) 2 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
⊢ (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) 2 (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
have simp_rw₂ : (2 * Gamma 2) ^ nrRealPlaces K * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * (2 * Gamma 2)) ^ nrComplexPlaces K =
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
Tactic: simp_rw [div_one, one_add_one_eq_two, Gamma_add_one two_ne_zero, Gamma_two, mul_one,
          mul_assoc, ← Real.rpow_add_one two_ne_zero, show (-2 : ℝ) + 1 = -1 by norm_num,
          Real.rpow_neg_one, div_eq_mul_inv]