-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
_ :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
_₁ :
  HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ 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) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
_₂ :
  ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ 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) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥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)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have _₃ : (↑(convexBodyLTFactor K) : ℝ≥0∞) *
    HMul.hMul (α := ℝ≥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) =
  (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
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 simp : 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_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]