-- 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
simp_rw :
  HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal 2 * ENNReal.ofReal (↑(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)
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 : { w : InfinitePlace K // w.IsComplex },
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2)
        (∏ x : { w : InfinitePlace K // w.IsComplex }, (↑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)
simp_rw₂ :
  (ENNReal.ofReal 2 ^ Finset.card.{u_1} (α := { w : InfinitePlace K // w.IsReal }) Finset.univ *
        ∏ 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∞) ^ Finset.card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) Finset.univ) =
    ((↑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)
simp_rw₃ :
  (ENNReal.ofReal 2 ^ card.{u_1} { w : InfinitePlace K // w.IsReal } *
        ∏ 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∞) ^ card.{u_1} { w : InfinitePlace K // w.IsComplex }) =
    ((↑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)
simp_rw₄ :
  (HPow.hPow (α := ℝ≥0∞) 2 (card.{u_1} { w : InfinitePlace K // w.IsReal }) *
        ∏ 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∞) ^ card.{u_1} { w : InfinitePlace K // w.IsComplex }) =
    ((↑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)
⊢ 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)
have simp_rw₅ : (HPow.hPow (α := ℝ≥0∞) 2 (card.{u_1} { w : InfinitePlace K // w.IsReal }) *
      ∏ 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) *
      (↑pi : ℝ≥0∞) ^ card.{u_1} { w : InfinitePlace K // w.IsComplex }) =
  ((↑2 : ℝ≥0∞) ^ nrRealPlaces K * ∏ 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) *
      (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
Tactic: 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]