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
x : mixedSpace K
simp_rw :
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₁ :
  HAdd.hAdd (α := ℝ)
      (∑ w : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ w : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₂ :
  HAdd.hAdd (α := ℝ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑1 : ℝ) : ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ w : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑(↑w : InfinitePlace K).mult : ℝ) : ℝ)
          ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
simp_rw₃ :
  HAdd.hAdd (α := ℝ)
      (∑ x_1 : { w : InfinitePlace K // w.IsReal },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑1 : ℝ) : ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
      (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
        HMul.hMul (α := ℝ) (β := ℝ) ((↑2 : ℝ) : ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
⊢ convexBodySumFun x =
    ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
      HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
have simp_rw₄ : HAdd.hAdd (α := ℝ)
    (∑ x_1 : { w : InfinitePlace K // w.IsReal },
      HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ))
    (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
      HMul.hMul (α := ℝ) (β := ℝ) ((↑2 : ℝ) : ℝ)
        ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) =
  ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ +
    HMul.hMul (α := ℝ) 2 (∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖)
Tactic: simp_rw [convexBodySumFun_apply, sum_eq_sum_add_sum, mult_isReal, mult_isComplex,
    Nat.cast_one, one_mul, Nat.cast_ofNat, normAtPlace_apply_of_isReal (Subtype.prop _),
    normAtPlace_apply_of_isComplex (Subtype.prop _), Finset.mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
⊢ convexBodySumFun (x + y) ≤ convexBodySumFun x + convexBodySumFun y
have simp_rw : LE.le (α := ℝ)
  (∑ w : InfinitePlace K,
    HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (x + y) : ℝ))
  (∑ x_1 : InfinitePlace K,
    (↑x_1.mult : ℝ) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ)
        ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) y : ℝ))
Tactic: simp_rw [convexBodySumFun, ← Finset.sum_add_distrib, ← mul_add]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
⊢ convexBodySumFun (c • x) = |c| * convexBodySumFun x
have simp_rw : ∑ w : InfinitePlace K,
    HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) =
  |c| *
    ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: simp_rw [convexBodySumFun, normAtPlace_smul, ← mul_assoc, mul_comm, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
simp_rw :
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ convexBodySumFun (c • x) = |c| * convexBodySumFun x
have simp_rw₁ : ∑ x_1 : InfinitePlace K, (↑x_1.mult : ℝ) * HMul.hMul (β := ℝ) |c| ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) =
  |c| *
    ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: simp_rw [convexBodySumFun, normAtPlace_smul, ← mul_assoc, mul_comm, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
simp_rw :
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
simp_rw₁ :
  ∑ x_1 : InfinitePlace K, (↑x_1.mult : ℝ) * HMul.hMul (β := ℝ) |c| ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ convexBodySumFun (c • x) = |c| * convexBodySumFun x
have simp_rw₂ : ∑ x_1 : InfinitePlace K, HMul.hMul (β := ℝ) ((↑x_1.mult : ℝ) * |c|) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) =
  |c| *
    ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: simp_rw [convexBodySumFun, normAtPlace_smul, ← mul_assoc, mul_comm, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
simp_rw :
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
simp_rw₁ :
  ∑ x_1 : InfinitePlace K, (↑x_1.mult : ℝ) * HMul.hMul (β := ℝ) |c| ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
simp_rw₂ :
  ∑ x_1 : InfinitePlace K,
      HMul.hMul (β := ℝ) ((↑x_1.mult : ℝ) * |c|) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ convexBodySumFun (c • x) = |c| * convexBodySumFun x
have simp_rw₃ : ∑ x_1 : InfinitePlace K, HMul.hMul (β := ℝ) (|c| * (↑x_1.mult : ℝ)) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) =
  |c| *
    ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: simp_rw [convexBodySumFun, normAtPlace_smul, ← mul_assoc, mul_comm, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
simp_rw :
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
simp_rw₁ :
  ∑ x_1 : InfinitePlace K, (↑x_1.mult : ℝ) * HMul.hMul (β := ℝ) |c| ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
simp_rw₂ :
  ∑ x_1 : InfinitePlace K,
      HMul.hMul (β := ℝ) ((↑x_1.mult : ℝ) * |c|) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
simp_rw₃ :
  ∑ x_1 : InfinitePlace K,
      HMul.hMul (β := ℝ) (|c| * (↑x_1.mult : ℝ)) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) =
    |c| *
      ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ convexBodySumFun (c • x) = |c| * convexBodySumFun x
have simp_rw₄ : Eq (α := ℝ)
  (∑ x_1 : InfinitePlace K,
    HMul.hMul (β := ℝ) (|c| * (↑x_1.mult : ℝ)) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ))
  (∑ i : InfinitePlace K,
    |c| * HMul.hMul (α := ℝ) (β := ℝ) ((↑i.mult : ℝ) : ℝ) ((normAtPlace i : (a : mixedSpace K) → ℝ) x : ℝ))
Tactic: simp_rw [convexBodySumFun, normAtPlace_smul, ← mul_assoc, mul_comm, Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ convexBodySumFun x = 0 ↔ x = 0
have rw : (∀ (i : InfinitePlace K),
    Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ i →
      HMul.hMul (α := ℝ) (β := ℝ) ((↑i.mult : ℝ) : ℝ) ((normAtPlace i : (a : mixedSpace K) → ℝ) x : ℝ) = 0) ↔
  ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [← forall_normAtPlace_eq_zero_iff, convexBodySumFun, Finset.sum_eq_zero_iff_of_nonneg
    fun _ _ ↦ mul_nonneg (Nat.cast_pos.mpr mult_pos).le (normAtPlace_nonneg _ _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ ‖x‖ ≤ convexBodySumFun x
have rw : (Finset.sup' Finset.univ sorry fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x) ≤ convexBodySumFun x
Tactic: rw [norm_eq_sup'_normAtPlace]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ (Finset.sup' Finset.univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x) ≤
    convexBodySumFun x
have refine : ∀ (w : InfinitePlace K),
  Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w →
    (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤ convexBodySumFun x
Tactic: refine (Finset.sup'_le_iff _ _).mpr fun w _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤ convexBodySumFun x
have rw : (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) +
    ∑ x_1 ∈ Finset.erase Finset.univ w,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑x_1.mult : ℝ) : ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: rw [convexBodySumFun_apply, ← Finset.univ.add_sum_erase _ (Finset.mem_univ w)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) +
      ∑ x_1 ∈ Finset.erase Finset.univ w,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑x_1.mult : ℝ) : ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ)
have refine_1 : (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: refine le_add_of_le_of_nonneg ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
refine_1 :
  (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) +
      ∑ x_1 ∈ Finset.erase Finset.univ w,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑x_1.mult : ℝ) : ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ)
have refine_2 : LE.le (α := ℝ) 0
  (∑ x_1 ∈ Finset.erase Finset.univ w,
    HMul.hMul (α := ℝ) (β := ℝ) ((↑x_1.mult : ℝ) : ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ))
Tactic: refine le_add_of_le_of_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 : ℝ
hB : B ≤ 0
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have inl : ∀ (hB : B < 0),
  Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: obtain hB | hB := lt_or_eq_of_le hB
-- 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
inl :
  ∀ (hB : B < 0),
    Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have inr : ∀ (hB : B = 0),
  Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: obtain hB | hB := lt_or_eq_of_le hB
-- 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_1 : B ≤ 0
hB : B < 0
this : Eq (α := Set (mixedSpace K)) (convexBodySum K B) ∅
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) ∅) 0
Tactic: rw [this, measure_empty]
-- 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_1 : B ≤ 0
hB : B < 0
this : Eq (α := Set (mixedSpace K)) (convexBodySum K B) ∅
rw : Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) ∅) 0
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [this, measure_empty]
-- 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_1 : B ≤ 0
hB : B < 0
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have inl : Eq (α := Set (mixedSpace K)) (convexBodySum K B) ∅
Tactic: suffices convexBodySum K B = ∅ by rw [this, measure_empty]
-- 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_1 : B ≤ 0
hB : B < 0
⊢ Eq (α := Set (mixedSpace K)) (convexBodySum K B) ∅
have inl : ∀ (x : mixedSpace K),
  Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔ Membership.mem (γ := Set (mixedSpace K)) ∅ x
Tactic: ext x
-- 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_1 : B ≤ 0
hB : B < 0
x : mixedSpace K
⊢ Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔ Membership.mem (γ := Set (mixedSpace K)) ∅ x
have inl : ∀ (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x), Membership.mem (γ := Set (mixedSpace K)) ∅ x
Tactic: refine ⟨fun hx => ?_, fun h => h.elim⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB_1 : B ≤ 0
hB : B < 0
x : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x
⊢ Membership.mem (γ := Set (mixedSpace K)) ∅ x
have hx₁ : convexBodySumFun x ≤ B
Tactic: rw [Set.mem_setOf] at hx
Cleared hypotheses: hx
-- 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_1 : B ≤ 0
hB : B < 0
x : mixedSpace K
hx : convexBodySumFun x ≤ B
⊢ Membership.mem (γ := Set (mixedSpace K)) ∅ x
have linarith : B - 0 + (convexBodySumFun x - B) + (0 - convexBodySumFun x) = 0
Tactic: linarith [convexBodySumFun_nonneg x]
-- 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_1 : B ≤ 0
hB : B = 0
this : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {0}
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) {0} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [this, measure_singleton]
-- 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_1 : B ≤ 0
hB : B = 0
this : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {0}
rw : Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) {0} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [this, measure_singleton]
-- 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_1 : B ≤ 0
hB : B = 0
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have inr : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {0}
Tactic: suffices convexBodySum K B = { 0 } by rw [this, measure_singleton]
-- 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_1 : B ≤ 0
hB : B = 0
⊢ Eq (α := Set (mixedSpace K)) (convexBodySum K B) {0}
have inr : ∀ (x : mixedSpace K),
  Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔ Membership.mem (γ := Set (mixedSpace K)) {0} 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 : ℝ
hB_1 : B ≤ 0
hB : B = 0
x : mixedSpace K
⊢ Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔ Membership.mem (γ := Set (mixedSpace K)) {0} x
have inr : convexBodySumFun x ≤ 0 ↔ convexBodySumFun x = 0
Tactic: rw [convexBodySum, Set.mem_setOf_eq, Set.mem_singleton_iff, hB, ← convexBodySumFun_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
x : K
⊢ Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (convexBodySum K B)
      ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) ↔
    ∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) x : ℝ) ≤
      B
have simp_rw : ∑ x_1 : InfinitePlace K, HMul.hMul (α := ℝ) (β := ℝ) ((↑x_1.mult : ℝ) : ℝ) ((x_1 : (a : K) → ℝ) x : ℝ) ≤ B ↔
  ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) x : ℝ) ≤
    B
Tactic: simp_rw [Set.mem_setOf_eq, convexBodySumFun, normAtPlace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
x : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x
⊢ Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) (-x)
have rw : convexBodySumFun x ≤ B
Tactic: rw [Set.mem_setOf, convexBodySumFun_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ Convex ℝ (E := mixedSpace K) (convexBodySum K B)
have refine : ∀ (c : ℝ) (x : mixedSpace K) (h : 0 ≤ c), convexBodySumFun (c • x) ≤ c * convexBodySumFun x
Tactic: refine Convex_subadditive_le (fun _ _ => convexBodySumFun_add_le _ _) (fun c x h => ?_) 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 c : ℝ
x : mixedSpace K
h : 0 ≤ c
⊢ convexBodySumFun (c • x) ≤ c * convexBodySumFun x
have h₁ : c = |c|
Tactic: convert! le_of_eq (convexBodySumFun_smul c x)
-- 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: refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx 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 : ℝ
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
have simp_rw : ‖x - y‖ ≤ B + B
Tactic: simp_rw [dist_eq_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
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
have refine_1 : ‖x‖ ≤ B
Tactic: refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
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
refine_1 : ‖x‖ ≤ B
⊢ ‖x - y‖ ≤ B + B
have refine_2 : ‖y‖ ≤ B
Tactic: refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)