case intro.intro
ι : Type ?u.36641
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
hy : y ∈ ↑(convexHull ℝ).toOrderHom t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
⊢ ∃ x', x' ∈ s ∧ ∃ y', y' ∈ t ∧ dist x y ≤ dist x' y'
ι : Type ?u.36641
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
hy : y ∈ ↑(convexHull ℝ).toOrderHom t
⊢ ∃ x', x' ∈ s ∧ ∃ y', y' ∈ t ∧ dist x y ≤ dist x' y'
rcases convexHull_exists_dist_ge hx y with ⟨x', hx', Hx'⟩
case intro.intro.intro.intro
ι : Type ?u.36641
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
hy : y ∈ ↑(convexHull ℝ).toOrderHom t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ ∃ x', x' ∈ s ∧ ∃ y', y' ∈ t ∧ dist x y ≤ dist x' y'
case intro.intro
ι : Type ?u.36641
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
hy : y ∈ ↑(convexHull ℝ).toOrderHom t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
⊢ ∃ x', x' ∈ s ∧ ∃ y', y' ∈ t ∧ dist x y ≤ dist x' y'
rcases convexHull_exists_dist_ge hy x' with ⟨y', hy', Hy'⟩
case intro.intro.intro.intro
ι : Type ?u.36641
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
hy : y ∈ ↑(convexHull ℝ).toOrderHom t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ dist x y ≤ dist x' y'
case intro.intro.intro.intro
ι : Type ?u.36641
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
hy : y ∈ ↑(convexHull ℝ).toOrderHom t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ ∃ x', x' ∈ s ∧ ∃ y', y' ∈ t ∧ dist x y ≤ dist x' y'
use x', hx', y', hy'
no goals
case intro.intro.intro.intro
ι : Type ?u.36641
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
hy : y ∈ ↑(convexHull ℝ).toOrderHom t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ dist x y ≤ dist x' y'
exact le_trans Hx' (dist_comm y x' ▸ dist_comm y' x' ▸ Hy')