-- 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∞))
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∞))
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∞)
        (∏ x : { w : InfinitePlace K // w.IsReal }, (↑(HPow.hPow (β := ℕ) (f (↑x : InfinitePlace K)) 1) : ℝ≥0∞))
        (∏ a : { w : InfinitePlace K // w.IsComplex },
          (↑(f (↑a : InfinitePlace K) ^ (↑a : 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∞) *
      HMul.hMul (α := ℝ≥0∞)
        (∏ x : { w : InfinitePlace K // w.IsReal }, (↑(HPow.hPow (β := ℕ) (f (↑x : InfinitePlace K)) 1) : ℝ≥0∞))
        (∏ x : { w : InfinitePlace K // w.IsComplex }, (↑(HPow.hPow (β := ℕ) (f (↑x : InfinitePlace K)) 2) : ℝ≥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∞) *
      HMul.hMul (α := ℝ≥0∞) (∏ x : { w : InfinitePlace K // w.IsReal }, (↑(f (↑x : InfinitePlace K)) : ℝ≥0∞))
        (∏ x : { w : InfinitePlace K // w.IsComplex }, (↑(HPow.hPow (β := ℕ) (f (↑x : InfinitePlace K)) 2) : ℝ≥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₆ : ((↑2 : ℝ≥0∞) ^ (nrRealPlaces K + 2) * (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
      ∏ 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 =
  (↑2 : ℝ≥0∞) ^ (nrRealPlaces K + 2) * (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
    HMul.hMul (α := ℝ≥0∞) (∏ x : { w : InfinitePlace K // w.IsReal }, (↑(f (↑x : InfinitePlace K)) : ℝ≥0∞))
      (∏ x : { w : InfinitePlace K // w.IsComplex }, HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ≥0∞) 2)
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]