case inl
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
h : Metric.Bounded ∅
⊢ EMetric.diam ∅ = ENNReal.ofReal (sSup ∅ - sInf ∅)

case inr
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
⊢ EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
⊢ EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)
rcases eq_empty_or_nonempty s with (rfl | hne)
case inr.refine'_1
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ dist x y ≤ sSup s - sInf s

case inr.refine'_2
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
⊢ ENNReal.ofReal (sSup s - sInf s) ≤ EMetric.diam s
case inr
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
⊢ EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)
refine' le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => _) _
no goals
case inl
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
h : Metric.Bounded ∅
⊢ EMetric.diam ∅ = ENNReal.ofReal (sSup ∅ - sInf ∅)
simp
case inr.refine'_1
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
this : s ⊆ Icc (sInf s) (sSup s)
⊢ dist x y ≤ sSup s - sInf s
case inr.refine'_1
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ dist x y ≤ sSup s - sInf s
have := Real.subset_Icc_sInf_sSup_of_bounded h
no goals
case inr.refine'_1
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
this : s ⊆ Icc (sInf s) (sSup s)
⊢ dist x y ≤ sSup s - sInf s
exact Real.dist_le_of_mem_Icc (this hx) (this hy)
case inr.refine'_2.h
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
⊢ sSup s - sInf s ≤ ENNReal.toReal (EMetric.diam s)
case inr.refine'_2
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
⊢ ENNReal.ofReal (sSup s - sInf s) ≤ EMetric.diam s
apply ENNReal.ofReal_le_of_le_toReal
case inr.refine'_2.h
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
⊢ sSup s - sInf s ≤ Metric.diam (closure s)
case inr.refine'_2.h
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
⊢ sSup s - sInf s ≤ ENNReal.toReal (EMetric.diam s)
rw [← Metric.diam, ← Metric.diam_closure]
case inr.refine'_2.h
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
h' : BddBelow s ∧ BddAbove s
⊢ sSup s - sInf s ≤ Metric.diam (closure s)
case inr.refine'_2.h
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
⊢ sSup s - sInf s ≤ Metric.diam (closure s)
have h' := Real.bounded_iff_bddBelow_bddAbove.1 h
no goals
case inr.refine'_2.h
α : Type ?u.434159
β : Type ?u.434162
γ : Type ?u.434165
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
hne : Set.Nonempty s
h' : BddBelow s ∧ BddAbove s
⊢ sSup s - sInf s ≤ Metric.diam (closure s)
calc sSup s - sInf s ≤ dist (sSup s) (sInf s) := le_abs_self _
_ ≤ Metric.diam (closure s) := dist_le_diam_of_mem h.closure (csSup_mem_closure hne h'.2)
    (csInf_mem_closure hne h'.1)