-- 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∞))
⊢ ((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∞) (β := ℝ≥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∞))
Tactic: simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]