[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
have hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p := by simpa using h.left_ne_right
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p ≠ p₃ -ᵥ p
[PROOFSTEP]
simpa using h.left_ne_right
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rw [Sbtw, ← wbtw_vsub_const_iff p, Wbtw, affineSegment_eq_segment, ← insert_endpoints_openSegment, Set.mem_insert_iff,
  Set.mem_insert_iff] at h 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rcases h with ⟨h | h | h, hp₂p₁, hp₂p₃⟩
[GOAL]
case intro.inl.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₁ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rw [vsub_left_cancel_iff] at h 
[GOAL]
case intro.inl.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₁
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
exact False.elim (hp₂p₁ h)
[GOAL]
case intro.inr.inl.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rw [vsub_left_cancel_iff] at h 
[GOAL]
case intro.inr.inl.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₃
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
exact False.elim (hp₂p₃ h)
[GOAL]
case intro.inr.inr.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rw [openSegment_eq_image, Set.mem_image] at h 
[GOAL]
case intro.inr.inr.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : ∃ x, x ∈ Set.Ioo 0 1 ∧ (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rcases h with ⟨r, ⟨hr0, hr1⟩, hr⟩
[GOAL]
case intro.inr.inr.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
simp_rw [@dist_eq_norm_vsub V, ← hr]
[GOAL]
case intro.inr.inr.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ ‖(1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p)‖ < max ‖p₁ -ᵥ p‖ ‖p₃ -ᵥ p‖
[PROOFSTEP]
exact norm_combo_lt_of_ne (le_max_left _ _) (le_max_right _ _) hp₁p₃ (sub_pos.2 hr1) hr0 (by abel)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ 1 - r + r = 1
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ 1 - r + r = 1
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
by_cases hp₁ : p₂ = p₁
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : p₂ = p₁
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
simp [hp₁]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
by_cases hp₃ : p₂ = p₃
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
hp₃ : p₂ = p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
simp [hp₃]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
hp₃ : ¬p₂ = p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
have hs : Sbtw ℝ p₁ p₂ p₃ := ⟨h, hp₁, hp₃⟩
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
hp₃ : ¬p₂ = p₃
hs : Sbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
exact (hs.dist_lt_max_dist _).le
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₁ p₂ p₃
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
exact hw
[GOAL]
case inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
by_cases hp₃p₂ : p₃ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : p₃ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
simp [hp₃p₂]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
have hs : Sbtw ℝ p₂ p₃ p₁ := ⟨hw, hp₃p₂, hp₁p₃.symm⟩
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
have hs' := hs.dist_lt_max_dist p
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : dist p₃ p < max (dist p₂ p) (dist p₁ p)
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, or_false_iff] at hs' 
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : r < dist p₂ p
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
exact False.elim (hp₂.not_lt hs')
[GOAL]
case inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
by_cases hp₁p₂ : p₁ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : p₁ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
simp [hp₁p₂]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
have hs : Sbtw ℝ p₃ p₁ p₂ := ⟨hw, hp₁p₃, hp₁p₂⟩
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
have hs' := hs.dist_lt_max_dist p
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
hs' : dist p₁ p < max (dist p₃ p) (dist p₂ p)
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, false_or_iff] at hs' 
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
hs' : r < dist p₂ p
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
exact False.elim (hp₂.not_lt hs')
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p < r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
⊢ Sbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
refine' ⟨h.wbtw_of_dist_eq_of_dist_le hp₁ hp₂.le hp₃ hp₁p₃, _, _⟩
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p < r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
⊢ p₂ ≠ p₁
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₂ p₃ : P
r : ℝ
hp₂ : dist p₂ p < r
hp₃ : dist p₃ p = r
h : Collinear ℝ {p₂, p₂, p₃}
hp₁ : dist p₂ p = r
hp₁p₃ : p₂ ≠ p₃
⊢ False
[PROOFSTEP]
exact hp₂.ne hp₁
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p < r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
⊢ p₂ ≠ p₃
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ : P
r : ℝ
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p < r
h : Collinear ℝ {p₁, p₂, p₂}
hp₃ : dist p₂ p = r
hp₁p₃ : p₁ ≠ p₂
⊢ False
[PROOFSTEP]
exact hp₂.ne hp₃
