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)

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)
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)
by_cases hp₁ : p₂ = p₁
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)

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)
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)
by_cases hp₃ : p₂ = p₃
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)
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)
have hs : Sbtw ℝ p₁ p₂ p₃ := ⟨h, hp₁, hp₃⟩
no goals
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)
exact (hs.dist_lt_max_dist _).le
no goals
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)
simp [hp₁]
no goals
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)
simp [hp₃]