case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.173927
E : Type u_2
F : Type ?u.173933
β : Type ?u.173936
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y
𝕜 : Type u_1
𝕝 : Type ?u.173927
E : Type u_2
F : Type ?u.173933
β : Type ?u.173936
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
⊢ x = y
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
no goals
case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.173927
E : Type u_2
F : Type ?u.173933
β : Type ?u.173936
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y
classical
  by_contra hxy
  exact
    (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel'_right _ _, rfl⟩).2
      (hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel'_right _ _)
case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.173927
E : Type u_2
F : Type ?u.173933
β : Type ?u.173936
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
hxy : ¬x = y
⊢ False
case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.173927
E : Type u_2
F : Type ?u.173933
β : Type ?u.173936
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y
by_contra hxy
no goals
case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.173927
E : Type u_2
F : Type ?u.173933
β : Type ?u.173936
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
hxy : ¬x = y
⊢ False
exact
  (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel'_right _ _, rfl⟩).2
    (hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel'_right _ _)