-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
        (↑(finrank ℚ K) : ℝ≥0∞)⁻¹) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
rw₁ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (ENNReal.ofReal 2 * ENNReal.ofReal Real.pi) ^ nrComplexPlaces K *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
        (↑(finrank ℚ K) : ℝ≥0∞)⁻¹) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
rw₂ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) *
        (ENNReal.ofReal 2 ^ nrComplexPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K) *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
        (↑(finrank ℚ K) : ℝ≥0∞)⁻¹) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
rw₃ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) *
        (HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K) *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
        (↑(finrank ℚ K) : ℝ≥0∞)⁻¹) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
rw₄ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) *
        (HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K) *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K)) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
⊢ HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
        ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ)))) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
have rw₅ : HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) *
      (HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K) *
    (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K)) =
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (↑NNReal.pi : ℝ) ^ nrComplexPlaces K *
    ENNReal.ofReal (regulator K)
Tactic: rw [setLIntegral_paramSet_exp K Module.finrank_pos, ofReal_mul zero_le_two, mul_pow,
    ofReal_ofNat, ENNReal.mul_inv_cancel_right (Nat.cast_ne_zero.mpr Module.finrank_pos.ne')
    (natCast_ne_top _), coe_nnreal_eq, NNReal.coe_real_pi, mul_mul_mul_comm, ← ENNReal.inv_pow,
    ← mul_assoc, ← mul_assoc, ENNReal.inv_mul_cancel_right (pow_ne_zero _ two_ne_zero)
    (pow_ne_top ENNReal.ofNat_ne_top)]