-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
rw :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' normAtAllPlaces ⁻¹' compactSet K,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
rw₁ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in compactSet K,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
rw₂ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in compactSet K,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in
        normAtAllPlaces '' normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K),
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
rw₃ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in compactSet K,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K),
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
⊢ Eq (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K)) :
      ℝ≥0∞)
have rw₄ : HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in (↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K),
      ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K),
      ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
Tactic: rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₁,
    normAtAllPlaces_image_preimage_of_nonneg (fun x a w ↦ nonneg_of_mem_compactSet K a w),
    volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₂,
    normAtAllPlaces_image_preimage_expMapBasis, setLIntegral_congr (compactSet_ae K),
    setLIntegral_expMapBasis_image measurableSet_closure (by fun_prop),
    setLIntegral_expMapBasis_image measurableSet_interior (by fun_prop),
    setLIntegral_congr (closure_paramSet_ae_interior K)]