-- 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 :
  (↑(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∞) *
      (↑(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)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces 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) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥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)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces 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) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥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)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces 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) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥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)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces 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) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥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)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces 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) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥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∞))
⊢ (↑(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∞)
have simp_rw₆ : (↑2 : ℝ≥0∞) ^ nrRealPlaces K * (↑pi : ℝ≥0∞) ^ nrComplexPlaces K *
    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) =
  (↑2 : ℝ≥0∞) ^ nrRealPlaces K * (↑pi : ℝ≥0∞) ^ nrComplexPlaces K *
    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]