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
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
simp_rw :
  (Measure.prod volume volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-1) 1) : ℝ≥0∞)
      ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) :
        ℝ≥0∞) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₂ :
  ENNReal.ofReal (HSub.hSub (α := ℝ) 1 (-1)) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 - -HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₃ :
  ENNReal.ofReal (HAdd.hAdd (α := ℝ) 1 1) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₄ :
  ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₅ : ENNReal.ofReal 2 * ENNReal.ofReal (2 * HPow.hPow (β := ℕ) (↑B : ℝ) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ (volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
have simp_rw₆ : ENNReal.ofReal 2 * (ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) =
  4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
Tactic: simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
        ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
        ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
simp_rw :
  (Measure.prod volume volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-1) 1) : ℝ≥0∞)
      ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) :
        ℝ≥0∞) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₂ :
  ENNReal.ofReal (HSub.hSub (α := ℝ) 1 (-1)) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 - -HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₃ :
  ENNReal.ofReal (HAdd.hAdd (α := ℝ) 1 1) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₄ :
  ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₅ : ENNReal.ofReal 2 * ENNReal.ofReal (2 * HPow.hPow (β := ℕ) (↑B : ℝ) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₆ :
  ENNReal.ofReal 2 * (ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ (volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
have simp_rw₇ : ENNReal.ofReal 2 * (ENNReal.ofReal 2 * HPow.hPow (β := ℕ) (ENNReal.ofReal (↑B : ℝ)) 2) =
  4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
Tactic: simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
        ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
        ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
simp_rw :
  (Measure.prod volume volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-1) 1) : ℝ≥0∞)
      ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) :
        ℝ≥0∞) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₂ :
  ENNReal.ofReal (HSub.hSub (α := ℝ) 1 (-1)) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 - -HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₃ :
  ENNReal.ofReal (HAdd.hAdd (α := ℝ) 1 1) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₄ :
  ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₅ : ENNReal.ofReal 2 * ENNReal.ofReal (2 * HPow.hPow (β := ℕ) (↑B : ℝ) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₆ :
  ENNReal.ofReal 2 * (ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₇ :
  ENNReal.ofReal 2 * (ENNReal.ofReal 2 * HPow.hPow (β := ℕ) (ENNReal.ofReal (↑B : ℝ)) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ (volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
have simp_rw₈ : 2 * (2 * HPow.hPow (β := ℕ) (ENNReal.ofReal (↑B : ℝ)) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
Tactic: simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
        ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
        ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
simp_rw :
  (Measure.prod volume volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-1) 1) : ℝ≥0∞)
      ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) :
        ℝ≥0∞) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₂ :
  ENNReal.ofReal (HSub.hSub (α := ℝ) 1 (-1)) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 - -HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₃ :
  ENNReal.ofReal (HAdd.hAdd (α := ℝ) 1 1) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₄ :
  ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₅ : ENNReal.ofReal 2 * ENNReal.ofReal (2 * HPow.hPow (β := ℕ) (↑B : ℝ) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₆ :
  ENNReal.ofReal 2 * (ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₇ :
  ENNReal.ofReal 2 * (ENNReal.ofReal 2 * HPow.hPow (β := ℕ) (ENNReal.ofReal (↑B : ℝ)) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₈ : 2 * (2 * HPow.hPow (β := ℕ) (ENNReal.ofReal (↑B : ℝ)) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ (volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
have simp_rw₉ : 2 * (2 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
Tactic: simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
        ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
        ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
simp_rw :
  (Measure.prod volume volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-1) 1) : ℝ≥0∞)
      ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) :
        ℝ≥0∞) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₂ :
  ENNReal.ofReal (HSub.hSub (α := ℝ) 1 (-1)) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 - -HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₃ :
  ENNReal.ofReal (HAdd.hAdd (α := ℝ) 1 1) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₄ :
  ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₅ : ENNReal.ofReal 2 * ENNReal.ofReal (2 * HPow.hPow (β := ℕ) (↑B : ℝ) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₆ :
  ENNReal.ofReal 2 * (ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₇ :
  ENNReal.ofReal 2 * (ENNReal.ofReal 2 * HPow.hPow (β := ℕ) (ENNReal.ofReal (↑B : ℝ)) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₈ : 2 * (2 * HPow.hPow (β := ℕ) (ENNReal.ofReal (↑B : ℝ)) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₉ : 2 * (2 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ (volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
have simp_rw₁₀ : HMul.hMul (α := ℝ≥0∞) 2 2 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2 = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
Tactic: simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
        ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
        ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
⊢ NullMeasurableSet (α := ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} volume
have refine_1 : MeasurableSet (α := ℂ) fun (x : ℂ) ↦ Real.lt✝ |x.re| 1
Tactic: refine (MeasurableSet.inter ?_ ?_).nullMeasurableSet
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
refine_1 : MeasurableSet (α := ℂ) fun (x : ℂ) ↦ Real.lt✝ |x.re| 1
⊢ NullMeasurableSet (α := ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} volume
have refine_2 : MeasurableSet (α := ℂ) fun (x : ℂ) ↦ Real.lt✝ |x.im| (HPow.hPow (β := ℕ) (↑B : ℝ) 2)
Tactic: refine (MeasurableSet.inter ?_ ?_).nullMeasurableSet
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀) =
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have vol_box : ∀ (B : ℝ≥0),
  (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
Tactic: have vol_box : ∀ B : ℝ≥0, volume {x : ℂ | |x.re| < 1 ∧ |x.im| < B ^ 2} = 4 * B ^ 2 := by
    intro B
    rw [← (Complex.volume_preserving_equiv_real_prod.symm).measure_preimage]
    · simp_rw [Set.preimage_setOf_eq, Complex.measurableEquivRealProd_symm_apply]
      rw [show {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < B ^ 2} =
        Set.Ioo (-1 : ℝ) (1 : ℝ) ×ˢ Set.Ioo (-(B : ℝ) ^ 2) ((B : ℝ) ^ 2) by
          ext; simp_rw [Set.mem_setOf_eq, Set.mem_prod, Set.mem_Ioo, abs_lt]]
      simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
        ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
        ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
    · refine (MeasurableSet.inter ?_ ?_).nullMeasurableSet
      · exact measurableSet_lt (measurable_norm.comp Complex.measurable_re) measurable_const
      · exact measurableSet_lt (measurable_norm.comp Complex.measurable_im) measurable_const
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀) =
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      ((∏ x ∈ Finset.erase Finset.univ w₀,
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
have simp_rw : HMul.hMul (α := ℝ≥0∞)
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ i : { w : InfinitePlace K // w.IsComplex },
      (volume : (a : Set ℂ) → ℝ≥0∞)
        (if i = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑i : InfinitePlace K)) : ℝ) 2}
        else ball 0 (↑(f (↑i : InfinitePlace K)) : ℝ))) =
  (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
    ((∏ x ∈ Finset.erase Finset.univ w₀,
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
      (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
Tactic: simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ i : { w : InfinitePlace K // w.IsComplex },
        (volume : (a : Set ℂ) → ℝ≥0∞)
          (if i = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑i : InfinitePlace K)) : ℝ) 2}
          else ball 0 (↑(f (↑i : InfinitePlace K)) : ℝ))) =
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      ((∏ x ∈ Finset.erase Finset.univ w₀,
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
have rw : (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (∏ x ∈ Finset.erase Finset.univ w₀,
          (volume : (a : Set ℂ) → ℝ≥0∞)
            (if x = w₀ then {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
            else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)) :
        ℝ≥0∞)
      ((volume : (a : Set ℂ) → ℝ≥0∞)
          (if w₀ = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2}
          else ball 0 (↑(f (↑w₀ : InfinitePlace K)) : ℝ)) :
        ℝ≥0∞) =
  (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
    ((∏ x ∈ Finset.erase Finset.univ w₀,
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
      (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
Tactic: rw [← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (∏ x ∈ Finset.erase Finset.univ w₀,
            (volume : (a : Set ℂ) → ℝ≥0∞)
              (if x = w₀ then
                {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
              else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)) :
          ℝ≥0∞)
        ((volume : (a : Set ℂ) → ℝ≥0∞)
            (if w₀ = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2}
            else ball 0 (↑(f (↑w₀ : InfinitePlace K)) : ℝ)) :
          ℝ≥0∞) =
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      ((∏ x ∈ Finset.erase Finset.univ w₀,
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
have e_a : Eq (α := ℝ≥0∞)
  (∏ x ∈ Finset.erase Finset.univ w₀,
    (volume : (a : Set ℂ) → ℝ≥0∞)
      (if x = w₀ then {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
      else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)))
  (∏ x ∈ Finset.erase Finset.univ w₀,
    HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
e_a :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ w₀,
      (volume : (a : Set ℂ) → ℝ≥0∞)
        (if x = w₀ then {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
        else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ x ∈ Finset.erase Finset.univ w₀,
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
⊢ (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (∏ x ∈ Finset.erase Finset.univ w₀,
            (volume : (a : Set ℂ) → ℝ≥0∞)
              (if x = w₀ then
                {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
              else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)) :
          ℝ≥0∞)
        ((volume : (a : Set ℂ) → ℝ≥0∞)
            (if w₀ = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2}
            else ball 0 (↑(f (↑w₀ : InfinitePlace K)) : ℝ)) :
          ℝ≥0∞) =
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      ((∏ x ∈ Finset.erase Finset.univ w₀,
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
have e_a₁ : (volume : (a : Set ℂ) → ℝ≥0∞)
    (if w₀ = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2}
    else ball 0 (↑(f (↑w₀ : InfinitePlace K)) : ℝ)) =
  4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ w₀,
      (volume : (a : Set ℂ) → ℝ≥0∞)
        (if x = w₀ then {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
        else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ x ∈ Finset.erase Finset.univ w₀,
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
have e_a : ∀ (w' : { w : InfinitePlace K // w.IsComplex }) (hw' : w' ∈ Finset.erase Finset.univ w₀),
  (volume : (a : Set ℂ) → ℝ≥0∞)
      (if w' = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w' : InfinitePlace K)) : ℝ) 2}
      else ball 0 (↑(f (↑w' : InfinitePlace K)) : ℝ)) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)
Tactic: refine Finset.prod_congr rfl (fun w' hw' ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
w' : { w : InfinitePlace K // w.IsComplex }
hw' : w' ∈ Finset.erase Finset.univ w₀
⊢ (volume : (a : Set ℂ) → ℝ≥0∞)
      (if w' = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w' : InfinitePlace K)) : ℝ) 2}
      else ball 0 (↑(f (↑w' : InfinitePlace K)) : ℝ)) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)
have e_a : (volume : (a : Set ℂ) → ℝ≥0∞) (ball 0 (↑(f (↑w' : InfinitePlace K)) : ℝ)) =
  HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)
Tactic: rw [if_neg (Finset.ne_of_mem_erase hw'), Complex.volume_ball]