-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySum_volume_eq_zero_of_le_zero {B} (hB : B ≤ 0) :
    volume (convexBodySum K B) = 0

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
⊢ volume (convexBodySum K B) = 0

Tactic:
suffices convexBodySum K B = { 0 } by rw [this, measure_singleton]

Result:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
⊢ convexBodySum K B = {0}

Proof state:
case inr.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
x✝ : mixedSpace K
⊢ convexBodySumFun x✝ ≤ 0 ↔ convexBodySumFun x✝ = 0

Tactic:
exact (convexBodySumFun_nonneg _).le_iff_eq

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ volume (convexBodySum K B) = 0

Tactic:
obtain hB | hB := lt_or_eq_of_le hB

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
⊢ volume (convexBodySum K B) = 0

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
⊢ volume (convexBodySum K B) = 0

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
⊢ convexBodySum K B = {0}

Tactic:
ext

Result:
case inr.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
x✝ : mixedSpace K
⊢ x✝ ∈ convexBodySum K B ↔ x✝ ∈ {0}

Proof state:
case inl.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
x : mixedSpace K
hx : convexBodySumFun x ≤ B
⊢ x ∈ ∅

Tactic:
linarith [convexBodySumFun_nonneg x]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
this : convexBodySum K B = ∅
⊢ volume (convexBodySum K B) = 0

Tactic:
rw [this, measure_empty]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
this : convexBodySum K B = {0}
⊢ volume (convexBodySum K B) = 0

Tactic:
rw [this, measure_singleton]

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
⊢ volume (convexBodySum K B) = 0

Tactic:
suffices convexBodySum K B = ∅ by rw [this, measure_empty]

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
⊢ convexBodySum K B = ∅

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
⊢ convexBodySum K B = ∅

Tactic:
ext x

Result:
case inl.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
x : mixedSpace K
⊢ x ∈ convexBodySum K B ↔ x ∈ ∅

Proof state:
case inl.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
x : mixedSpace K
⊢ x ∈ convexBodySum K B ↔ x ∈ ∅

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

Result:
case inl.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
x : mixedSpace K
hx : x ∈ convexBodySum K B
⊢ x ∈ ∅

Proof state:
case inr.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
x✝ : mixedSpace K
⊢ x✝ ∈ convexBodySum K B ↔ x✝ ∈ {0}

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

Result:
case inr.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
x✝ : mixedSpace K
⊢ convexBodySumFun x✝ ≤ 0 ↔ convexBodySumFun x✝ = 0

Proof state:
case inl.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
x : mixedSpace K
hx : x ∈ convexBodySum K B
⊢ x ∈ ∅

Tactic:
rw [Set.mem_setOf] at hx

Result:
case inl.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B < 0
x : mixedSpace K
hx : convexBodySumFun x ≤ B
⊢ x ∈ ∅