case inl
𝕜 : Type u_1
E : Type ?u.290354
F : Type ?u.290357
G : Type ?u.290360
ι : Type ?u.290363
π : ι → Type ?u.290368
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxy : x ≠ y
h : x < y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)

case inr
𝕜 : Type u_1
E : Type ?u.290354
F : Type ?u.290357
G : Type ?u.290360
ι : Type ?u.290363
π : ι → Type ?u.290368
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxy : x ≠ y
h : y < x
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
𝕜 : Type u_1
E : Type ?u.290354
F : Type ?u.290357
G : Type ?u.290360
ι : Type ?u.290363
π : ι → Type ?u.290368
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxy : x ≠ y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
cases' hxy.lt_or_lt with h h
no goals
case inl
𝕜 : Type u_1
E : Type ?u.290354
F : Type ?u.290357
G : Type ?u.290360
ι : Type ?u.290363
π : ι → Type ?u.290368
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxy : x ≠ y
h : x < y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]
no goals
case inr
𝕜 : Type u_1
E : Type ?u.290354
F : Type ?u.290357
G : Type ?u.290360
ι : Type ?u.290363
π : ι → Type ?u.290368
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxy : x ≠ y
h : y < x
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
rw [openSegment_symm, openSegment_eq_Ioo h, max_eq_left h.le, min_eq_right h.le]