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