-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
_ :
  (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal =
    (↑((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 (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹ =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2
              (HSub.hSub (α := ℤ) (↑(finrank ℚ K) : ℤ) (↑(nrComplexPlaces K) : ℤ) - (↑(nrRealPlaces K) : ℤ) +
                (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      π⁻¹ ^ nrComplexPlaces K
_₂ :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2
              (HSub.hSub (α := ℤ) (↑(finrank ℚ K) : ℤ) (↑(nrComplexPlaces K) : ℤ) - (↑(nrRealPlaces K) : ℤ) +
                (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      π⁻¹ ^ nrComplexPlaces K =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2 (HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      π⁻¹ ^ nrComplexPlaces K
_₃ :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2 (HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      π⁻¹ ^ nrComplexPlaces K =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
          (4 / π) ^ nrComplexPlaces K *
        (↑(finrank ℚ K).factorial : ℝ) *
      √|(↑(discr K) : ℝ)|
⊢ (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
          (4 / π) ^ nrComplexPlaces K *
        (↑(finrank ℚ K).factorial : ℝ) *
      √|(↑(discr K) : ℝ)|

Tactic:
calc
    _ = FractionalIdeal.absNorm I.1 * (2 : ℝ)⁻¹ ^ nrComplexPlaces K * sqrt ‖discr K‖₊ *
          (2 : ℝ) ^ finrank ℚ K * ((2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K /
            (Nat.factorial (finrank ℚ K)))⁻¹ := by
      simp_rw [minkowskiBound, convexBodySumFactor,
        volume_fundamentalDomain_fractionalIdealLatticeBasis,
        volume_fundamentalDomain_latticeBasis, toReal_mul, toReal_pow, toReal_inv, coe_toReal,
        toReal_ofNat, mixedEmbedding.finrank, mul_assoc]
      rw [ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.1))]
      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]
    _ = FractionalIdeal.absNorm I.1 * (2 : ℝ) ^ (finrank ℚ K - nrComplexPlaces K - nrRealPlaces K +
          nrComplexPlaces K : ℤ) * Real.sqrt ‖discr K‖ * Nat.factorial (finrank ℚ K) *
            π⁻¹ ^ (nrComplexPlaces K) := by
      simp_rw [inv_div, div_eq_mul_inv, mul_inv, ← zpow_neg_one, ← zpow_natCast, mul_zpow,
        ← zpow_mul, neg_one_mul, mul_neg_one, neg_neg, Real.coe_sqrt, coe_nnnorm, sub_eq_add_neg,
        zpow_add₀ (two_ne_zero : (2 : ℝ) ≠ 0)]
      ring
    _ = FractionalIdeal.absNorm I.1 * (2 : ℝ) ^ (2 * nrComplexPlaces K : ℤ) * Real.sqrt ‖discr K‖ *
          Nat.factorial (finrank ℚ K) * π⁻¹ ^ (nrComplexPlaces K) := by
      congr
      rw [← card_add_two_mul_card_eq_rank, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat]
      ring
    _ = FractionalIdeal.absNorm I.1 * (4 / π) ^ nrComplexPlaces K * (finrank ℚ K).factorial *
          Real.sqrt |discr K| := by
      rw [Int.norm_eq_abs, zpow_mul, show (2 : ℝ) ^ (2 : ℤ) = 4 by norm_cast, div_pow,
        inv_eq_one_div, div_pow, one_pow, zpow_natCast]
      ring

Premises used: Norm.norm, Int.cast, Units.val, Real.pi, HMul.hMul, abs, NNNorm.nnnorm, Rat, HSub.hSub, FractionalIdeal.absNorm, HDiv.hDiv, NumberField.InfinitePlace.nrRealPlaces, Nat.cast, NNReal.sqrt, HPow.hPow, HAdd.hAdd, Nat.factorial, Real.sqrt, NumberField.discr, NumberField.InfinitePlace.nrComplexPlaces, OfNat.ofNat, DFunLike.coe, Module.finrank