-- 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 :
  ((Measure.prod volume volume :
          Measure (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ))) :
        (a : Set (mixedSpace K)) → ℝ≥0∞)
      (convexBodyLT K f) =
    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∞))
simp_rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((volume : Measure ({ w : InfinitePlace K // w.IsReal } → ℝ)) :
            (a : Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) Set.univ
            fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ball 0 (↑(f (↑w : InfinitePlace K)) : ℝ)) :
        ℝ≥0∞)
      (((volume : Measure ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
            (a : Set ({ w : InfinitePlace K // w.IsComplex } → ℂ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ) Set.univ
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ ball 0 (↑(f (↑w : InfinitePlace K)) : ℝ)) :
        ℝ≥0∞) =
    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∞))
simp_rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((Measure.pi (α := fun (i : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                fun (x : { w : InfinitePlace K // w.IsReal }) ↦ volume :
              Measure ((i : { w : InfinitePlace K // w.IsReal }) → ℝ)) :
            (a : Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) Set.univ
            fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ball 0 (↑(f (↑w : InfinitePlace K)) : ℝ)) :
        ℝ≥0∞)
      (((Measure.pi (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ volume :
              Measure ((i : { w : InfinitePlace K // w.IsComplex }) → ℂ)) :
            (a : Set ({ w : InfinitePlace K // w.IsComplex } → ℂ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ) Set.univ
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ ball 0 (↑(f (↑w : InfinitePlace K)) : ℝ)) :
        ℝ≥0∞) =
    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∞))
simp_rw₃ :
  HMul.hMul (α := ℝ≥0∞)
      (∏ i : { w : InfinitePlace K // w.IsReal },
        (volume : (a : Set ℝ) → ℝ≥0∞) (ball 0 (↑(f (↑i : InfinitePlace K)) : ℝ)))
      (∏ i : { w : InfinitePlace K // w.IsComplex },
        (volume : (a : Set ℂ) → ℝ≥0∞) (ball 0 (↑(f (↑i : InfinitePlace 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∞))
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    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∞))
have simp_rw₄ : HMul.hMul (α := ℝ≥0∞)
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ i : { w : InfinitePlace K // w.IsComplex },
      (volume : (a : Set ℂ) → ℝ≥0∞) (ball 0 (↑(f (↑i : InfinitePlace 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∞))
Tactic: simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]