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 :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
h₂ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ w : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
        1}
h₃ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B⁻¹| ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₄ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B|⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₅ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K, (↑x.mult : ℝ) * HMul.hMul (β := ℝ) B⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₆ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          HMul.hMul (β := ℝ) ((↑x.mult : ℝ) * B⁻¹) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₇ : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  {a : mixedSpace K |
    LE.le (α := ℝ)
      (∑ x : InfinitePlace K, HMul.hMul (β := ℝ) (B⁻¹ * (↑x.mult : ℝ)) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
      1}
Tactic: 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]
-- 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 :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
h₂ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ w : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
        1}
h₃ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B⁻¹| ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₄ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B|⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₅ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K, (↑x.mult : ℝ) * HMul.hMul (β := ℝ) B⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₆ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          HMul.hMul (β := ℝ) ((↑x.mult : ℝ) * B⁻¹) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₇ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          HMul.hMul (β := ℝ) (B⁻¹ * (↑x.mult : ℝ)) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₈ : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  {a : mixedSpace K |
    LE.le (α := ℝ)
      (∑ x : InfinitePlace K,
        B⁻¹ * HMul.hMul (α := ℝ) (β := ℝ) ((↑x.mult : ℝ) : ℝ) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
      1}
Tactic: 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]
-- 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 :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
h₂ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ w : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
        1}
h₃ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B⁻¹| ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₄ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B|⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₅ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K, (↑x.mult : ℝ) * HMul.hMul (β := ℝ) B⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₆ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          HMul.hMul (β := ℝ) ((↑x.mult : ℝ) * B⁻¹) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₇ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          HMul.hMul (β := ℝ) (B⁻¹ * (↑x.mult : ℝ)) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₈ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          B⁻¹ * HMul.hMul (α := ℝ) (β := ℝ) ((↑x.mult : ℝ) : ℝ) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₉ : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  {a : mixedSpace K |
    B⁻¹ *
        ∑ i : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑i.mult : ℝ) : ℝ) ((normAtPlace i : (a : mixedSpace K) → ℝ) a : ℝ) ≤
      1}
Tactic: 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]
-- 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 :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
h₂ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ w : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
        1}
h₃ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B⁻¹| ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₄ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B|⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₅ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K, (↑x.mult : ℝ) * HMul.hMul (β := ℝ) B⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₆ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          HMul.hMul (β := ℝ) ((↑x.mult : ℝ) * B⁻¹) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₇ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          HMul.hMul (β := ℝ) (B⁻¹ * (↑x.mult : ℝ)) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₈ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          B⁻¹ * HMul.hMul (α := ℝ) (β := ℝ) ((↑x.mult : ℝ) : ℝ) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₉ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      B⁻¹ *
          ∑ i : InfinitePlace K,
            HMul.hMul (α := ℝ) (β := ℝ) ((↑i.mult : ℝ) : ℝ) ((normAtPlace i : (a : mixedSpace K) → ℝ) a : ℝ) ≤
        1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₁₀ : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  {a : mixedSpace K |
    ∑ i : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑i.mult : ℝ) : ℝ) ((normAtPlace i : (a : mixedSpace K) → ℝ) a : ℝ) ≤
      B * 1}
Tactic: 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]
-- 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 :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank.{0, u_1} ℝ (mixedSpace K)|
have h : 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]
-- 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 :
  ((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))
⊢ ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank.{0, u_1} ℝ (mixedSpace K)|
have h₁ : 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]
-- 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 :
  ((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)
⊢ ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank.{0, u_1} ℝ (mixedSpace K)|
have h₂ : 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]
-- 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 :
  ((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)
⊢ ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank.{0, u_1} ℝ (mixedSpace K)|
have h₃ : ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal B ^ finrank ℚ K
Tactic: rw [abs_pow, ofReal_pow (abs_nonneg _), abs_eq_self.mpr (le_of_lt hB),
          mixedEmbedding.finrank]
-- 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
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
have inr : ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
  (↑(convexBodySumFactor K) : ℝ≥0∞)
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
-- 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
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have inr : ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) {x : mixedSpace K | convexBodySumFun x < 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))]
-- 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
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) {x : mixedSpace K | convexBodySumFun x < 1} =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have 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∞)
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]
-- 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 (-HPow.hPow (β := ℝ) (convexBodySumFun x) 1)) /
        Gamma (HDiv.hDiv (α := ℝ) (↑(finrank.{0, u_1} ℝ (mixedSpace K)) : ℝ) 1 + 1)) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have inr : ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
    (↑(finrank ℚ K).factorial : ℝ≥0∞) =
  (↑(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]
-- 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
⊢ ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have rw : ENNReal.ofReal (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K) /
    (↑(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]
-- 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∞)
⊢ ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have 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∞)
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∞)
⊢ ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ rexp (-convexBodySumFun x)) /
      (↑(finrank ℚ K).factorial : ℝ≥0∞) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
have 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∞)
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∞)
⊢ 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]