awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
have h : ∀ (hw : w.IsReal), normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
h : ∀ (hw : w.IsReal), normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
have h₁ : ∀ (hw : w.IsComplex), normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsReal
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
have h : ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x).1
    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw) =
  x w
Tactic: rw [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsReal
h :
  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x).1
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw) =
    x w
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
have h₁ : (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)).1
    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw) =
  x w
Tactic: rw [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
have h : norm (E := ℂ)
    (((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x).2
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)) =
  x w
Tactic: rw [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩, mixedSpaceOfRealSpace_apply,
      Complex.norm_of_nonneg (hx w hw)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsComplex
h :
  norm (E := ℂ)
      (((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x).2
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)) =
    x w
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
have h₁ : norm (E := ℂ)
    ((fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)).2
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)) =
  x w
Tactic: rw [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩, mixedSpaceOfRealSpace_apply,
      Complex.norm_of_nonneg (hx w hw)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsComplex
h :
  norm (E := ℂ)
      (((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x).2
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)) =
    x w
h₁ :
  norm (E := ℂ)
      ((fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)).2
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)) =
    x w
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
have h₂ : x w = x w
Tactic: rw [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩, mixedSpaceOfRealSpace_apply,
      Complex.norm_of_nonneg (hx w hw)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 ≤ x w
⊢ normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) = x
have h : ∀ (x_1 : InfinitePlace K), normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) x_1 = x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 ≤ x w
x_1 : InfinitePlace K
⊢ normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) x_1 = x x_1
have h : (normAtPlace x_1 : (a : mixedSpace K) → ℝ)
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) =
  x x_1
Tactic: rw [normAtAllPlaces_apply, normAtPlace_mixedSpaceOfRealSpace (hx _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 ≤ x w
x_1 : InfinitePlace K
h :
  (normAtPlace x_1 : (a : mixedSpace K) → ℝ)
      ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) =
    x x_1
⊢ normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) x_1 = x x_1
have h₁ : x x_1 = x x_1
Tactic: rw [normAtAllPlaces_apply, normAtPlace_mixedSpaceOfRealSpace (hx _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : K
w : InfinitePlace K
⊢ normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) w = (w : (a : K) → ℝ) x
have rw : Eq (α := ℝ)
  ((normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
  ((w : (a : K) → ℝ) x : ℝ)
Tactic: rw [normAtAllPlaces_apply, normAtPlace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : K
w : InfinitePlace K
rw :
  Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
⊢ normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) w = (w : (a : K) → ℝ) x
have rw₁ : Eq (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) ((w : (a : K) → ℝ) x : ℝ)
Tactic: rw [normAtAllPlaces_apply, normAtPlace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
⊢ normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) = normAtAllPlaces x
have h : ∀ (w : InfinitePlace K),
  normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
Tactic: ext w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : InfinitePlace K
⊢ normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
have h : ∀ (hw : w.IsReal),
  normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : InfinitePlace K
h :
  ∀ (hw : w.IsReal),
    normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
⊢ normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
have h₁ : ∀ (hw : w.IsComplex),
  normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
have h : Eq (α := ℝ)
  ((normAtPlace w : (a : mixedSpace K) → ℝ) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) : ℝ)
  ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: simp_rw [normAtAllPlaces, normAtPlace_apply_of_isReal hw, norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : InfinitePlace K
hw : w.IsReal
h :
  Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
have h₁ : ‖‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖‖ =
  ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
Tactic: simp_rw [normAtAllPlaces, normAtPlace_apply_of_isReal hw, norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
⊢ normAtAllPlaces x = normAtAllPlaces y
have h₁ : ∀ (w : InfinitePlace K), normAtAllPlaces x w = normAtAllPlaces y w
Tactic: ext w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
w : InfinitePlace K
⊢ normAtAllPlaces x w = normAtAllPlaces y w
have h₁ : ∀ (hw : w.IsReal), normAtAllPlaces x w = normAtAllPlaces y w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
w : InfinitePlace K
h₁ : ∀ (hw : w.IsReal), normAtAllPlaces x w = normAtAllPlaces y w
⊢ normAtAllPlaces x w = normAtAllPlaces y w
have h₂ : ∀ (hw : w.IsComplex), normAtAllPlaces x w = normAtAllPlaces y w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
⊢ normAtAllPlaces '' normAtAllPlaces ⁻¹' s = s
have rw : s ⊆ Set.range normAtAllPlaces
Tactic: rw [Set.image_preimage_eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
x : realSpace K
hx : x ∈ s
⊢ Membership.mem (γ := Set (realSpace K)) (Set.range normAtAllPlaces) x
have refine : ∀ (w : InfinitePlace K), normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
Tactic: refine ⟨mixedSpaceOfRealSpace x, funext fun w ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
x : realSpace K
hx : x ∈ s
w : InfinitePlace K
⊢ normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
have rw : (normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) =
  x w
Tactic: rw [normAtAllPlaces_apply, normAtPlace_mixedSpaceOfRealSpace (hs x hx w)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
x : realSpace K
hx : x ∈ s
w : InfinitePlace K
rw :
  (normAtPlace w : (a : mixedSpace K) → ℝ)
      ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) =
    x w
⊢ normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
have rw₁ : x w = x w
Tactic: rw [normAtAllPlaces_apply, normAtPlace_mixedSpaceOfRealSpace (hs x hx w)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ Membership.mem (α := mixedSpace K) (convexBodyLT K f) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
have simp_rw : Membership.mem (α := mixedSpace K) (convexBodyLT K f)
    ((RingHom.prod
            (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
              fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal sorry)
            (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
              fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding) :
          (a : K) → mixedSpace K)
        x :
      mixedSpace K) ↔
  ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
Tactic: simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ,
    forall_true_left, mem_ball_zero_iff, Pi.ringHom_apply, ← Complex.norm_real,
    embedding_of_isReal_apply, Subtype.forall, ← forall₂_or_left, ← not_isReal_iff_isComplex, em,
    forall_true_left, norm_embedding_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
x : K
simp_rw :
  Membership.mem (α := mixedSpace K) (convexBodyLT K f)
      ((RingHom.prod
              (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal ⋯)
              (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding) :
            (a : K) → mixedSpace K)
          x :
        mixedSpace K) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
⊢ Membership.mem (α := mixedSpace K) (convexBodyLT K f) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
have simp_rw₁ : Membership.mem (α := mixedSpace K) (convexBodyLT K f)
    (((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
              fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal sorry :
            (a : K) → { w : InfinitePlace K // w.IsReal } → ℝ)
          x,
        (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
              fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding :
            (a : K) → { w : InfinitePlace K // w.IsComplex } → ℂ)
          x) :
      ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) ↔
  ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
Tactic: simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ,
    forall_true_left, mem_ball_zero_iff, Pi.ringHom_apply, ← Complex.norm_real,
    embedding_of_isReal_apply, Subtype.forall, ← forall₂_or_left, ← not_isReal_iff_isComplex, em,
    forall_true_left, norm_embedding_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx : x ∈ convexBodyLT K f
⊢ -x ∈ convexBodyLT K f
have simp : ∀
  (hx :
    (∀ (a : InfinitePlace K) (b : a.IsReal),
        |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex),
        ‖x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)‖ < (↑(f a) : ℝ)),
  (∀ (a : InfinitePlace K) (b : a.IsReal),
      |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      ‖x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)‖ < (↑(f a) : ℝ)
Tactic: simp only [Set.mem_prod, Prod.fst_neg, Set.mem_pi, Set.mem_univ, Pi.neg_apply,
    mem_ball_zero_iff, norm_neg, Real.norm_eq_abs, forall_true_left, Subtype.forall,
    Prod.snd_neg] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
have simp_rw : ((Measure.prod volume volume :
        Measure (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ))) :
      (a : Set (mixedSpace K)) → ℝ≥0∞)
    (convexBodyLT K f) =
  HMul.hMul (α := ℝ≥0∞)
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ x : { w : InfinitePlace K // w.IsComplex },
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
Tactic: simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
simp_rw :
  ((Measure.prod volume volume :
          Measure (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ))) :
        (a : Set (mixedSpace K)) → ℝ≥0∞)
      (convexBodyLT K f) =
    HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
have simp_rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
    (((volume : Measure ({ w : InfinitePlace K // w.IsReal } → ℝ)) :
          (a : Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) Set.univ
          fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ball 0 (↑(f (↑w : InfinitePlace K)) : ℝ)) :
      ℝ≥0∞)
    (((volume : Measure ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
          (a : Set ({ w : InfinitePlace K // w.IsComplex } → ℂ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ) Set.univ
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ ball 0 (↑(f (↑w : InfinitePlace K)) : ℝ)) :
      ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞)
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ x : { w : InfinitePlace K // w.IsComplex },
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
Tactic: simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x : { w : InfinitePlace K // w.IsComplex },
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
have simp_rw : HMul.hMul (α := ℝ≥0∞)
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal 2 * ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ))
    (∏ x : { w : InfinitePlace K // w.IsComplex },
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) =
  ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
      ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    ((∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
      (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
Tactic: simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]