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
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₀
e_a :
  (volume : (a : Set ℂ) → ℝ≥0∞) (ball 0 (↑(f (↑w' : InfinitePlace K)) : ℝ)) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥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)) : ℝ)) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)
have e_a₁ : HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞) =
  HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)
Tactic: rw [if_neg (Finset.ne_of_mem_erase hw'), Complex.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
⊢ (∏ 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)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
          (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
have simp_rw : (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal 2 * ENNReal.ofReal (↑(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)) =
  ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
      ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
        (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
      (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
Tactic: simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, ofReal_ofNat,
        ofReal_coe_nnreal, coe_ofNat]
-- 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
simp_rw :
  (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal 2 * ENNReal.ofReal (↑(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)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
          (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
⊢ (∏ 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)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
          (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
have simp_rw₁ : HMul.hMul (α := ℝ≥0∞) (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal 2)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    (HMul.hMul (α := ℝ≥0∞)
        (∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2)
        (∏ x ∈ Finset.erase Finset.univ w₀, (↑pi : ℝ≥0∞)) *
      (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2)) =
  ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
      ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
        (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
      (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
Tactic: simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, ofReal_ofNat,
        ofReal_coe_nnreal, coe_ofNat]
-- 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
⊢ ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
          (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2)) =
    ((↑(convexBodyLT'Factor K) : ℝ≥0∞) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2
have rw : ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
      ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
        (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
      (HPow.hPow (β := ℕ) (↑2 : ℝ≥0∞) 2 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2)) =
  ((↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * HPow.hPow (α := ℝ≥0) (β := ℕ) 2 2 * pi ^ (nrComplexPlaces K - 1)) :
        ℝ≥0∞) *
      ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
      HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2)
Tactic: rw [show (4 : ℝ≥0∞) = (2 : ℝ≥0) ^ 2 by norm_num, convexBodyLT'Factor, pow_add,
        ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀), ofReal_coe_nnreal]
-- 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
⊢ ((↑(convexBodyLT'Factor K) : ℝ≥0∞) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 =
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have simp_rw : ((↑(convexBodyLT'Factor K) : ℝ≥0∞) *
      ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    ∏ x : { w : InfinitePlace K // w.IsComplex },
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 =
  (↑(convexBodyLT'Factor K) : ℝ≥0∞) *
    (↑(HMul.hMul (α := ℝ≥0)
          (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)
          (∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)) :
      ℝ≥0∞)
Tactic: simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal, mul_assoc]
-- 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
simp_rw :
  ((↑(convexBodyLT'Factor K) : ℝ≥0∞) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 =
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) *
      (↑(HMul.hMul (α := ℝ≥0)
            (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)
            (∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)) :
        ℝ≥0∞)
⊢ ((↑(convexBodyLT'Factor K) : ℝ≥0∞) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 =
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have simp_rw₁ : ((↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K + 2)) : ℝ≥0∞) * (↑(pi ^ (nrComplexPlaces K - 1)) : ℝ≥0∞) *
      ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    ∏ x : { w : InfinitePlace K // w.IsComplex },
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 =
  (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K + 2)) : ℝ≥0∞) * (↑(pi ^ (nrComplexPlaces K - 1)) : ℝ≥0∞) *
    ((↑(∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) : ℝ≥0∞) *
      (↑(∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) : ℝ≥0∞))
Tactic: simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal, mul_assoc]
-- 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
simp_rw :
  ((↑(convexBodyLT'Factor K) : ℝ≥0∞) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 =
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) *
      (↑(HMul.hMul (α := ℝ≥0)
            (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)
            (∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)) :
        ℝ≥0∞)
simp_rw₁ :
  ((↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K + 2)) : ℝ≥0∞) * (↑(pi ^ (nrComplexPlaces K - 1)) : ℝ≥0∞) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K + 2)) : ℝ≥0∞) * (↑(pi ^ (nrComplexPlaces K - 1)) : ℝ≥0∞) *
      ((↑(∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) : ℝ≥0∞) *
        (↑(∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) :
          ℝ≥0∞))
⊢ ((↑(convexBodyLT'Factor K) : ℝ≥0∞) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 =
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have simp_rw₂ : ((↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K + 2)) : ℝ≥0∞) * (↑(pi ^ (nrComplexPlaces K - 1)) : ℝ≥0∞) *
      ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    ∏ x : { w : InfinitePlace K // w.IsComplex },
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 =
  (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K + 2)) : ℝ≥0∞) * (↑(pi ^ (nrComplexPlaces K - 1)) : ℝ≥0∞) *
    HMul.hMul (α := ℝ≥0∞)
      (∏ a : { w : InfinitePlace K // w.IsReal }, (↑(f (↑a : InfinitePlace K) ^ (↑a : InfinitePlace K).mult) : ℝ≥0∞))
      (∏ a : { w : InfinitePlace K // w.IsComplex }, (↑(f (↑a : InfinitePlace K) ^ (↑a : InfinitePlace K).mult) : ℝ≥0∞))
Tactic: simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal, mul_assoc]
-- 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₀) =
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have _ : ((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))
Tactic: calc
    _ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
          ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal (f x.val) ^ 2 * pi) *
          (4 * (f w₀) ^ 2)) := by
      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball]
      rw [← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
      congr 2
      · refine Finset.prod_congr rfl (fun w' hw' ↦ ?_)
        rw [if_neg (Finset.ne_of_mem_erase hw'), Complex.volume_ball]
      · simpa only [ite_true] using vol_box (f w₀)
    _ = ((2 : ℝ≥0) ^ nrRealPlaces K *
          (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))) *
            ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal (f x.val) ^ 2) *
              ↑pi ^ (nrComplexPlaces K - 1) * (4 * (f w₀) ^ 2)) := by
      simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, ofReal_ofNat,
        ofReal_coe_nnreal, coe_ofNat]
    _ = convexBodyLT'Factor K * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))
        * (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2) := by
      rw [show (4 : ℝ≥0∞) = (2 : ℝ≥0) ^ 2 by norm_num, convexBodyLT'Factor, pow_add,
        ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀), ofReal_coe_nnreal]
      simp_rw [coe_mul, ENNReal.coe_pow]
      ring
    _ = convexBodyLT'Factor K * ∏ w, (f w) ^ (mult w) := by
      simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ convexBodySumFun x =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
have simp_rw : ∑ w : InfinitePlace K,
    HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) =
  ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
    HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
Tactic: simp_rw [convexBodySumFun_apply, sum_eq_sum_add_sum, mult_isReal, mult_isComplex,
    Nat.cast_one, one_mul, Nat.cast_ofNat, normAtPlace_apply_of_isReal (Subtype.prop _),
    normAtPlace_apply_of_isComplex (Subtype.prop _), Finset.mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
simp_rw :
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
⊢ convexBodySumFun x =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
have simp_rw₁ : HAdd.hAdd (α := ℝ)
    (∑ w : { w : InfinitePlace K // w.IsReal },
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
        ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
    (∑ w : { w : InfinitePlace K // w.IsComplex },
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
        ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
  ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
    HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
Tactic: simp_rw [convexBodySumFun_apply, sum_eq_sum_add_sum, mult_isReal, mult_isComplex,
    Nat.cast_one, one_mul, Nat.cast_ofNat, normAtPlace_apply_of_isReal (Subtype.prop _),
    normAtPlace_apply_of_isComplex (Subtype.prop _), Finset.mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
simp_rw :
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₁ :
  HAdd.hAdd (α := ℝ)
      (∑ w : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ w : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
⊢ convexBodySumFun x =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
have simp_rw₂ : HAdd.hAdd (α := ℝ)
    (∑ x_1 : { w : InfinitePlace K // w.IsReal },
      HMul.hMul (α := ℝ) (β := ℝ) ((↑1 : ℝ) : ℝ)
        ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
    (∑ w : { w : InfinitePlace K // w.IsComplex },
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
        ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
  ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
    HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
Tactic: simp_rw [convexBodySumFun_apply, sum_eq_sum_add_sum, mult_isReal, mult_isComplex,
    Nat.cast_one, one_mul, Nat.cast_ofNat, normAtPlace_apply_of_isReal (Subtype.prop _),
    normAtPlace_apply_of_isComplex (Subtype.prop _), Finset.mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
simp_rw :
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₁ :
  HAdd.hAdd (α := ℝ)
      (∑ w : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ w : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₂ :
  HAdd.hAdd (α := ℝ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑1 : ℝ) : ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ w : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
⊢ convexBodySumFun x =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
have simp_rw₃ : HAdd.hAdd (α := ℝ)
    (∑ x_1 : { w : InfinitePlace K // w.IsReal },
      HMul.hMul (α := ℝ) (β := ℝ) ((↑1 : ℝ) : ℝ)
        ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
    (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
      HMul.hMul (α := ℝ) (β := ℝ) ((↑2 : ℝ) : ℝ)
        ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
  ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
    HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
Tactic: simp_rw [convexBodySumFun_apply, sum_eq_sum_add_sum, mult_isReal, mult_isComplex,
    Nat.cast_one, one_mul, Nat.cast_ofNat, normAtPlace_apply_of_isReal (Subtype.prop _),
    normAtPlace_apply_of_isComplex (Subtype.prop _), Finset.mul_sum]