awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
      Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
        x
pos :
  ∀ (x : realSpace K) (hx₀ : x = 0),
    Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
      Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
        x
⊢ Eq (α := Set (realSpace K)) (compactSet K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
have neg : ∀ (x : realSpace K) (hx₀ : ¬x = 0),
  Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
Tactic: classical
  ext x
  by_cases hx₀ : x = 0
  · simpa [hx₀] using zero_mem_compactSet K
  · refine ⟨fun hx ↦ Set.mem_union_left _ (compactSet_eq_union_aux₁ hx₀ hx), fun hx ↦ ?_⟩
    simp only [Set.union_singleton, Set.mem_insert_iff, hx₀, false_or] at hx
    exact compactSet_eq_union_aux₂ hx₀ hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) (compactSet K)
have rw : Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))
  ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
Tactic: rw [compactSet_eq_union]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (mixedSpace K)) (closure (normLeOne K)) (normAtAllPlaces ⁻¹' compactSet K)
have rw : Subset (α := Set (mixedSpace K))
  (closure (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
  (normAtAllPlaces ⁻¹' compactSet K)
Tactic: rw [normLeOne_eq_preimage]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (mixedSpace K))
    (closure (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
    (normAtAllPlaces ⁻¹' compactSet K)
have refine : Subset (α := Set (realSpace K)) (closure ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)) (compactSet K)
Tactic: refine ((continuous_normAtAllPlaces K).closure_preimage_subset _).trans (Set.preimage_mono ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (realSpace K)) (closure ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)) (compactSet K)
have refine : Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) (compactSet K)
Tactic: refine (isCompact_compactSet K).isClosed.closure_subset_iff.mpr ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ compactSet K =ᶠ[ae (F := Measure (realSpace K)) volume]
    (↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)
have rw : (↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0} =ᶠ[ae (F := Measure (realSpace K)) volume]
  (↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)
Tactic: rw [compactSet_eq_union]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsBounded (α := mixedSpace K) (normLeOne K)
have rw : IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
Tactic: rw [normLeOne_eq_preimage]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
⊢ IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
have obtain : ∀ (C : ℝ)
  (hC :
    ∀ (x : realSpace K),
      Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C),
  IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
Tactic: obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
C : ℝ
hC :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C
⊢ IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
have refine : ∀ (x : mixedSpace K)
  (hx :
    Membership.mem (γ := Set (mixedSpace K))
      (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x),
  ‖x‖ ≤ C
Tactic: refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
C : ℝ
hC :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C
x : mixedSpace K
hx :
  Membership.mem (γ := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
⊢ ‖x‖ ≤ C
have rw : (sup' univ sorry fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x) ≤ C
Tactic: rw [norm_eq_sup'_normAtPlace]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
C : ℝ
hC :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C
x : mixedSpace K
hx :
  Membership.mem (γ := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
⊢ (sup' univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x) ≤ C
have refine : ∀ (w : InfinitePlace K),
  Membership.mem (γ := Finset (InfinitePlace K)) univ w → (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤ C
Tactic: refine sup'_le _ _ fun w _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
have suffices : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
Tactic: suffices IsBounded (expMapBasis '' paramSet K) by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
have refine : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))
Tactic: refine IsBounded.subset ?_ (Set.image_mono subset_closure)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsBounded (α := mixedSpace K) (normLeOne K)
have rw : IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
Tactic: classical
  rw [normLeOne_eq_preimage]
  suffices IsBounded (expMapBasis '' paramSet K) by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w
  refine IsBounded.subset ?_ (Set.image_mono subset_closure)
  exact (isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw rw₁ rw₂ :
  IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
⊢ IsBounded (α := mixedSpace K) (normLeOne K)
have rw₃ : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
Tactic: classical
  rw [normLeOne_eq_preimage]
  suffices IsBounded (expMapBasis '' paramSet K) by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w
  refine IsBounded.subset ?_ (Set.image_mono subset_closure)
  exact (isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw rw₁ rw₂ :
  IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
rw₃ : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
⊢ IsBounded (α := mixedSpace K) (normLeOne K)
have rw₄ : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))
Tactic: classical
  rw [normLeOne_eq_preimage]
  suffices IsBounded (expMapBasis '' paramSet K) by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w
  refine IsBounded.subset ?_ (Set.image_mono subset_closure)
  exact (isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normLeOne K) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
have 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∞) *
      ∫⁻ (x : realSpace K) in paramSet K,
        ENNReal.ofReal (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ))) *
            (∏ i : { w : InfinitePlace K // w.IsComplex },
                ENNReal.ofReal
                  ((↑expMapBasis : realSpace K → realSpace K) (fun (w : InfinitePlace K) ↦ x w)
                    (↑i : InfinitePlace K)))⁻¹ *
          ∏ w : { w : InfinitePlace K // w.IsComplex },
            ENNReal.ofReal ((↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))) =
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
Tactic: rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral (normLeOne_eq_preimage_image K).symm
    (measurableSet_normLeOne K), normLeOne_eq_preimage,
    normAtAllPlaces_image_preimage_expMapBasis,
    setLIntegral_expMapBasis_image (measurableSet_paramSet K) (by fun_prop)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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) : ℝ))) *
              (∏ i : { w : InfinitePlace K // w.IsComplex },
                  ENNReal.ofReal
                    ((↑expMapBasis : realSpace K → realSpace K) (fun (w : InfinitePlace K) ↦ x w)
                      (↑i : InfinitePlace K)))⁻¹ *
            ∏ w : { w : InfinitePlace K // w.IsComplex },
              ENNReal.ofReal ((↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
have simp_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∞) *
      ∫⁻ (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: simp_rw [ENNReal.inv_mul_cancel_right
    (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ ofReal_ne_zero_iff.mpr (expMapBasis_pos _ _))
    (prod_ne_top fun _ _ ↦ ofReal_ne_top)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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) * 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)
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)]
-- 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)
⊢ 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) * (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)
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)]
-- 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)
⊢ 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) *
      (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)
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)]
-- 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)
⊢ 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) * (↑(finrank ℚ K) : ℝ≥0∞) *
      (↑(finrank ℚ K) : ℝ≥0∞)⁻¹) =
  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)]