-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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)
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)
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 Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
rw₇ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) *
      (HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K *
        ENNReal.ofReal (regulator K)) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
rw₈ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K))⁻¹ *
      (HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K *
        ENNReal.ofReal (regulator K)) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
rw₉ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K))⁻¹ *
        (HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K) *
      ENNReal.ofReal (regulator K) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
rw₁₀ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K))⁻¹ *
          HPow.hPow (α := ℝ≥0∞) 2 (nrComplexPlaces K) *
        ENNReal.ofReal Real.pi ^ nrComplexPlaces K *
      ENNReal.ofReal (regulator K) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
rw₁₁ rw₁₂ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal Real.pi ^ 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)

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)]

Premises used: Iff.mpr, ENNReal.ofNat_ne_top, mul_mul_mul_comm, ENNReal.ofReal_mul, ENNReal.natCast_ne_top, ENNReal.pow_ne_top, mul_assoc, ENNReal.mul_inv_cancel_right, pow_ne_zero, ENNReal.ofReal_ofNat, LT.lt.ne', NNReal.coe_real_pi, two_ne_zero, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp, ENNReal.coe_nnreal_eq, zero_le_two, mul_pow, ENNReal.inv_pow, Module.finrank_pos, ENNReal.inv_mul_cancel_right, Nat.cast_ne_zero