-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodyLT_volume :
    volume (convexBodyLT K f) = (convexBodyLTFactor K) * ∏ w, (f w) ^ (mult w)

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (↑2 ^ nrRealPlaces K * ∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ nrComplexPlaces K) =
    ↑(convexBodyLTFactor K) *
      ((∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) * ∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2)

Tactic:
simp_rw [convexBodyLTFactor, coe_mul, ENNReal.coe_pow]

Result:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (↑2 ^ nrRealPlaces K * ∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ nrComplexPlaces K) =
    ↑2 ^ nrRealPlaces K * ↑pi ^ nrComplexPlaces K *
      ((∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) * ∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2)

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ volume (convexBodyLT K f) = ↑(convexBodyLTFactor K) * ↑(∏ w : InfinitePlace K, f w ^ w.mult)

Tactic:
calc
  _ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
        ∏ x : {w // InfinitePlace.IsComplex w}, ENNReal.ofReal (f x.val) ^ 2 * NNReal.pi := by
    simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
  _ = ((2 : ℝ≥0) ^ nrRealPlaces K
        * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val)))
        * ((∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2) *
          NNReal.pi ^ nrComplexPlaces K) := by
    simp_rw [ofReal_mul (by norm_num : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
      Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
  _ = (convexBodyLTFactor K) * ((∏ x : {w // InfinitePlace.IsReal w}, .ofReal (f x.val)) *
      (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by
    simp_rw [convexBodyLTFactor, coe_mul, ENNReal.coe_pow]
    ring
  _ = (convexBodyLTFactor K) * ∏ w, (f w) ^ (mult w) := by
    simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finset_prod, mult_isReal, mult_isComplex,
      pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ volume (convexBodyLT K f) =
    (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi

Tactic:
simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ ↑(convexBodyLTFactor K) *
      ((∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) * ∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2) =
    ↑(convexBodyLTFactor K) * ↑(∏ w : InfinitePlace K, f w ^ w.mult)

Tactic:
simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finset_prod, mult_isReal, mult_isComplex,
  pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ 0 ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (↑2 ^ nrRealPlaces K * ∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ nrComplexPlaces K) =
    ↑2 ^ nrRealPlaces K * ↑pi ^ nrComplexPlaces K *
      ((∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) * ∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2)

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi =
    (↑2 ^ nrRealPlaces K * ∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x : { w // w.IsComplex }, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ nrComplexPlaces K)

Tactic:
simp_rw [ofReal_mul (by norm_num : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
  Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]

Result:
no goals