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
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)
⊢ 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)) =
  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 (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)
have h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
Tactic: have h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K) :=
    (isCompact_compactSet K).measurableSet.preimage (continuous_normAtAllPlaces K).measurable
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
⊢ MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
have refine : MeasurableSet (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
Tactic: refine MeasurableSet.preimage ?_ (continuous_normAtAllPlaces K).measurable
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
⊢ MeasurableSet (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
have refine : MeasurableSet (α := realSpace K) (interior (paramSet K))
Tactic: refine MeasurableSet.image_of_continuousOn_injOn ?_ (continuous_expMapBasis K).continuousOn
      (injective_expMapBasis K).injOn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)
have h₂ : MeasurableSet (α := mixedSpace K)
  (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
Tactic: have h₂ : MeasurableSet (normAtAllPlaces ⁻¹' expMapBasis '' interior (paramSet K)) := by
    refine MeasurableSet.preimage ?_ (continuous_normAtAllPlaces K).measurable
    refine MeasurableSet.image_of_continuousOn_injOn ?_ (continuous_expMapBasis K).continuousOn
      (injective_expMapBasis K).injOn
    exact measurableSet_interior
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)
  (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
Tactic: refine le_antisymm (measure_mono interior_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
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ LE.le (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞)
  (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
  (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
Tactic: refine (measure_mono (closure_normLeOne_subset K)).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ LE.le (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
have refine : Eq (α := ℝ≥0∞)
  (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
  (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K)) :
    ℝ≥0∞)
Tactic: refine le_of_eq_of_le ?_ (measure_mono (subset_interior_normLeOne K))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ Eq (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K)) :
      ℝ≥0∞)
have rw : HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in normAtAllPlaces '' normAtAllPlaces ⁻¹' compactSet K,
      ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
Tactic: rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₁,
    normAtAllPlaces_image_preimage_of_nonneg (fun x a w ↦ nonneg_of_mem_compactSet K a w),
    volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₂,
    normAtAllPlaces_image_preimage_expMapBasis, setLIntegral_congr (compactSet_ae K),
    setLIntegral_expMapBasis_image measurableSet_closure (by fun_prop),
    setLIntegral_expMapBasis_image measurableSet_interior (by fun_prop),
    setLIntegral_congr (closure_paramSet_ae_interior K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
rw :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' normAtAllPlaces ⁻¹' compactSet K,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ Eq (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K)) :
      ℝ≥0∞)
have rw₁ : HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in compactSet K,
      ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
Tactic: rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₁,
    normAtAllPlaces_image_preimage_of_nonneg (fun x a w ↦ nonneg_of_mem_compactSet K a w),
    volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₂,
    normAtAllPlaces_image_preimage_expMapBasis, setLIntegral_congr (compactSet_ae K),
    setLIntegral_expMapBasis_image measurableSet_closure (by fun_prop),
    setLIntegral_expMapBasis_image measurableSet_interior (by fun_prop),
    setLIntegral_congr (closure_paramSet_ae_interior K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
rw :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' normAtAllPlaces ⁻¹' compactSet K,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
rw₁ :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in compactSet K,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ Eq (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K)) :
      ℝ≥0∞)
have rw₂ : HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in compactSet K,
      ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in
      normAtAllPlaces '' normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K),
      ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
Tactic: rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₁,
    normAtAllPlaces_image_preimage_of_nonneg (fun x a w ↦ nonneg_of_mem_compactSet K a w),
    volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₂,
    normAtAllPlaces_image_preimage_expMapBasis, setLIntegral_congr (compactSet_ae K),
    setLIntegral_expMapBasis_image measurableSet_closure (by fun_prop),
    setLIntegral_expMapBasis_image measurableSet_interior (by fun_prop),
    setLIntegral_congr (closure_paramSet_ae_interior K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (frontier (normLeOne K)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have h : Subset (α := Set (mixedSpace K)) (interior (normLeOne K)) (closure (normLeOne K))
Tactic: rw [frontier, measure_diff, volume_interior_eq_volume_closure, tsub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Subset (α := Set (mixedSpace K)) (interior (normLeOne K)) (closure (normLeOne K))
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (frontier (normLeOne K)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have h₂ : NullMeasurableSet (α := mixedSpace K) (interior (normLeOne K)) volume
Tactic: rw [frontier, measure_diff, volume_interior_eq_volume_closure, tsub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Subset (α := Set (mixedSpace K)) (interior (normLeOne K)) (closure (normLeOne K))
h₂ : NullMeasurableSet (α := mixedSpace K) (interior (normLeOne K)) volume
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (frontier (normLeOne K)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have h_fin : Ne (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [frontier, measure_diff, volume_interior_eq_volume_closure, tsub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Ne (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have h_fin : LT.lt (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normLeOne K) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: refine lt_top_iff_ne_top.mp <| lt_of_le_of_lt (measure_mono interior_subset) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LT.lt (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normLeOne K) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have h_fin : HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) < ∞
Tactic: rw [volume_normLeOne]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Measurable (α := realMixedSpace K)
    (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K)
have refine : Measurable.{u_1, u_1} (α := { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) (β :=
  { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
  (↑(PartialEquiv.symm
        (OpenPartialHomeomorph.toPartialEquiv
          (OpenPartialHomeomorph.pi (X := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) (Y :=
            fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
            polarCoord))) :
    ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) → { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
Tactic: refine measurable_fst.prodMk <| Measurable.comp ?_ measurable_snd
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
have this : (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) =
  LinearMap.prodMap LinearMap.id
    (↑(fderivPiPolarCoordSymm x.2) :
      ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
Tactic: have : (FDerivPolarCoordRealSymm K x).toLinearMap =
      LinearMap.prodMap (LinearMap.id) (fderivPiPolarCoordSymm x.2).toLinearMap := rfl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
this :
  (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) =
    LinearMap.prodMap LinearMap.id
      (↑(fderivPiPolarCoordSymm x.2) :
        ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
have rw : Eq (α := ℝ)
  ((LinearMap.det : (a : realMixedSpace K →ₗ[ℝ] realMixedSpace K) → ℝ)
      (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) :
    ℝ)
  (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1 : ℝ)
Tactic: rw [ContinuousLinearMap.det, this, LinearMap.det_prodMap, LinearMap.det_id, one_mul,
    ← ContinuousLinearMap.det, det_fderivPiPolarCoordSymm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
this :
  (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) =
    LinearMap.prodMap LinearMap.id
      (↑(fderivPiPolarCoordSymm x.2) :
        ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
rw :
  Eq (α := ℝ)
    ((LinearMap.det : (a : realMixedSpace K →ₗ[ℝ] realMixedSpace K) → ℝ)
        (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) :
      ℝ)
    (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1 : ℝ)
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
have rw₁ : Eq (α := ℝ)
  ((LinearMap.det : (a : realMixedSpace K →ₗ[ℝ] realMixedSpace K) → ℝ)
      (LinearMap.prodMap LinearMap.id
        (↑(fderivPiPolarCoordSymm x.2) :
          ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) :
    ℝ)
  (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1 : ℝ)
Tactic: rw [ContinuousLinearMap.det, this, LinearMap.det_prodMap, LinearMap.det_id, one_mul,
    ← ContinuousLinearMap.det, det_fderivPiPolarCoordSymm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
this :
  (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) =
    LinearMap.prodMap LinearMap.id
      (↑(fderivPiPolarCoordSymm x.2) :
        ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)
rw :
  Eq (α := ℝ)
    ((LinearMap.det : (a : realMixedSpace K →ₗ[ℝ] realMixedSpace K) → ℝ)
        (↑(FDerivPolarCoordRealSymm K x) : realMixedSpace K →ₗ[ℝ] realMixedSpace K) :
      ℝ)
    (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1 : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((LinearMap.det : (a : realMixedSpace K →ₗ[ℝ] realMixedSpace K) → ℝ)
        (LinearMap.prodMap LinearMap.id
          (↑(fderivPiPolarCoordSymm x.2) :
            ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) :
      ℝ)
    (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1 : ℝ)
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
have rw₂ : HMul.hMul (α := ℝ) (β := ℝ)
    ((LinearMap.det : (a : ({ w : InfinitePlace K // w.IsReal } → ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsReal } → ℝ) → ℝ)
        LinearMap.id :
      ℝ)
    ((LinearMap.det :
          (a : ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →
            ℝ)
        (↑(fderivPiPolarCoordSymm x.2) :
          ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) →ₗ[ℝ] { w : InfinitePlace K // w.IsComplex } → ℝ × ℝ) :
      ℝ) =
  ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1
Tactic: rw [ContinuousLinearMap.det, this, LinearMap.det_prodMap, LinearMap.det_id, one_mul,
    ← ContinuousLinearMap.det, det_fderivPiPolarCoordSymm]