awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
have refine : ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
  (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), dist x y ≤ B + B
Tactic: classical
  refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩
  simp_rw [dist_eq_norm]
  refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)
  · exact le_trans (norm_le_convexBodySumFun x) hx
  · exact le_trans (norm_le_convexBodySumFun y) hy
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
refine :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), dist x y ≤ B + B
⊢ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
have refine₁ : ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
  (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), ‖x - y‖ ≤ B + B
Tactic: classical
  refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩
  simp_rw [dist_eq_norm]
  refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)
  · exact le_trans (norm_le_convexBodySumFun x) hx
  · exact le_trans (norm_le_convexBodySumFun y) hy
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
refine :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), dist x y ≤ B + B
refine₁ :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), ‖x - y‖ ≤ B + B
⊢ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
have refine_1 : ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
  (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), ‖x‖ ≤ B
Tactic: classical
  refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩
  simp_rw [dist_eq_norm]
  refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)
  · exact le_trans (norm_le_convexBodySumFun x) hx
  · exact le_trans (norm_le_convexBodySumFun y) hy
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
refine :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), dist x y ≤ B + B
refine₁ :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), ‖x - y‖ ≤ B + B
refine_1 :
  ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
    (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), ‖x‖ ≤ B
⊢ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
have refine_2 : ∀ (x : mixedSpace K) (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x) (y : mixedSpace K)
  (hy : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) y), ‖y‖ ≤ B
Tactic: classical
  refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩
  simp_rw [dist_eq_norm]
  refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)
  · exact le_trans (norm_le_convexBodySumFun x) hx
  · exact le_trans (norm_le_convexBodySumFun y) hy
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ IsCompact (X := mixedSpace K) (convexBodySum K B)
have rw : IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
Tactic: rw [Metric.isCompact_iff_isClosed_bounded]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
have refine : IsClosed (X := mixedSpace K) (convexBodySum K B)
Tactic: refine ⟨?_, convexBodySum_isBounded K B⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ IsClosed (X := mixedSpace K) (convexBodySum K B)
have h : Eq (α := Set (mixedSpace K)) (convexBodySum K B) (convexBodySumFun ⁻¹' Set.Icc 0 B)
Tactic: convert! IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ Eq (α := Set (mixedSpace K)) (convexBodySum K B) (convexBodySumFun ⁻¹' Set.Icc 0 B)
have h : ∀ (x : mixedSpace K),
  Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔
    Membership.mem (γ := Set (mixedSpace K)) (convexBodySumFun ⁻¹' Set.Icc 0 B) x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ IsCompact (X := mixedSpace K) (convexBodySum K B)
have rw : IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
Tactic: classical
  rw [Metric.isCompact_iff_isClosed_bounded]
  refine ⟨?_, convexBodySum_isBounded K B⟩
  convert! IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
  ext
  simp [convexBodySumFun_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
rw rw₁ rw₂ :
  IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
⊢ IsCompact (X := mixedSpace K) (convexBodySum K B)
have rw₃ : IsClosed (X := mixedSpace K) (convexBodySum K B)
Tactic: classical
  rw [Metric.isCompact_iff_isClosed_bounded]
  refine ⟨?_, convexBodySum_isBounded K B⟩
  convert! IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
  ext
  simp [convexBodySumFun_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
rw rw₁ rw₂ :
  IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
rw₃ : IsClosed (X := mixedSpace K) (convexBodySum K B)
⊢ IsCompact (X := mixedSpace K) (convexBodySum K B)
have h : Eq (α := Set (mixedSpace K)) (convexBodySum K B) (convexBodySumFun ⁻¹' Set.Icc 0 B)
Tactic: classical
  rw [Metric.isCompact_iff_isClosed_bounded]
  refine ⟨?_, convexBodySum_isBounded K B⟩
  convert! IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
  ext
  simp [convexBodySumFun_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
rw rw₁ rw₂ :
  IsClosed (X := mixedSpace K) (convexBodySum K B) ∧ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)
rw₃ : IsClosed (X := mixedSpace K) (convexBodySum K B)
h : Eq (α := Set (mixedSpace K)) (convexBodySum K B) (convexBodySumFun ⁻¹' Set.Icc 0 B)
⊢ IsCompact (X := mixedSpace K) (convexBodySum K B)
have h₁ : ∀ (x : mixedSpace K),
  Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔
    Membership.mem (γ := Set (mixedSpace K)) (convexBodySumFun ⁻¹' Set.Icc 0 B) x
Tactic: classical
  rw [Metric.isCompact_iff_isClosed_bounded]
  refine ⟨?_, convexBodySum_isBounded K B⟩
  convert! IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
  ext
  simp [convexBodySumFun_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ convexBodySumFactor K ≠ 0
have refine : HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (NNReal.pi / 2) ^ nrComplexPlaces K ≠ 0
Tactic: refine div_ne_zero ?_ <| Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
have inl : ∀ (hB : B ≤ 0),
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
Tactic: obtain hB | hB := le_or_gt B 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
inl :
  ∀ (hB : B ≤ 0),
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
      (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
have inr : ∀ (hB : 0 < B),
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
Tactic: obtain hB | hB := le_or_gt B 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : B ≤ 0
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
have inl : finrank ℚ K ≠ 0
Tactic: rw [convexBodySum_volume_eq_zero_of_le_zero K hB, ofReal_eq_zero.mpr hB, zero_pow, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    (↑(convexBodySumFactor K) : ℝ≥0∞) * ENNReal.ofReal B ^ finrank ℚ K
have rw : ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
  ENNReal.ofReal B ^ finrank ℚ K * (↑(convexBodySumFactor K) : ℝ≥0∞)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    ENNReal.ofReal B ^ finrank ℚ K * (↑(convexBodySumFactor K) : ℝ≥0∞)
have h : convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
Tactic: convert! addHaar_smul volume B (convexBodySum K 1)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h : convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    ENNReal.ofReal B ^ finrank ℚ K * (↑(convexBodySumFactor K) : ℝ≥0∞)
have h₁ : ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank.{0, u_1} ℝ (mixedSpace K)|
Tactic: convert! addHaar_smul volume B (convexBodySum K 1)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h : convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
h₁ : ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank.{0, u_1} ℝ (mixedSpace K)|
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) =
    ENNReal.ofReal B ^ finrank ℚ K * (↑(convexBodySumFactor K) : ℝ≥0∞)
have h₂ : (↑(convexBodySumFactor K) : ℝ≥0∞) =
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1)
Tactic: convert! addHaar_smul volume B (convexBodySum K 1)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₂ : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  {a : mixedSpace K |
    LE.le (α := ℝ)
      (∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
      1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
h₂ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ w : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
        1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₃ : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  {a : mixedSpace K |
    LE.le (α := ℝ)
      (∑ x : InfinitePlace K, (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B⁻¹| ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
      1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
h₂ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ w : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
        1}
h₃ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B⁻¹| ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₄ : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  {a : mixedSpace K |
    LE.le (α := ℝ)
      (∑ x : InfinitePlace K, (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B|⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
      1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
h₂ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ w : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
        1}
h₃ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B⁻¹| ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₄ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B|⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₅ : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  {a : mixedSpace K |
    LE.le (α := ℝ)
      (∑ x : InfinitePlace K, (↑x.mult : ℝ) * HMul.hMul (β := ℝ) B⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
      1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
h₂ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ w : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
        1}
h₃ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B⁻¹| ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₄ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B|⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₅ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K, (↑x.mult : ℝ) * HMul.hMul (β := ℝ) B⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)
have h₆ : Eq (α := Set (mixedSpace K)) (convexBodySum K B)
  {a : mixedSpace K |
    LE.le (α := ℝ)
      (∑ x : InfinitePlace K, HMul.hMul (β := ℝ) ((↑x.mult : ℝ) * B⁻¹) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
      1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]