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
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
simp_rw₂ :
  (2 * Gamma 2) ^ nrRealPlaces K * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * (2 * Gamma 2)) ^ 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₃ : HMul.hMul (α := ℝ) 2 1 ^ nrRealPlaces K *
    (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * HMul.hMul (α := ℝ) 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
simp_rw₂ :
  (2 * Gamma 2) ^ nrRealPlaces K * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * (2 * Gamma 2)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₃ :
  HMul.hMul (α := ℝ) 2 1 ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * HMul.hMul (α := ℝ) 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₄ : HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 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]
-- 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
simp_rw₂ :
  (2 * Gamma 2) ^ nrRealPlaces K * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * (2 * Gamma 2)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₃ :
  HMul.hMul (α := ℝ) 2 1 ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * HMul.hMul (α := ℝ) 2 1) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₄ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 2) ^ 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₅ : HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * (HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 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]
-- 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
simp_rw₂ :
  (2 * Gamma 2) ^ nrRealPlaces K * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * (2 * Gamma 2)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₃ :
  HMul.hMul (α := ℝ) 2 1 ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * HMul.hMul (α := ℝ) 2 1) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₄ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 2) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₅ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * (HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 2)) ^ 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₆ : HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) 2 (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
simp_rw₂ :
  (2 * Gamma 2) ^ nrRealPlaces K * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * (2 * Gamma 2)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₃ :
  HMul.hMul (α := ℝ) 2 1 ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * HMul.hMul (α := ℝ) 2 1) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₄ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 2) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₅ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * (HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 2)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₆ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) 2 (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₇ : HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) (β := ℝ) 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
simp_rw₂ :
  (2 * Gamma 2) ^ nrRealPlaces K * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * (2 * Gamma 2)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₃ :
  HMul.hMul (α := ℝ) 2 1 ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * HMul.hMul (α := ℝ) 2 1) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₄ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 2) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₅ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * (HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 2)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₆ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℝ) (-2) 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₇ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) (β := ℝ) 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₈ : HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * 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]
-- 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)) =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
have _ : (@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‖))
Tactic: calc
      _ = (∫ x : {w : InfinitePlace K // IsReal w} → ℝ, ∏ w, exp (-‖x w‖)) *
              (∫ x : {w : InfinitePlace K // IsComplex w} → ℂ, ∏ w, exp (-2 * ‖x w‖)) := by
        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]
      _ = (∫ x : ℝ, exp (-|x|)) ^ nrRealPlaces K *
              (∫ x : ℂ, Real.exp (-2 * ‖x‖)) ^ nrComplexPlaces K := by
        rw [integral_fintype_prod_volume_eq_pow (fun x => exp (-‖x‖)),
          integral_fintype_prod_volume_eq_pow (fun x => exp (-2 * ‖x‖))]
        simp_rw [norm_eq_abs]
      _ = (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K *
              (π * (2 : ℝ) ^ (-(2 : ℝ) / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K := by
        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]
        simp_rw [Real.rpow_one]
      _ = (2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K := by
        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
_ :
  (@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‖))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
have _₁ : 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)
Tactic: calc
      _ = (∫ x : {w : InfinitePlace K // IsReal w} → ℝ, ∏ w, exp (-‖x w‖)) *
              (∫ x : {w : InfinitePlace K // IsComplex w} → ℂ, ∏ w, exp (-2 * ‖x w‖)) := by
        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]
      _ = (∫ x : ℝ, exp (-|x|)) ^ nrRealPlaces K *
              (∫ x : ℂ, Real.exp (-2 * ‖x‖)) ^ nrComplexPlaces K := by
        rw [integral_fintype_prod_volume_eq_pow (fun x => exp (-‖x‖)),
          integral_fintype_prod_volume_eq_pow (fun x => exp (-2 * ‖x‖))]
        simp_rw [norm_eq_abs]
      _ = (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K *
              (π * (2 : ℝ) ^ (-(2 : ℝ) / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K := by
        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]
        simp_rw [Real.rpow_one]
      _ = (2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K := by
        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
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)
have refine : Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) =
  Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))
Tactic: refine Fintype.equivOfCardEq ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) =
    Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))
have rw : finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) =
  Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
rw :
  finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) =
    Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))
⊢ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) =
    Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))
have rw₁ : finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) = finrank.{0, u_1} ℤ (𝓞 K)
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
rw :
  finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) =
    Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))
rw₁ : finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) = finrank.{0, u_1} ℤ (𝓞 K)
⊢ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) =
    Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))
have rw₂ : finrank.{0, u_1} ℤ (𝓞 K) = finrank.{0, u_1} ℤ (𝓞 K)
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
  Fintype.equivOfCardEq ⋯
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
        (fractionalIdealLatticeBasis K I)) =
    HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
        ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞)
    (ENNReal.ofReal
      |((Basis.det (latticeBasis K) : mixedSpace K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
          (⇑(Basis.reindex (fractionalIdealLatticeBasis K I) e) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)|)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
      ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞)
    (ENNReal.ofReal
      (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
      ℝ≥0∞)
Tactic: rw [← fundamentalDomain_reindex (fractionalIdealLatticeBasis K I) e,
    measure_fundamentalDomain ((fractionalIdealLatticeBasis K I).reindex e)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
  Fintype.equivOfCardEq ⋯
rw :
  HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal
        |((Basis.det (latticeBasis K) : mixedSpace K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
            (⇑(Basis.reindex (fractionalIdealLatticeBasis K I) e) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)|)
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
        ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
        ℝ≥0∞)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
        (fractionalIdealLatticeBasis K I)) =
    HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
        ℝ≥0∞)
have b₀ : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
Tactic: rw [← fundamentalDomain_reindex (fractionalIdealLatticeBasis K I) e,
    measure_fundamentalDomain ((fractionalIdealLatticeBasis K I).reindex e)]