-- 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)ˣ
rw :
  Measure.real.{u_1} (α := mixedSpace K) (m := Prod.instMeasurableSpace) (volume : Measure (mixedSpace K))
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
        (fractionalIdealLatticeBasis K I)) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
rw₁ :
  ENNReal.toReal
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K :=
          ℝ) (fractionalIdealLatticeBasis K I))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
rw₂ :
  (HMul.hMul (β := ℝ≥0∞)
        (ENNReal.ofReal
          (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
        (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
            (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
          ℝ≥0∞)).toReal =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
rw₃ :
  (ENNReal.ofReal
          (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞))).toReal =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (idealLattice K I) (volume : Measure (mixedSpace K)) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
have rw₄ : (ENNReal.ofReal
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) :
          ℝ)).toReal *
    (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)).toReal =
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
    √|(↑(discr K) : ℝ)|
Tactic: rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_idealLattice K I),
    measureReal_def,
    volume_fundamentalDomain_fractionalIdealLatticeBasis, volume_fundamentalDomain_latticeBasis,
    ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_inv, toReal_ofNat,
    ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm, Int.norm_eq_abs,
    ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.val)), mul_assoc]