awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
x : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x
y : mixedSpace K
hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y
⊢ ‖y‖ ≤ B

Tactic:
le_trans (norm_le_convexBodySumFun y) hy

Premises used: NumberField.mixedEmbedding.norm_le_convexBodySumFun, le_trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
x : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x
y : mixedSpace K
hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y
⊢ ‖y‖ ≤ B

Tactic:
exact le_trans (norm_le_convexBodySumFun y) hy

Premises used: NumberField.mixedEmbedding.norm_le_convexBodySumFun, le_trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
refine :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), dist x y ≤ B + B
refine₁ :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), ‖x - y‖ ≤ B + B
refine_1 :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), ‖x‖ ≤ B
refine_2 refine_2₁ :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), ‖y‖ ≤ B
⊢ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)

Tactic:
classical
  refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩
  simp_rw [dist_eq_norm]
  refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)
  · exact le_trans (norm_le_convexBodySumFun x) hx
  · exact le_trans (norm_le_convexBodySumFun y) hy

Premises used: Iff.mpr, dist_eq_norm, Metric.isBounded_iff, HAdd.hAdd, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
rw : IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
⊢ IsCompact (X := mixedSpace K) (convexBodySum K B)

Tactic:
rw [Metric.isCompact_iff_isClosed_bounded]

Premises used: Metric.isCompact_iff_isClosed_bounded
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)

Tactic:
⟨?_, convexBodySum_isBounded K B⟩

Premises used: And.intro, NumberField.mixedEmbedding.convexBodySum_isBounded
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
refine : IsClosed (X := mixedSpace K) (convexBodySum K B)
⊢ IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)

Tactic:
refine ⟨?_, convexBodySum_isBounded K B⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ IsClosed.{u_1} (X := mixedSpace K) (convexBodySumFun ⁻¹' Set.Icc 0 B)

Tactic:
IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))

Premises used: NumberField.mixedEmbedding.convexBodySumFun_continuous, isClosed_Icc, IsClosed.preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
h : Eq (α := Set (mixedSpace K)) (convexBodySum K B) (convexBodySumFun ⁻¹' Set.Icc 0 B)
⊢ IsClosed (X := mixedSpace K) (convexBodySum K B)

Tactic:
convert! IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))

Premises used: NumberField.mixedEmbedding.convexBodySumFun_continuous, isClosed_Icc, IsClosed.preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
h :
  ∀ (x : mixedSpace K),
    Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔
      Membership.mem (γ := Set (mixedSpace K)) (convexBodySumFun ⁻¹' Set.Icc 0 B) x
⊢ Eq (α := Set (mixedSpace K)) (convexBodySum K B) (convexBodySumFun ⁻¹' Set.Icc 0 B)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
x : mixedSpace K
⊢ Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔
    Membership.mem (γ := Set (mixedSpace K)) (convexBodySumFun ⁻¹' Set.Icc 0 B) x

Tactic:
simp [convexBodySumFun_nonneg]

Premises used: NumberField.mixedEmbedding.convexBodySumFun_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
rw rw₁ rw₂ :
  IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
rw₃ : IsClosed (X := mixedSpace K) (convexBodySum K B)
h : Eq (α := Set (mixedSpace K)) (convexBodySum K B) (convexBodySumFun ⁻¹' Set.Icc 0 B)
h₁ :
  ∀ (x : mixedSpace K),
    Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔
      Membership.mem (γ := Set (mixedSpace K)) (convexBodySumFun ⁻¹' Set.Icc 0 B) x
⊢ IsCompact (X := mixedSpace K) (convexBodySum K B)

Tactic:
classical
  rw [Metric.isCompact_iff_isClosed_bounded]
  refine ⟨?_, convexBodySum_isBounded K B⟩
  convert! IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
  ext
  simp [convexBodySumFun_nonneg]

Premises used: Metric.isCompact_iff_isClosed_bounded, NumberField.mixedEmbedding.convexBodySumFun_continuous, NumberField.mixedEmbedding.convexBodySumFun_nonneg, isClosed_Icc, IsClosed.preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ convexBodySumFactor K ≠ 0

Tactic:
div_ne_zero ?_ <| Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)

Premises used: Iff.mpr, div_ne_zero, Nat.factorial_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K ≠ 0
⊢ convexBodySumFactor K ≠ 0

Tactic:
refine div_ne_zero ?_ <| Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)

Premises used: Iff.mpr, div_ne_zero, Nat.factorial_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K ≠ 0

Tactic:
mul_ne_zero (pow_ne_zero _ two_ne_zero)
    (pow_ne_zero _ (div_ne_zero NNReal.pi_ne_zero two_ne_zero))

Premises used: NNReal.pi_ne_zero, pow_ne_zero, div_ne_zero, two_ne_zero, mul_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K ≠ 0

Tactic:
exact mul_ne_zero (pow_ne_zero _ two_ne_zero)
    (pow_ne_zero _ (div_ne_zero NNReal.pi_ne_zero two_ne_zero))

Premises used: NNReal.pi_ne_zero, pow_ne_zero, div_ne_zero, two_ne_zero, mul_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
inl :
  ∀ (hB : B ≤ 0),
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
      (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
inr :
  ∀ (hB : 0 < B),
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
      (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
obtain hB | hB := le_or_gt B 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : B ≤ 0
inl : finrank ℚ K ≠ 0
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
rw [convexBodySum_volume_eq_zero_of_le_zero K hB, ofReal_eq_zero.mpr hB, zero_pow, mul_zero]

Premises used: Iff.mpr, ENNReal.ofReal_eq_zero, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, MulZeroClass.mul_zero, zero_pow
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : B ≤ 0
⊢ finrank ℚ K ≠ 0

Tactic:
finrank_pos.ne'

Premises used: LT.lt.ne', Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : B ≤ 0
⊢ finrank ℚ K ≠ 0

Tactic:
exact finrank_pos.ne'

Premises used: LT.lt.ne', Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
rw :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    ENNReal.ofReal B ^ finrank ℚ K * (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |B ^ finrank.{0, u_1} ℝ (mixedSpace K)|)
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) : ℝ≥0∞)

Tactic:
addHaar_smul volume B (convexBodySum K 1)

Premises used: NumberField.mixedEmbedding.convexBodySum, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, MeasureTheory.Measure.addHaar_smul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h : convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
h₁ : ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank.{0, u_1} ℝ (mixedSpace K)|
h₂ :
  (↑(convexBodySumFactor K) : ℝ≥0∞) =
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    ENNReal.ofReal B ^ finrank ℚ K * (↑(convexBodySumFactor K) : ℝ≥0∞)

Tactic:
convert! addHaar_smul volume B (convexBodySum K 1)

Premises used: NumberField.mixedEmbedding.convexBodySum, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, MeasureTheory.Measure.addHaar_smul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h : ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal (|B| ^ finrank.{0, u_1} ℝ (mixedSpace K))
h₁ : ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B| ^ finrank.{0, u_1} ℝ (mixedSpace K)
h₂ : ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal B ^ finrank.{0, u_1} ℝ (mixedSpace K)
h₃ h₄ : ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal B ^ finrank ℚ K
⊢ ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank.{0, u_1} ℝ (mixedSpace K)|

Tactic:
rw [abs_pow, ofReal_pow (abs_nonneg _), abs_eq_self.mpr (le_of_lt hB),
          mixedEmbedding.finrank]

Premises used: Iff.mpr, le_of_lt, NumberField.mixedEmbedding.finrank, abs_eq_self, abs_nonneg, ENNReal.ofReal_pow, abs_pow
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ (↑(convexBodySumFactor K) : ℝ≥0∞) =
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1)

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ (↑(convexBodySumFactor K) : ℝ≥0∞) =
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1)

Tactic:
exact this.symm

Premises used: Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
inr :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
suffices volume (convexBodySum K 1) = (convexBodySumFactor K) by
      rw [mul_comm]
      convert! addHaar_smul volume B (convexBodySum K 1)
      · simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]
      · rw [abs_pow, ofReal_pow (abs_nonneg _), abs_eq_self.mpr (le_of_lt hB),
          mixedEmbedding.finrank]
      · exact this.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
inr :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) {x : mixedSpace K | convexBodySumFun x < 1} =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)

Tactic:
rw [MeasureTheory.measure_le_eq_lt _ ((convexBodySumFun_eq_zero_iff 0).mpr rfl)
      convexBodySumFun_neg convexBodySumFun_add_le
      (fun hx => (convexBodySumFun_eq_zero_iff _).mp hx)
      (fun r x => le_of_eq (convexBodySumFun_smul r x))]

Premises used: Iff.mpr, NumberField.mixedEmbedding.convexBodySumFun_add_le, NumberField.mixedEmbedding.convexBodySumFun_smul, NumberField.mixedEmbedding.convexBodySumFun_neg, MeasureTheory.measure_le_eq_lt, Iff.mp, le_of_eq, OfNat.ofNat, rfl, NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
inr :
  ENNReal.ofReal
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
          rexp (-HPow.hPow (β := ℝ) (convexBodySumFun x) 1)) /
        Gamma (HDiv.hDiv (α := ℝ) (↑(finrank.{0, u_1} ℝ (mixedSpace K)) : ℝ) 1 + 1)) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) {x : mixedSpace K | convexBodySumFun x < 1} =
    (↑(convexBodySumFactor K) : ℝ≥0∞)

Tactic:
rw [measure_lt_one_eq_integral_div_gamma (g := fun x : (mixedSpace K) => convexBodySumFun x)
      volume ((convexBodySumFun_eq_zero_iff 0).mpr rfl) convexBodySumFun_neg convexBodySumFun_add_le
      (fun hx => (convexBodySumFun_eq_zero_iff _).mp hx)
      (fun r x => le_of_eq (convexBodySumFun_smul r x)) zero_lt_one]

Premises used: Iff.mpr, NumberField.mixedEmbedding.convexBodySumFun_add_le, MeasureTheory.measure_lt_one_eq_integral_div_gamma, NumberField.mixedEmbedding.convexBodySumFun_smul, NumberField.mixedEmbedding.convexBodySumFun_neg, zero_lt_one, MeasureTheory.MeasureSpace.volume, Iff.mp, le_of_eq, OfNat.ofNat, rfl, NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
inr :
  ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ ENNReal.ofReal
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦
          rexp (-HPow.hPow (β := ℝ) (convexBodySumFun x) 1)) /
        Gamma (HDiv.hDiv (α := ℝ) (↑(finrank.{0, u_1} ℝ (mixedSpace K)) : ℝ) 1 + 1)) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)

Tactic:
simp_rw [mixedEmbedding.finrank, div_one, Gamma_nat_eq_factorial, ofReal_div_of_pos
      (Nat.cast_pos.mpr (Nat.factorial_pos _)), Real.rpow_one, ofReal_natCast]

Premises used: Iff.mpr, Nat.cast_pos, ENNReal.ofReal_div_of_pos, Real.rpow_one, NumberField.mixedEmbedding.finrank, Nat.factorial_pos, Real.Gamma_nat_eq_factorial, div_one, ENNReal.ofReal_natCast
-- 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
⊢ 0 ≤ HPow.hPow (α := ℝ) 2 (nrRealPlaces K)

Tactic:
positivity
-- 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
⊢ 0 ≤ π / 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
inr :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
⊢ ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)

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]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
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)
⊢ 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:
rw [integral_fintype_prod_volume_eq_pow (fun x => exp (-‖x‖)),
          integral_fintype_prod_volume_eq_pow (fun x => exp (-2 * ‖x‖))]

Premises used: Norm.norm, MeasureTheory.integral_fintype_prod_volume_eq_pow, HMul.hMul, Real.exp, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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‖))
        (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:
simp_rw [norm_eq_abs]

Premises used: Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
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)
⊢ 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

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]

Premises used: le_rfl, integral_comp_abs, Complex.integral_exp_neg_mul_rpow, integral_exp_neg_rpow, zero_lt_one, zero_lt_two