-- 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))
_₁ :
  (∏ 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))
⊢ ((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 _₂ : ((↑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
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]