case inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.269436
G : Type ?u.269439
ι : Type ?u.269442
π : ι → Type ?u.269447
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ uIcc x y

case inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.269436
G : Type ?u.269439
ι : Type ?u.269442
π : ι → Type ?u.269447
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : y ≤ x
⊢ [x-[𝕜]y] ⊆ uIcc x y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.269436
G : Type ?u.269439
ι : Type ?u.269442
π : ι → Type ?u.269447
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
⊢ [x-[𝕜]y] ⊆ uIcc x y
cases' le_total x y with h h
case inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.269436
G : Type ?u.269439
ι : Type ?u.269442
π : ι → Type ?u.269447
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ Icc x y
case inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.269436
G : Type ?u.269439
ι : Type ?u.269442
π : ι → Type ?u.269447
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ uIcc x y
rw [uIcc_of_le h]
no goals
case inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.269436
G : Type ?u.269439
ι : Type ?u.269442
π : ι → Type ?u.269447
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ Icc x y
exact segment_subset_Icc h
case inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.269436
G : Type ?u.269439
ι : Type ?u.269442
π : ι → Type ?u.269447
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : y ≤ x
⊢ [y-[𝕜]x] ⊆ Icc y x
case inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.269436
G : Type ?u.269439
ι : Type ?u.269442
π : ι → Type ?u.269447
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : y ≤ x
⊢ [x-[𝕜]y] ⊆ uIcc x y
rw [uIcc_of_ge h, segment_symm]
no goals
case inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.269436
G : Type ?u.269439
ι : Type ?u.269442
π : ι → Type ?u.269447
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : y ≤ x
⊢ [y-[𝕜]x] ⊆ Icc y x
exact segment_subset_Icc h