-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal ^ HDiv.hDiv (α := ℝ) 1 (↑(finrank ℚ K) : ℝ)
h_le : minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
x : K
simp_rw :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (pi / 2) ^ nrComplexPlaces K /
                    (↑(finrank ℚ K).factorial : ℝ≥0)) :
                ℝ)⁻¹))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹)))
simp_rw₁ :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            ((↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (pi / 2) ^ nrComplexPlaces K) : ℝ) /
                (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ))⁻¹))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹)))
simp_rw₂ :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            ((↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ) * (↑((pi / 2) ^ nrComplexPlaces K) : ℝ) /
                (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ))⁻¹))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹)))
simp_rw₃ :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            ((↑2 : ℝ) ^ nrRealPlaces K * (↑(pi / 2) : ℝ) ^ nrComplexPlaces K /
                (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ))⁻¹))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹)))
⊢ (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (pi / 2) ^ nrComplexPlaces K /
                    (↑(finrank ℚ K).factorial : ℝ≥0))⁻¹ :
              ℝ)))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹)))
have simp_rw₄ : (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
    (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
        (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
          ((↑2 : ℝ) ^ nrRealPlaces K * ((↑pi : ℝ) / (↑2 : ℝ)) ^ nrComplexPlaces K /
              (↑(↑(finrank ℚ K).factorial : ℝ≥0) : ℝ))⁻¹))) =
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
    (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
        (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
          (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹)))
Tactic: simp_rw [NNReal.coe_inv, NNReal.coe_div, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_div,
        coe_real_pi, NNReal.coe_ofNat, NNReal.coe_natCast]