-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem convexHull_ediam (s : Set E) : EMetric.diam (convexHull ℝ s) = EMetric.diam s

Proof state:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ ENNReal.ofReal (dist x y) ≤ EMetric.diam s

Tactic:
apply le_trans (ENNReal.ofReal_le_ofReal H)

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ ENNReal.ofReal (dist x' y') ≤ EMetric.diam s

Proof state:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x y ≤ EMetric.diam s

Tactic:
rw [edist_dist]

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ ENNReal.ofReal (dist x y) ≤ EMetric.diam s

Proof state:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x' y' ≤ EMetric.diam s

Tactic:
exact EMetric.edist_le_diam_of_mem hx' hy'

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
⊢ EMetric.diam ((convexHull ℝ) s) = EMetric.diam s

Tactic:
refine (EMetric.diam_le fun x hx y hy => ?_).antisymm (EMetric.diam_mono <| subset_convexHull ℝ s)

Result:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
⊢ edist x y ≤ EMetric.diam s

Proof state:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ ENNReal.ofReal (dist x' y') ≤ EMetric.diam s

Tactic:
rw [← edist_dist]

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x' y' ≤ EMetric.diam s

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
⊢ edist x y ≤ EMetric.diam s

Tactic:
rcases convexHull_exists_dist_ge2 hx hy with ⟨x', hx', y', hy', H⟩

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x y ≤ EMetric.diam s