𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
⊢ [x-[𝕜]y] ⊆ insert x (insert y (openSegment 𝕜 x y))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
⊢ insert x (insert y (openSegment 𝕜 x y)) = [x-[𝕜]y]
simp only [subset_antisymm_iff, insert_subset, left_mem_segment, right_mem_segment,
  openSegment_subset_segment, true_and_iff]
case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
⊢ [x-[𝕜]y] ⊆ insert x (insert y (openSegment 𝕜 x y))
rintro z ⟨a, b, ha, hb, hab, rfl⟩
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b = 0 → a • x + b • y = x

case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
⊢ a = 0 → a • x + b • y = y

case intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y
case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))
refine' hb.eq_or_gt.imp _ fun hb' => ha.eq_or_gt.imp _ fun ha' => _
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a + 0 = 1
⊢ a • x + 0 • y = x
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b = 0 → a • x + b • y = x
rintro rfl
no goals
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a + 0 = 1
⊢ a • x + 0 • y = x
rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y = y
case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
⊢ a = 0 → a • x + b • y = y
rintro rfl
no goals
case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y = y
rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
no goals
case intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.40657
G : Type ?u.40660
ι : Type ?u.40663
π : ι → Type ?u.40668
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y
exact ⟨a, b, ha', hb', hab, rfl⟩