awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
⊢ 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:
exact Finset.sum_le_sum
    fun _ _ ↦ mul_le_mul_of_nonneg_left (normAtPlace_add_le _ x y) (Nat.cast_pos.mpr mult_pos).le

Premises used: Iff.mpr, Nat.cast_pos, LT.lt.le, NumberField.mixedEmbedding.normAtPlace_add_le, NumberField.InfinitePlace.mult_pos, Finset.sum_le_sum, mul_le_mul_of_nonneg_left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 : ℝ)
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 : ℝ))
⊢ convexBodySumFun (c • x) = |c| * convexBodySumFun x

Tactic:
simp_rw [convexBodySumFun, normAtPlace_smul, ← mul_assoc, mul_comm, Finset.mul_sum, mul_assoc]

Premises used: Finset.mul_sum, NumberField.mixedEmbedding.convexBodySumFun, mul_assoc, mul_comm, NumberField.mixedEmbedding.normAtPlace_smul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
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 : ℝ)
⊢ convexBodySumFun x = 0 ↔ 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 _ _)]

Premises used: Iff.mpr, mul_nonneg, NumberField.mixedEmbedding.convexBodySumFun, Nat.cast_pos, Finset.sum_eq_zero_iff_of_nonneg, LT.lt.le, NumberField.InfinitePlace.mult_pos, NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff, NumberField.mixedEmbedding.normAtPlace_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ (∀ (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:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
rw :
  (Finset.sup' Finset.univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x) ≤
    convexBodySumFun x
⊢ ‖x‖ ≤ convexBodySumFun x

Tactic:
rw [norm_eq_sup'_normAtPlace]

Premises used: NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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

Tactic:
(Finset.sup'_le_iff _ _).mpr fun w _ ↦ ?_

Premises used: Iff.mpr, Finset.sup'_le_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
refine :
  ∀ (w : InfinitePlace K),
    Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w →
      (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤ convexBodySumFun x
⊢ (Finset.sup' Finset.univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x) ≤
    convexBodySumFun x

Tactic:
refine (Finset.sup'_le_iff _ _).mpr fun w _ ↦ ?_

Premises used: Iff.mpr, Finset.sup'_le_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
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 : ℝ)
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤ convexBodySumFun x

Tactic:
rw [convexBodySumFun_apply, ← Finset.univ.add_sum_erase _ (Finset.mem_univ w)]

Premises used: Finset.mem_univ, Finset.univ, NumberField.mixedEmbedding.convexBodySumFun_apply, Finset.add_sum_erase
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 : ℝ)

Tactic:
le_add_of_le_of_nonneg ?_ ?_

Premises used: le_add_of_le_of_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 : ℝ)
refine_2 :
  LE.le (α := ℝ) 0
    (∑ x_1 ∈ Finset.erase Finset.univ w,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑x_1.mult : ℝ) : ℝ) ((normAtPlace x_1 : (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 : ℝ)

Tactic:
refine le_add_of_le_of_nonneg ?_ ?_

Premises used: le_add_of_le_of_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 : ℝ)

Tactic:
le_mul_of_one_le_left (normAtPlace_nonneg w x) one_le_mult

Premises used: le_mul_of_one_le_left, NumberField.InfinitePlace.one_le_mult, NumberField.mixedEmbedding.normAtPlace_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 : ℝ)

Tactic:
exact le_mul_of_one_le_left (normAtPlace_nonneg w x) one_le_mult

Premises used: le_mul_of_one_le_left, NumberField.InfinitePlace.one_le_mult, NumberField.mixedEmbedding.normAtPlace_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
⊢ LE.le (α := ℝ) 0
    (∑ x_1 ∈ Finset.erase Finset.univ w,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑x_1.mult : ℝ) : ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ))

Tactic:
Finset.sum_nonneg (fun _ _ => mul_nonneg (Nat.cast_pos.mpr mult_pos).le
      (normAtPlace_nonneg _ _))

Premises used: Iff.mpr, mul_nonneg, Nat.cast_pos, LT.lt.le, Finset.sum_nonneg, NumberField.InfinitePlace.mult_pos, NumberField.mixedEmbedding.normAtPlace_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
⊢ LE.le (α := ℝ) 0
    (∑ x_1 ∈ Finset.erase Finset.univ w,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑x_1.mult : ℝ) : ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ))

Tactic:
exact Finset.sum_nonneg (fun _ _ => mul_nonneg (Nat.cast_pos.mpr mult_pos).le
      (normAtPlace_nonneg _ _))

Premises used: Iff.mpr, mul_nonneg, Nat.cast_pos, LT.lt.le, Finset.sum_nonneg, NumberField.InfinitePlace.mult_pos, NumberField.mixedEmbedding.normAtPlace_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Continuous.{u_1, 0} (X := mixedSpace K) convexBodySumFun

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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∞)
inr :
  ∀ (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∞)

Tactic:
obtain hB | hB := lt_or_eq_of_le hB

Premises used: lt_or_eq_of_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [this, measure_empty]

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB_1 : B ≤ 0
hB : B < 0
inl : Eq (α := Set (mixedSpace K)) (convexBodySum K B) ∅
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
suffices convexBodySum K B = ∅ by rw [this, measure_empty]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB_1 : B ≤ 0
hB : B < 0
inl :
  ∀ (x : mixedSpace K),
    Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔ Membership.mem (γ := Set (mixedSpace K)) ∅ x
⊢ Eq (α := Set (mixedSpace K)) (convexBodySum K B) ∅

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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

Tactic:
⟨fun hx => ?_, fun h => h.elim⟩

Premises used: False.elim, Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB_1 : B ≤ 0
hB : B < 0
x : mixedSpace K
inl :
  ∀ (hx : Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x), Membership.mem (γ := Set (mixedSpace K)) ∅ x
⊢ Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔ Membership.mem (γ := Set (mixedSpace K)) ∅ x

Tactic:
refine ⟨fun hx => ?_, fun h => h.elim⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
⊢ convexBodySumFun x ≤ B

Tactic:
rw [Set.mem_setOf] at hx

Premises used: Set.mem_setOf
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
linarith : B - 0 + (convexBodySumFun x - B) + (0 - convexBodySumFun x) = 0
⊢ Membership.mem (γ := Set (mixedSpace K)) ∅ x

Tactic:
linarith [convexBodySumFun_nonneg x]

Premises used: NumberField.mixedEmbedding.convexBodySumFun_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [this, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB_1 : B ≤ 0
hB : B = 0
inr : 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∞)

Tactic:
suffices convexBodySum K B = { 0 } by rw [this, measure_singleton]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB_1 : B ≤ 0
hB : B = 0
inr :
  ∀ (x : mixedSpace K),
    Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔ Membership.mem (γ := Set (mixedSpace K)) {0} x
⊢ Eq (α := Set (mixedSpace K)) (convexBodySum K B) {0}

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB_1 : B ≤ 0
hB : B = 0
x : mixedSpace K
inr : convexBodySumFun x ≤ 0 ↔ convexBodySumFun x = 0
⊢ Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) x ↔ Membership.mem (γ := Set (mixedSpace K)) {0} x

Tactic:
rw [convexBodySum, Set.mem_setOf_eq, Set.mem_singleton_iff, hB, ← convexBodySumFun_eq_zero_iff]

Premises used: NumberField.mixedEmbedding.convexBodySum, Set.mem_setOf_eq, Set.mem_singleton_iff, NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB_1 : B ≤ 0
hB : B = 0
x : mixedSpace K
⊢ convexBodySumFun x ≤ 0 ↔ convexBodySumFun x = 0

Tactic:
(convexBodySumFun_nonneg _).ge_iff_eq'

Premises used: NumberField.mixedEmbedding.convexBodySumFun_nonneg, LE.le.ge_iff_eq'
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB_1 : B ≤ 0
hB : B = 0
x : mixedSpace K
⊢ convexBodySumFun x ≤ 0 ↔ convexBodySumFun x = 0

Tactic:
exact (convexBodySumFun_nonneg _).ge_iff_eq'

Premises used: NumberField.mixedEmbedding.convexBodySumFun_nonneg, LE.le.ge_iff_eq'
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
x : K
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
⊢ 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

Tactic:
simp_rw [Set.mem_setOf_eq, convexBodySumFun, normAtPlace_apply]

Premises used: NumberField.mixedEmbedding.convexBodySumFun, Set.mem_setOf_eq, NumberField.mixedEmbedding.normAtPlace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
x : K
⊢ ∑ 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:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
rw : convexBodySumFun x ≤ B
⊢ Membership.mem (γ := Set (mixedSpace K)) (convexBodySum K B) (-x)

Tactic:
rw [Set.mem_setOf, convexBodySumFun_neg]

Premises used: NumberField.mixedEmbedding.convexBodySumFun_neg, Set.mem_setOf
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
⊢ convexBodySumFun x ≤ B

Tactic:
hx

Premises used: Set.Mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
⊢ convexBodySumFun x ≤ B

Tactic:
exact hx
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ Convex ℝ (E := mixedSpace K) (convexBodySum K B)

Tactic:
Convex_subadditive_le (fun _ _ => convexBodySumFun_add_le _ _) (fun c x h => ?_) B

Premises used: NumberField.mixedEmbedding.convexBodySumFun_add_le, setOf, Convex_subadditive_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
refine : ∀ (c : ℝ) (x : mixedSpace K) (h : 0 ≤ c), convexBodySumFun (c • x) ≤ c * convexBodySumFun x
⊢ Convex ℝ (E := mixedSpace K) (convexBodySum K B)

Tactic:
refine Convex_subadditive_le (fun _ _ => convexBodySumFun_add_le _ _) (fun c x h => ?_) B

Premises used: NumberField.mixedEmbedding.convexBodySumFun_add_le, Convex_subadditive_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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

Tactic:
le_of_eq (convexBodySumFun_smul c x)

Premises used: NumberField.mixedEmbedding.convexBodySumFun_smul, le_of_eq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B c : ℝ
x : mixedSpace K
h : 0 ≤ c
h₁ : c = |c|
⊢ convexBodySumFun (c • x) ≤ c * convexBodySumFun x

Tactic:
convert! le_of_eq (convexBodySumFun_smul c x)

Premises used: NumberField.mixedEmbedding.convexBodySumFun_smul, le_of_eq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B c : ℝ
x : mixedSpace K
h : 0 ≤ c
⊢ c = |c|

Tactic:
(abs_eq_self.mpr h).symm

Premises used: Iff.mpr, Eq.symm, abs_eq_self
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B c : ℝ
x : mixedSpace K
h : 0 ≤ c
⊢ c = |c|

Tactic:
exact (abs_eq_self.mpr h).symm

Premises used: Iff.mpr, Eq.symm, abs_eq_self
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
⊢ Bornology.IsBounded (α := mixedSpace K) (convexBodySum K B)

Tactic:
Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩

Premises used: Iff.mpr, Metric.isBounded_iff, HAdd.hAdd, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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)

Tactic:
refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩

Premises used: Iff.mpr, Metric.isBounded_iff, HAdd.hAdd, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
simp_rw : ‖x - y‖ ≤ B + B
⊢ dist x y ≤ B + B

Tactic:
simp_rw [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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

Tactic:
le_trans (norm_sub_le x y) (add_le_add ?_ ?_)

Premises used: norm_sub_le, add_le_add, le_trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
refine_2 : ‖y‖ ≤ B
⊢ ‖x - y‖ ≤ B + B

Tactic:
refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)

Premises used: norm_sub_le, add_le_add, le_trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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‖ ≤ B

Tactic:
le_trans (norm_le_convexBodySumFun x) hx

Premises used: NumberField.mixedEmbedding.norm_le_convexBodySumFun, le_trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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‖ ≤ B

Tactic:
exact le_trans (norm_le_convexBodySumFun x) hx

Premises used: NumberField.mixedEmbedding.norm_le_convexBodySumFun, le_trans