awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₁ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ p₂ = p₁

Tactic:
rw [vsub_left_cancel_iff] at h

Premises used: vsub_left_cancel_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₁ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
h₁ : p₂ = p₁
⊢ p₂ ≠ p₁

Tactic:
rw [vsub_left_cancel_iff] at h

Premises used: vsub_left_cancel_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₁ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
h₁ : p₂ = p₁
hp₂p₂ : p₂ ≠ p₁
⊢ p₂ ≠ p₃

Tactic:
rw [vsub_left_cancel_iff] at h

Premises used: vsub_left_cancel_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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)

Tactic:
False.elim (hp₂p₁ h)

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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)

Tactic:
exact False.elim (hp₂p₁ h)

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ p₂ = p₃

Tactic:
rw [vsub_left_cancel_iff] at h

Premises used: vsub_left_cancel_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
h₁ : p₂ = p₃
⊢ p₂ ≠ p₁

Tactic:
rw [vsub_left_cancel_iff] at h

Premises used: vsub_left_cancel_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
h₁ : p₂ = p₃
hp₂p₂ : p₂ ≠ p₁
⊢ p₂ ≠ p₃

Tactic:
rw [vsub_left_cancel_iff] at h

Premises used: vsub_left_cancel_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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)

Tactic:
False.elim (hp₂p₃ h)

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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)

Tactic:
exact False.elim (hp₂p₃ h)

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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₃
⊢ ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x ∧ (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p

Tactic:
rw [openSegment_eq_image, Set.mem_image] at h

Premises used: Set.mem_image, openSegment_eq_image
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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₃
h₁ : ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x ∧ (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
⊢ p₂ ≠ p₁

Tactic:
rw [openSegment_eq_image, Set.mem_image] at h

Premises used: Set.mem_image, openSegment_eq_image
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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₃
h₁ : ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x ∧ (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
hp₂p₂ : p₂ ≠ p₁
⊢ p₂ ≠ p₃

Tactic:
rw [openSegment_eq_image, Set.mem_image] at h

Premises used: Set.mem_image, openSegment_eq_image
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x ∧ (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
inr :
  ∀ (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)
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
rcases h with ⟨r, ⟨hr0, hr1⟩, hr⟩
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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
inr : ‖(1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p)‖ < max ‖p₁ -ᵥ p‖ ‖p₃ -ᵥ p‖
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
simp_rw [@dist_eq_norm_vsub V, ← hr]

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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

Tactic:
abel
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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‖

Tactic:
exact
      norm_combo_lt_of_ne (le_max_left _ _) (le_max_right _ _) hp₁p₃ (sub_pos.2 hr1) hr0 (by abel)

Premises used: le_max_right, Iff.mpr, sub_pos, le_max_left, norm_combo_lt_of_ne
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
pos : ∀ (hp₁ : p₂ = p₁), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
neg : ∀ (hp₁ : ¬p₂ = p₁), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)

Tactic:
by_cases hp₁ : p₂ = p₁
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : p₂ = p₁
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)

Tactic:
simp [hp₁]
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
pos : ∀ (hp₃ : p₂ = p₃), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
neg : ∀ (hp₃ : ¬p₂ = p₃), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)

Tactic:
by_cases hp₃ : p₂ = p₃
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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)

Tactic:
simp [hp₃]
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
hp₃ : ¬p₂ = p₃
⊢ Sbtw ℝ p₁ p₂ p₃

Tactic:
have hs : Sbtw ℝ p₁ p₂ p₃ := ⟨h, hp₁, hp₃⟩
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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)

Tactic:
(hs.dist_lt_max_dist _).le

Premises used: LT.lt.le, Sbtw.dist_lt_max_dist
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
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)

Tactic:
exact (hs.dist_lt_max_dist _).le

Premises used: LT.lt.le, Sbtw.dist_lt_max_dist
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
inl : ∀ (hw : Wbtw ℝ p₁ p₂ p₃), Wbtw ℝ p₁ p₂ p₃
inr : ∀ (hw : Wbtw ℝ p₂ p₃ p₁), Wbtw ℝ p₁ p₂ p₃
inr₁ : ∀ (hw : Wbtw ℝ p₃ p₁ p₂), Wbtw ℝ p₁ p₂ p₃
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)

Premises used: Collinear.wbtw_or_wbtw_or_wbtw
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₃

Tactic:
hw
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₃

Tactic:
exact hw
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₁
pos : ∀ (hp₃p₂ : p₃ = p₂), Wbtw ℝ p₁ p₂ p₃
neg : ∀ (hp₃p₂ : ¬p₃ = p₂), Wbtw ℝ p₁ p₂ p₃
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
by_cases hp₃p₂ : p₃ = p₂
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₃

Tactic:
simp [hp₃p₂]
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₂
⊢ Sbtw ℝ p₂ p₃ p₁

Tactic:
have hs : Sbtw ℝ p₂ p₃ p₁ := ⟨hw, hp₃p₂, hp₁p₃.symm⟩
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₁
⊢ dist p₃ p < max (dist p₂ p) (dist p₁ p)

Tactic:
have hs' := hs.dist_lt_max_dist p
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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)
⊢ r < dist p₂ p

Tactic:
rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, or_false] at hs'

Premises used: lt_self_iff_false, or_false, lt_max_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₃

Tactic:
False.elim (hp₂.not_gt hs')

Premises used: False.elim, LE.le.not_gt
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₃

Tactic:
exact False.elim (hp₂.not_gt hs')

Premises used: False.elim, LE.le.not_gt
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₂
pos : ∀ (hp₁p₂ : p₁ = p₂), Wbtw ℝ p₁ p₂ p₃
neg : ∀ (hp₁p₂ : ¬p₁ = p₂), Wbtw ℝ p₁ p₂ p₃
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
by_cases hp₁p₂ : p₁ = p₂
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₃

Tactic:
simp [hp₁p₂]
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₂
⊢ Sbtw ℝ p₃ p₁ p₂

Tactic:
have hs : Sbtw ℝ p₃ p₁ p₂ := ⟨hw, hp₁p₃, hp₁p₂⟩
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₂
⊢ dist p₁ p < max (dist p₃ p) (dist p₂ p)

Tactic:
have hs' := hs.dist_lt_max_dist p
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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)
⊢ r < dist p₂ p

Tactic:
rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, false_or] at hs'

Premises used: false_or, lt_self_iff_false, lt_max_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₃

Tactic:
False.elim (hp₂.not_gt hs')

Premises used: False.elim, LE.le.not_gt
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {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₃

Tactic:
exact False.elim (hp₂.not_gt hs')

Premises used: False.elim, LE.le.not_gt
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
⊢ dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a -[ℝ] c -ᵥ a]

Tactic:
simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
      eq_comm]

Premises used: sub_add_sub_cancel', dist_eq_norm', mem_segment_iff_sameRay, sameRay_iff_norm_add, eq_comm
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
⊢ dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a -[ℝ] c -ᵥ a]

Tactic:
have :
      dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔
        b -ᵥ a ∈ segment ℝ (a -ᵥ a) (c -ᵥ a) := by
    simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
      eq_comm]
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
this : dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a -[ℝ] c -ᵥ a]
⊢ dist a b + dist b c = dist a c ↔ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ a) '' affineSegment ℝ a c) (b -ᵥ a)

Tactic:
simp_rw [dist_vsub_cancel_right, ← affineSegment_eq_segment, ← affineSegment_vsub_const_image]
    at this

Premises used: dist_vsub_cancel_right, affineSegment_eq_segment, affineSegment_vsub_const_image
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
this :
  dist a b + dist b c = dist a c ↔ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ a) '' affineSegment ℝ a c) (b -ᵥ a)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : dist a b + dist b c = dist a c ↔ b ∈ affineSegment ℝ a c), dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
rwa [(vsub_left_injective _).mem_set_image] at this

Premises used: vsub_left_injective, Function.Injective.mem_set_image
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
rw : dist a c ≠ dist a b + dist b c ↔ ¬Wbtw ℝ a b c
rw₁ : dist a c = dist a b + dist b c ↔ Wbtw ℝ a b c
rw₂ : dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
rw₃ rw₄ : Wbtw ℝ a b c ↔ Wbtw ℝ a b c
⊢ dist a c < dist a b + dist b c ↔ ¬Wbtw ℝ a b c

Tactic:
rw [← ne_iff_lt_iff_le.mpr (dist_triangle _ _ _), not_iff_not, eq_comm, dist_add_dist_eq_iff]

Premises used: dist_triangle, not_iff_not, Iff.mpr, eq_comm, dist_add_dist_eq_iff, ne_iff_lt_iff_le
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
rw₂ : ‖y -ᵥ x‖ + dist (y -ᵥ x) (z -ᵥ x) = ‖z -ᵥ x‖
rw₃ : ‖y -ᵥ x‖ + dist y z = ‖z -ᵥ x‖
rw₄ : dist x y + dist y z = ‖z -ᵥ x‖
rw₅ : dist x y + dist y z = dist x z
rw₆ : r * dist x z + dist y z = dist x z
rw₇ : r * dist x z + (1 - r) * dist x z = dist x z
rw₈ : (r + (1 - r)) * dist x z = dist x z
rw₉ : 1 * dist x z = dist x z
rw₁₀ rw₁₁ : dist x z = dist x z
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]

Tactic:
rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]

Premises used: add_mul, dist_eq_norm_vsub', dist_vsub_cancel_right, dist_add_dist_eq_iff, add_sub_cancel, mem_segment_iff_wbtw, dist_zero, one_mul